nLab shape modality



Cohesive \infty-Toposes

Modalities, Closure and Reflection

Deduction and Induction

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels





In a locally ∞-connected (∞,1)-topos with fully faithful inverse image (such as a cohesive (∞,1)-topos), the extra left adjoint Π\Pi to the inverse image DiscDisc of the global sections geometric morphism Γ\Gamma induces a higher modality ʃDiscΠ\esh \coloneqq Disc \circ \Pi, which sends an object to something that may be regarded equivalently as its geometric realization or its fundamental ∞-groupoid (see at fundamental ∞-groupoid of a locally ∞-connected (∞,1)-topos and at shape via cohesive path ∞-groupoid). In either case ʃX\esh X may be thought of as the shape of XX and therefore one may call ʃ\esh the shape modality. It forms an adjoint modality with the flat modality DiscΓ\flat \coloneqq Disc \circ \Gamma.


In type theory

We assume a dependent type theory with crisp term judgments a::Aa::A in addition to the usual (cohesive) type and term judgments AtypeA \; \mathrm{type} and a:Aa:A, as well as context judgments Ξ|Γctx\Xi \vert \Gamma \; \mathrm{ctx} where Ξ\Xi is a list of crisp term judgments, and Γ\Gamma is a list of cohesive term judgments. A crisp type is a type in the context Ξ|()\Xi \vert (), where ()() is the empty list of cohesive term judgments. In addition, we also assume the dependent type theory has typal equality and judgmental equality, as well as the following axiom of cohesion:

There is a crisp type Ξ|()Rtype\Xi \vert () \vdash R \; \mathrm{type} such that given any crisp type Ξ|()Atype\Xi \vert () \vdash A \; \mathrm{type}, AA is discrete if and only if the function const A,R:A(RA)\mathrm{const}_{A, R}:A \to (R \to A) is an equivalence of types.

From here, there are two different notions of the shape modality which could be defined in the type theory, the strict shape modality, which uses judgmental equality in the computation rule and uniqueness rule, and the weak shape modality, which uses typal equality in the computation rule and uniqueness rule. When applied to a type they result in strict shape types and weak shape types respectively. The natural deduction rules for strict and weak shape types are provided as follows:

  • Formation rules for weak and strict shape types:
Ξ|ΓAtypeΞ|ΓʃAtypeʃform\frac{\Xi \vert \Gamma \vdash A \; \mathrm{type}}{\Xi \vert \Gamma \vdash \esh A \; \mathrm{type}}\esh-\mathrm{form}
  • Introduction rules for weak and strict shape types:
Ξ|Γa:AΞ|Γσ A(a):ʃAʃintro1\frac{\Xi \vert \Gamma \vdash a:A}{\Xi \vert \Gamma \vdash \sigma_A(a):\esh A}\esh-\mathrm{intro}1
Ξ|Γg:RʃAΞ,Γ|()x:RΞ|Γk A(g):ʃAʃintro2\frac{\Xi \vert \Gamma \vdash g:R \to \esh A \quad \Xi, \Gamma \vert () \vdash x:R}{\Xi \vert \Gamma \vdash k_A(g):\esh A}\esh-\mathrm{intro}2
Ξ|Γg:RʃAΞ,Γ|()x:RΞ|Γι A(g,x):g(x)= ʃAk A(g)ʃintro3\frac{\Xi \vert \Gamma \vdash g:R \to \esh A \quad \Xi, \Gamma \vert () \vdash x:R}{\Xi \vert \Gamma \vdash \iota_A(g, x):g(x) =_{\esh A} k_A(g)}\esh-\mathrm{intro}3
Ξ|Γg:RʃAΞ,Γ|()x:RΞ|Γk A(g):ʃAʃintro4\frac{\Xi \vert \Gamma \vdash g:R \to \esh A \quad \Xi, \Gamma \vert () \vdash x:R}{\Xi \vert \Gamma \vdash k_A'(g):\esh A}\esh-\mathrm{intro}4
Ξ|Γx:RΞ|Γι A(x):x= ʃAk A(const ʃA,R(x))ʃintro5\frac{\Xi \vert \Gamma \vdash x:R}{\Xi \vert \Gamma \vdash \iota_A'(x):x =_{\esh A} k_A'(\mathrm{const}_{\esh A, R}(x))}\esh-\mathrm{intro}5
  • Elimination rules for weak and strict shape types:
Ξ|ΓAtypeΞ|Γ,w:ʃAQtypeΞ|Γx:AΞ|Γd σ A(x):Q[σ A(x)/w]ʃelim1\frac{\Xi \vert \Gamma \vdash A \; \mathrm{type} \quad \Xi \vert \Gamma, w:\esh A \vdash Q \; \mathrm{type} \quad \Xi \vert \Gamma \vdash x:A}{\Xi \vert \Gamma \vdash d_{\sigma_A}(x):Q[\sigma_A(x)/w]}\esh-\mathrm{elim}1
Ξ|ΓAtypeΞ|Γ,w:ʃAQtypeΞ|Γg:RʃAΞ|Γx:RΞ|Γh:Q[g(x)/w]Ξ|Γd κ A(g,h):Q[κ A(g)/w]ʃelim2\frac{\Xi \vert \Gamma \vdash A \; \mathrm{type} \quad \Xi \vert \Gamma, w:\esh A \vdash Q \; \mathrm{type} \quad \Xi \vert \Gamma \vdash g:R \to \esh A \quad \Xi \vert \Gamma \vdash x:R \quad \Xi \vert \Gamma \vdash h:Q[g(x)/w]}{\Xi \vert \Gamma \vdash d_{\kappa_A}(g, h):Q[\kappa_A(g)/w]}\esh-\mathrm{elim}2
Ξ|ΓAtypeΞ|Γ,w:ʃAQtypeΞ|Γg:RʃAΞ|Γx:RΞ|Γh:Q[g(x)/w]Ξ|Γd ι A(g,x.h):h= Q[κ A(g)/w]d κ A(g,h)ʃelim3\frac{\Xi \vert \Gamma \vdash A \; \mathrm{type} \quad \Xi \vert \Gamma, w:\esh A \vdash Q \; \mathrm{type} \quad \Xi \vert \Gamma \vdash g:R \to \esh A \quad \Xi \vert \Gamma \vdash x:R \quad \Xi \vert \Gamma \vdash h:Q[g(x)/w]}{\Xi \vert \Gamma \vdash d_{\iota_A}(g, x.h):h =_{Q[\kappa_A(g)/w]} d_{\kappa_A}(g, h)}\esh-\mathrm{elim}3
Ξ|ΓAtypeΞ|Γ,w:ʃAQtypeΞ|Γg:RʃAΞ|Γx:RΞ|Γh:Q[g(x)/w]Ξ|Γd κ A(g,h):Q[κ A(g)/w]ʃelim4\frac{\Xi \vert \Gamma \vdash A \; \mathrm{type} \quad \Xi \vert \Gamma, w:\esh A \vdash Q \; \mathrm{type} \quad \Xi \vert \Gamma \vdash g:R \to \esh A \quad \Xi \vert \Gamma \vdash x:R \quad \Xi \vert \Gamma \vdash h:Q[g(x)/w]}{\Xi \vert \Gamma \vdash d_{\kappa_A'}(g, h):Q[\kappa_A'(g)/w]}\esh-\mathrm{elim}4
Ξ|ΓAtypeΞ|Γ,w:ʃAQtypeΞ|Γx:ʃAΞ|Γy:Q[x/w]Ξ|Γd ι A(y,x):y= Q[κ A(const ʃA,R(x))/w]d κ A(const ʃA,R(x),const ʃA,R(y))ʃelim5\frac{\Xi \vert \Gamma \vdash A \; \mathrm{type} \quad \Xi \vert \Gamma, w:\esh A \vdash Q \; \mathrm{type} \quad \Xi \vert \Gamma \vdash x:\esh A \quad \Xi \vert \Gamma \vdash y:Q[x/w]}{\Xi \vert \Gamma \vdash d_{\iota_A'}(y, x):y =_{Q[\kappa_A'(\mathrm{const}_{\esh A, R}(x))/w]} d_{\kappa_A'}(\mathrm{const}_{\esh A, R}(x), \mathrm{const}_{\esh A, R}(y))}\esh-\mathrm{elim}5
  • Computation rules for weak and strict shape types:
Ξ|ΓAtypeΞ|Γ,w:ʃAQtypeΞ|Γx:AΞ|Γ,y:ʃAf:QΞ|Γf[σ A(x)/y]d σ A(x):Q[σ A(x)/w]ʃcompstrict1\frac{\Xi \vert \Gamma \vdash A \; \mathrm{type} \quad \Xi \vert \Gamma, w:\esh A \vdash Q \; \mathrm{type} \quad \Xi \vert \Gamma \vdash x:A \quad \Xi \vert \Gamma, y:\esh A \vdash f:Q}{\Xi \vert \Gamma \vdash f[\sigma_A(x)/y] \equiv d_{\sigma_A}(x):Q[\sigma_A(x)/w]}\esh-\mathrm{comp}\mathrm{strict}1
Ξ|ΓAtypeΞ|Γ,w:ʃAQtypeΞ|Γx:AΞ|Γ,y:ʃAf:QΞ|Γβ ʃ 1(x):f[σ A(x)/y]= Q[σ A(x)/w]d σ A(x)ʃcompweak1\frac{\Xi \vert \Gamma \vdash A \; \mathrm{type} \quad \Xi \vert \Gamma, w:\esh A \vdash Q \; \mathrm{type} \quad \Xi \vert \Gamma \vdash x:A \quad \Xi \vert \Gamma, y:\esh A \vdash f:Q}{\Xi \vert \Gamma \vdash \beta_\esh^1(x):f[\sigma_A(x)/y] =_{Q[\sigma_A(x)/w]} d_{\sigma_A}(x)}\esh-\mathrm{comp}\mathrm{weak}1

The shape modality is an example of a higher inductive type which states that the shape modality of a type AA ʃ(A)\esh(A) is the localization L R 1(A)L_{R^1}(A) of AA at the function const:A(RA)\mathrm{const}:A \to (R \to A), equivalent to const:(1A)(RA)\mathrm{const}':(1 \to A) \to (R \to A). Weak shape modalities are primarily used in cohesive objective type theories, while strict shape modalities are typically used in cohesive type theories with judgmental equality, such as cohesive Martin-Löf type theory (cohesive homotopy type theory or cohesive higher observational type theory.


Preservation of some \infty-fiber products

The shape operation is defined to preserve finite homotopy products and small homotopy colimits (being a left adjoint) but it does not preserve general homotopy limits, not even all homotopy pullbacks:


(shape does not preserve homotopy fibers of points over positive-dimensional smooth spheres)
For n +n \in \mathbb{N}_+ consider the n n -sphere in its standard incarnation as a smooth manifold (or just as a D-topological space) and as such as a 0-truncated smooth \infty -groupoid

S smth nSmthMfdSmthGrpd . S^n_{smth} \,\in\, SmthMfd \hookrightarrow SmthGrpd_\infty \,.

This is such that the shape is the nn-sphere as a geometrically discrete higher homotopy type

ʃS smth nS nGrpd DiscSmthGrpd . \esh S^n_{smth} \,\simeq\, S^n \,\in\, Grpd_\infty \xhookrightarrow{Disc} SmthGrpd_{\infty}.

Now for x:*S smth nx \colon \ast \to S^n_{smth} any point (and using that ʃ*=*\esh \ast \,=\, \ast by the condition that ʃ\esh preserves finite products):

  1. its fiber product over S smth nS^n_{smth} may be computed in SmthMfd and hence is that same point:

  2. its homotopy fiber product over S n=ʃS smth nS^n = \esh S^n_{smth} is the loop space ΩS n\Omega S^n, which (under our assumption that nn is a positive number) is far from equivalent to the point (for example: ΩS 1\Omega S^1 \,\simeq\, \mathbb{Z}).


n +*ʃ(*×S smth n*)((ʃ*)×ʃS smth n(ʃ*))ΩS n. n \in \mathbb{N}_+ \;\;\;\; \vdash \;\;\;\; \ast \;\simeq\; \esh \big( \ast \underset {S^n_{smth}} {\times} \ast \big) \;\neq\; \big( (\esh\ast) \underset {\esh S^n_{smth}} {\times} (\esh\ast) \big) \;\simeq\; \Omega S^{n} \,.

However, the shape modality does preserve some useful classes of homotopy fiber products after all:



(cohesive shape preserves looping and delooping)

For H\mathbf{H} a cohesive \infty -topos and B𝒢H\mathbf{B}\mathcal{G} \,\in\, \mathbf{H} a pointed connected object, hence the delooping of an \infty -group 𝒢Grp(H)\mathcal{G} \,\in\, Grp(\mathbf{H}), the cohesive shape modality preserves the looping homotopy fiber product:

ʃ(*×B𝒢*)*×ʃB𝒢*. \esh \big( \ast \underset {\mathbf{B}\mathcal{G}}{\times} \ast \big) \;\; \simeq \;\; \ast \underset {\esh \mathbf{B}\mathcal{G}}{\times} \ast \,.


Since groupoid objects in an (∞,1)-topos are effective, the delooping of an \infty -group is the simplicial \infty -colimit of the simplicial object 𝒢 × \mathcal{G}^{\times^\bullet} of finite products of 𝒢\mathcal{G}. Since the shape operation preserves finite products and general colimits, it preserves the delooping:

ʃB𝒢ʃlimn𝒢 × nlimn(ʃ𝒢) × nBʃ𝒢. \esh \mathbf{B}\mathcal{G} \;\simeq\; \esh \underset{\underset{n \in \mathbb{N}}{\longrightarrow}} {\lim} \mathcal{G}^{\times^n} \;\simeq\; \underset{\underset{n \in \mathbb{N}}{\longrightarrow}} {\lim} \big( \esh \mathcal{G} \big)^{\times^n} \;\simeq\; \mathbf{B} \esh \mathcal{G} \,.

Finally, using again that groupoid objects in an (∞,1)-topos are effective, the claim follows:

ʃ(*×B𝒢*)ʃ𝒢ʃ(*×ʃB𝒢*). \esh \big( \ast \underset{\mathbf{B}\mathcal{G}}{\times} \ast \big) \;\simeq\; \esh \mathcal{G} \;\simeq\; \esh \big( \ast \underset{\esh\mathbf{B}\mathcal{G}}{\times} \ast \big) \,.


(cohesive shape preserves homotopy fiber products over discrete objects)
If H\mathbf{H} is a cohesive \infty -topos over Grpd Grpd_\infty , then its shape modality preserves homotopy fiber products over discrete objects.

The following argument follows dcct, Thm. 3.8.19, which in turn follows discussion with Mike Shulman. The diagram is taken from the writeup of the proof given in SS21, Prop. 3.38.

By a version of the \infty -Grothendieck construction (Beardsley & Péroux 2022, Lem. 3.10), a slice \infty -topos over the inverse image of a plain \infty -groupoid BB is equivalent to the \infty -category of \infty -functors BHB \to \mathbf{H}. This way, the BB-sliced adjunction ShpDscrShp \dashv Dscr is seen to be of the following form:

Now Fnctr(B,Shp)Fnctr(B,Shp) preserves binary products as soon as ShpShp does (because products of presheaves are computed objectwise). But binary products in the equivalent slice category H /B\mathbf{H}_{/B} are the homotopy fiber products in question, and hence the claim follows.


(shape preserves homotopy fibers of maps from discrete to delooped objects)
For H\mathbf{H} is a cohesive \infty -topos over Grpd Grpd_\infty the shape modality preserves the homotopy fibers of morphisms

f:XB𝒢 f \,\colon\, X \longrightarrow \mathbf{B}\mathcal{G}
  • from any discrete object XGrpd DscrHX \,\in\, Grpd_\infty \xhookrightarrow{Dscr} \mathbf{H}

  • to any delooped object B𝒢H\mathbf{B}\mathcal{G} \,\in\, \mathbf{H}

in that

ʃfib(f)fib(ʃf). \esh fib(f) \;\simeq\; fib\big( \esh f \big) \,.


Since a discrete \infty-groupoid XX is the coproduct of its connected components, and since coproducts are preserved by homotopy pullback (due to universal colimits in an \infty -topos) and by the shape modality (being a left adjoint), we may assume without restriction of generaliity that also XX is connected, hence XB𝒦X \,\simeq\,B \mathcal{K} with *B𝒦\ast \twoheadrightarrow B\mathcal{K} an effective epimorphism.

First, observe that the pasting law for homotopy pullbacks gives the pasting diagram of homotopy pullbacks shown on the left below:

𝒢 fib(f) * (pb) (pb) * B𝒦 f B𝒢ʃ𝒢 ʃfib(f) * (pb) (pb) * B𝒦 ʃf B𝒢. \array{ \mathcal{G} &\longrightarrow& fib(f) &\longrightarrow& \ast \\ \big\downarrow &{}^{{}_{(pb)}}& \big\downarrow &{}^{{}_{(pb)}}& \big\downarrow \\ \ast &\twoheadrightarrow& B\mathcal{K} &\underset{f}{\longrightarrow}& \mathbf{B}\mathcal{G} } \;\;\;\;\;\;\;\;\;\; \vdash \;\;\;\;\;\;\;\;\;\; \array{ \esh \mathcal{G} &\longrightarrow& \esh fib(f) &\longrightarrow& \ast \\ \big\downarrow &{}^{{}_{(pb)}}& \big\downarrow &{}^{{}_{(pb)}}& \big\downarrow \\ \ast &\twoheadrightarrow& B\mathcal{K} &\underset{\esh f}{\longrightarrow}& B\mathcal{G} \mathrlap{\,.} }

Now, as shown on the right, the shape modality

  1. preserves the left pullback square and its bottom effective epimorphism, by Prop. ;

  2. preserves the outer pullback rectangle by Prop. .

Therefore also the square on the far right is homotopy Cartesian, by the “reverse pasting law” (this Prop.). But this is equivalently the claim to be shown.

More specific cases

The following discussion is about the topological/smooth shape modality commuting with looping (homotopy fiber products of points) of mapping stacks between delooping stacks of certain topological groups. This is a technical point of crucial importance in the construction and discussion of equivariant classifying spaces for equivariant principal bundles – though not traditionally presented as being about behaviour under a shape modality. The following perspective is from SS21, though the hard results themselves are either classical (essentially Conner & Floyd 1964, Lemma 31.8 for the case of compact Γ\Gamma) or, in more generality, due to Uribe & Lück 2014. (Beware that the following differs from their notation by the exchange “GG\leftrightarrowΓ\Gamma”! For us here, GG denotes the equivariance group and Γ\Gamma the structure group.)


(Condition H on families of topological group homomorphisms)
Let G,ΓGrp(kTop)G, \Gamma \,\in\, Grp(kTop) be topological groups and let

HGHom(H,Γ) \mathcal{R} \,\subset\, \underset{ H \subset G }{\coprod} Hom(H,\Gamma)

be a set of pairs (H,ρ)(H,\rho) consisting of a topological subgroup HH of GG and a continuous homomorphism HΓH \to \Gamma such that (Uribe & Lück 2014, Def. 3.4) \mathcal{R} is closed under:

  1. fiber products, i.e. under products in Grp(kTop) /ΓGrp(kTop)_{/\Gamma},

  2. conjugation by Γ\Gamma (under postcomposition),

  3. conjugation by GG (under precomposition).

We say (with Uribe & Lück 2014, Def. 6.1) that such data satisfies Condition H if for all (H,ρ)(H, \rho) \,\in\, \mathcal{R} we have:

  1. the path component of ρ\rho in HomMap(H,Γ)HomMap(H,\Gamma) is contained in its orbit under the Γ\Gamma-conjugation action:

    HomMap(H,Γ) ρΓ(ρ){Ad γρ|γΓ} HomMap(H,\Gamma)_{\rho} \;\; \subset \;\; \Gamma(\rho) \;\coloneqq\; \big\{ Ad_\gamma \circ \rho \;\big\vert\; \gamma \in \Gamma \big\}
  2. the coset space-coprojections

    1. GG/HG \longrightarrow G/H

    2. ΓΓ/Stab Γ(ρ)\Gamma \longrightarrow \Gamma/Stab_\Gamma(\rho)

      (by the the stabilizer subgroup Stab Γ(ρ)ΓStab_{\Gamma}(\rho) \subset \Gamma under the conjugation action)

    admit local sections.

  3. the map

    Γ/Stab Γ(ρ) HomMap(H,Γ) [γ] Ad γρ \array{ \Gamma/Stab_\Gamma(\rho) &\longrightarrow& HomMap(H,\Gamma) \\ [\gamma] &\mapsto& Ad_\gamma \circ \rho }

    is a homeomorphism onto its image.


Examples of families of topological group homomorphisms satsifying Condition H (Def. ) include the following:

  1. Γ\Gamma and GG any Lie groups with Γ\Gamma almost connected

    with \mathcal{R} consisting of all compact subsgroups HGH \subset G and all their homomorphisms HΓH \to \Gamma

    (established in Uribe & Lück 2014, Thm. 6.3)

  2. Γ=\Gamma = PU(ℋ) and GG any finite group

    with \mathcal{R} consisting of all subgroups HGH \subset G and all their homomorphisms HPU()H \to PU(\mathcal{H})

    (established in Uribe & Lück 2014, Sec. 15)

For the following formulation of the main result of Uribe & Lück 2014 in terms of cohesive homotopy theory we use the continuous diffeology

kTopCDfflgDiffSpSmthGrp kTop \xrightarrow{CDfflg} DiffSp \hookrightarrow SmthGrp_\infty

and the fact that this preserves shapes and shapes of mapping spaces (see the introduction of SS21).


(shape commutes with looping of mapping stacks between delooping stacks of certain pairs of topological groups)

we have for all homomorphisms ρ:HΓ\rho \,\colon\, H \to \Gamma from subgroups HGH \subset G that the shape modality commutes with the looping-operation on the mapping stack between the deloopings of HH and Γ\Gamma in SmoothGrpd SmoothGrpd_{\infty} :

ʃΩ ρMap(BH,BΓ)Ω ρʃMap(BH,BΓ). \esh \Omega_\rho Map \big( \mathbf{B}H ,\, \mathbf{B}\Gamma \big) \;\; \simeq \;\; \Omega_\rho \esh Map \big( \mathbf{B}H ,\, \mathbf{B}\Gamma \big) \,.


First notice (e.g. from the discussion at stabilizer subgroup, here) that

(1)Stab Γ(ρ)Ω ρMap(BH,BΓ) Stab_\Gamma(\rho) \;\simeq\; \Omega_\rho Map \big( \mathbf{B}H ,\, \mathbf{B}\Gamma \big)

From the discussion at equivariant principal bundles we have, under the given assumptions, that

B GΓ:G/HʃMap(BH,BΓ) B_G \Gamma \;\;\; \colon \;\;\; G/H \;\mapsto\; \esh \, Map \big( \mathbf{B}H ,\, \mathbf{B}\Gamma \big)

is the GG-equivariant homotopy type of the GG-equivariant classifying space of Γ\Gamma.

(For Γ\Gamma compact Lie this is the Murayama-Shimakawa result as reviewed in Guillou, May & Merling 2017, Thm. 3.1, while for Γ=PU()\Gamma = PU(\mathcal{H}) this is due to Bárcenas, Espinoza, Joachim & Uribe 2012, with a re-derivation in a more explicitly cohesive context in SS21).

Moreover, by Exp. both cases satisfy Condition H (Def. ), whence the main result Uribe & Lück 2014, Sec. 13 applies, which, using the above identification of the equivariant classifying space, gives a weak homotopy equivalence of the form

[ρ]Hom(H,Γ)/ΓBStab Γ(ρ)ʃMap(BH,BΓ). \underset{ { [\rho] \in } \atop { Hom(H,\Gamma)/\Gamma } }{\coprod} B Stab_\Gamma(\rho) \;\;\; \simeq \;\;\; \esh Map \big( \mathbf{B}H ,\, \mathbf{B}\Gamma \big) \,.

(For Γ\Gamma a Lie group this is the classical fact that nearby homomorphisms from compact Lie groups are conjugate.)

Observing that BStab Γ(ρ)BʃStab Γ(ρ)B Stab_\Gamma(\rho) \,\simeq\, \mathbf{B} \esh Stab_\Gamma(\rho), the looping of this equivalence at the basepoint given by ρ\rho yields the claim.

Relative shape and factorization system

Generally, given an (∞,1)-topos H\mathbf{H} (or just a 1-topos) equipped with an idempotent monad ʃ:HH\esh \colon \mathbf{H} \to \mathbf{H} (a (higher) modality/closure operator) which preserves (∞,1)-pullbacks over objects in its essential image, one may call a morphism f:XYf \colon X \to Y in H\mathbf{H} ʃ\esh-closed if the unit-diagram

X η X ʃ(X) f ʃ(f) Y η Y ʃ(Y) \array{ X &\overset{\eta_X}{\longrightarrow}& \esh(X) \\ \big\downarrow {\mathrlap{{}^f}} && \big\downarrow{\mathrlap{{}^{\esh(f)}}} \\ Y & \overset{\eta_Y}{\longrightarrow} & \esh(Y) }

is an (∞,1)-pullback diagram. These ʃ\esh-closed morphisms form the right half of an orthogonal factorization system, the left half being the morphisms that are sent to equivalences in H\mathbf{H}.


Let (ΠDiscΓ):HGrpd(\Pi\dashv \Disc\dashv \Gamma):H\to\infty\Grpd be an infinity-connected (infinity,1)-topos, let ʃ:=DiscΠ\esh:=\Disc \Pi be the geometric path functor / geometric homotopy functor, let f:XYf:X\to Y be a HH-morphism, let c ʃfc_{\esh} f denote the ∞-pullback

c ʃf ʃX ʃ f Y 1 (ΠDisc) ʃY \array{ c_{\esh} f &\longrightarrow& {\esh} X \\ \big\downarrow && \big\downarrow^{\mathrlap{{\esh}_f}} \\ Y &\xrightarrow{1_{(\Pi\dashv \Disc)}} & {\esh}Y }

c ʃfc_{\esh} f is called ʃ\esh-closure of ff.

ff is called ʃ\esh-closed if Xc ʃfX\simeq c_{\esh}f.

If a morphism f:XYf:X\to Y factors into f=ghf=g\circ h and hh is a ʃ\esh-equivalence then gg is ʃ\esh-closed; this is seen by using that ʃ\esh is idempotent.

Π\Pi-closed morphisms are a right class of an orthogonal factorization system (in an (∞,1)-category) and hence, as discussed there, are closed under limits, composition, retracts and satisfy the left cancellation property.


(shape-modal maps as open maps)
A consequence of the previous property is that the class of ʃ\esh-closed morphisms gives rise to an admissible structure in the sense of structured spaces on an (∞,1)-connected (∞,1)-topos, hence they serve as a class of a kind of open maps.

Shape via cohesive path ∞-groupoid

See at shape via cohesive path ∞-groupoid.


Internal locally constant \infty-stacks

In a cohesive (∞,1)-topos H\mathbf{H} with an ∞-cohesive site of definition, the fundamental ∞-groupoid-functor ʃ\esh satisfies the above assumptions (this is the example gives this entry its name). The ʃ\esh-closed morphisms into some XHX \in \mathbf{H} are canonically identified with the locally constant ∞-stacks over XX. The correspondence is effectively what is called categorical Galois theory.


Let HH be a cohesive (∞,1)-topos possessing a ∞-cohesive site of definition. Then for XHX\in H the locally constant ∞-stacks ELConst(X)E\in \L\Const(X), regarded as ∞-bundle morphisms p:EXp:E\to X are precisely the ʃ\esh-closed morphisms into XX

Formally étale morphisms

If a differential cohesive (∞,1)-topos H th\mathbf{H}_{th}, the de Rham space functor \Im satisfies the above assumptions. The \Im-closed morphisms are precisely the formally étale morphisms.


infinitesimal cohesion

tangent cohesion

differential cohesion

graded differential cohesion

singular cohesion

id id fermionic bosonic bosonic Rh rheonomic reduced infinitesimal infinitesimal & étale cohesive ʃ discrete discrete continuous * \array{ && id &\dashv& id \\ && \vee && \vee \\ &\stackrel{fermionic}{}& \rightrightarrows &\dashv& \rightsquigarrow & \stackrel{bosonic}{} \\ && \bot && \bot \\ &\stackrel{bosonic}{} & \rightsquigarrow &\dashv& \mathrm{R}\!\!\mathrm{h} & \stackrel{rheonomic}{} \\ && \vee && \vee \\ &\stackrel{reduced}{} & \Re &\dashv& \Im & \stackrel{infinitesimal}{} \\ && \bot && \bot \\ &\stackrel{infinitesimal}{}& \Im &\dashv& \& & \stackrel{\text{étale}}{} \\ && \vee && \vee \\ &\stackrel{cohesive}{}& \esh &\dashv& \flat & \stackrel{discrete}{} \\ && \bot && \bot \\ &\stackrel{discrete}{}& \flat &\dashv& \sharp & \stackrel{continuous}{} \\ && \vee && \vee \\ && \emptyset &\dashv& \ast }



Original discussion:

In Smooth∞Grpd

For the case of Smooth∞Grpd:

On shape via cohesive path ∞-groupoids:

Discussion for orbifolds, étale groupoids and, generally, étale ∞-groupoids:

Last revised on November 4, 2023 at 08:44:01. See the history of this page for a list of all contributions to it.