Backround
Definition
Presentation over a site
Models
natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
In a locally ∞-connected (∞,1)-topos with fully faithful inverse image (such as a cohesive (∞,1)-topos), the extra left adjoint to the inverse image of the global sections geometric morphism induces a higher modality , 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 may be thought of as the shape of and therefore one may call the shape modality. It forms an adjoint modality with the flat modality .
We assume a dependent type theory with crisp term judgments in addition to the usual (cohesive) type and term judgments and , as well as context judgments where is a list of crisp term judgments, and is a list of cohesive term judgments. A crisp type is a type in the context , 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 such that given any crisp type , is discrete if and only if the function 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:
…
The shape modality is an example of a higher inductive type which states that the shape modality of a type is the localization of at the function , equivalent to . 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.
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 consider the -sphere in its standard incarnation as a smooth manifold (or just as a D-topological space) and as such as a 0-truncated smooth -groupoid
This is such that the shape is the -sphere as a geometrically discrete higher homotopy type
Now for any point (and using that by the condition that preserves finite products):
its fiber product over may be computed in SmthMfd and hence is that same point:
its homotopy fiber product over is the loop space , which (under our assumption that is a positive number) is far from equivalent to the point (for example: ).
Hence
However, the shape modality does preserve some useful classes of homotopy fiber products after all:
(cohesive shape preserves looping and delooping)
For a cohesive -topos and a pointed connected object, hence the delooping of an -group , the cohesive shape modality preserves the looping homotopy fiber product:
Since groupoid objects in an (∞,1)-topos are effective, the delooping of an -group is the simplicial -colimit of the simplicial object of finite products of . Since the shape operation preserves finite products and general colimits, it preserves the delooping:
Finally, using again that groupoid objects in an (∞,1)-topos are effective, the claim follows:
(cohesive shape preserves homotopy fiber products over discrete objects)
If is a cohesive -topos
over , then its shape modality preserves homotopy fiber products over discrete objects.
By a version of the -Grothendieck construction (Beardsley & Péroux 2022, Lem. 3.10), a slice -topos over the inverse image of a plain -groupoid is equivalent to the -category of -functors . This way, the -sliced adjunction is seen to be of the following form:
Now preserves binary products as soon as does (because products of presheaves are computed objectwise). But binary products in the equivalent slice category are the homotopy fiber products in question, and hence the claim follows.
(shape preserves homotopy fibers of maps from discrete to delooped objects)
For is a cohesive -topos
over the shape modality preserves the homotopy fibers of morphisms
from any discrete object
to any delooped object
in that
Since a discrete -groupoid is the coproduct of its connected components, and since coproducts are preserved by homotopy pullback (due to universal colimits in an -topos) and by the shape modality (being a left adjoint), we may assume without restriction of generaliity that also is connected, hence with an effective epimorphism.
First, observe that the pasting law for homotopy pullbacks gives the pasting diagram of homotopy pullbacks shown on the left below:
Now, as shown on the right, the shape modality
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.
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 ) or, in more generality, due to Uribe & Lück 2014. (Beware that the following differs from their notation by the exchange “” “”! For us here, denotes the equivariance group and the structure group.)
(Condition H on families of topological group homomorphisms)
Let be topological groups and let
be a set of pairs consisting of a topological subgroup of and a continuous homomorphism such that (Uribe & Lück 2014, Def. 3.4) is closed under:
fiber products, i.e. under products in ,
conjugation by (under postcomposition),
conjugation by (under precomposition).
We say (with Uribe & Lück 2014, Def. 6.1) that such data satisfies Condition H if for all we have:
the path component of in is contained in its orbit under the -conjugation action:
(by the the stabilizer subgroup under the conjugation action)
the map
is a homeomorphism onto its image.
Examples of families of topological group homomorphisms satsifying Condition H (Def. ) include the following:
and any Lie groups with almost connected
with consisting of all compact subsgroups and all their homomorphisms
(established in Uribe & Lück 2014, Thm. 6.3)
PU(ℋ) and any finite group
with consisting of all subgroups and all their homomorphisms
(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
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)
For
a compact Lie group or PU(ℋ),
we have for all homomorphisms from subgroups that the shape modality commutes with the looping-operation on the mapping stack between the deloopings of and in :
First notice (e.g. from the discussion at stabilizer subgroup, here) that
From the discussion at equivariant principal bundles we have, under the given assumptions, that
is the -equivariant homotopy type of the -equivariant classifying space of .
(For compact Lie this is the Murayama-Shimakawa result as reviewed in Guillou, May & Merling 2017, Thm. 3.1, while for 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
(For a Lie group this is the classical fact that nearby homomorphisms from compact Lie groups are conjugate.)
Observing that , the looping of this equivalence at the basepoint given by yields the claim.
Generally, given an (∞,1)-topos (or just a 1-topos) equipped with an idempotent monad (a (higher) modality/closure operator) which preserves (∞,1)-pullbacks over objects in its essential image, one may call a morphism in -closed if the unit-diagram
is an (∞,1)-pullback diagram. These -closed morphisms form the right half of an orthogonal factorization system, the left half being the morphisms that are sent to equivalences in .
Let be an infinity-connected (infinity,1)-topos, let be the geometric path functor / geometric homotopy functor, let be a -morphism, let denote the ∞-pullback
is called -closure of .
is called -closed if .
If a morphism factors into and is a -equivalence then is -closed; this is seen by using that is idempotent.
-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 -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.
See at shape via cohesive path ∞-groupoid.
In a cohesive (∞,1)-topos with an ∞-cohesive site of definition, the fundamental ∞-groupoid-functor satisfies the above assumptions (this is the example gives this entry its name). The -closed morphisms into some are canonically identified with the locally constant ∞-stacks over . The correspondence is effectively what is called categorical Galois theory.
Let be a cohesive (∞,1)-topos possessing a ∞-cohesive site of definition. Then for the locally constant ∞-stacks , regarded as ∞-bundle morphisms are precisely the -closed morphisms into
If a differential cohesive (∞,1)-topos , the de Rham space functor satisfies the above assumptions. The -closed morphisms are precisely the formally étale morphisms.
Original discussion:
Urs Schreiber, Zoran Škoda: §7.4.2 of: Categorified symmetries [arXiv:1004.2472]
Urs Schreiber, Sec. 3.4.5 in: differential cohomology in a cohesive topos (arXiv:1310.7930)
Mike Shulman, Sec. 9.7 in: Brouwer’s fixed-point theorem in real-cohesive homotopy type theory, Mathematical Structures in Computer Science Vol 28 (6) (2018): 856-941 (arXiv:1509.07584, doi:10.1017/S0960129517000147)
For the case of Smooth∞Grpd:
On shape via cohesive path ∞-groupoids:
Dmitri Pavlov, Structured Brown representability via concordance, 2014 (pdf, pdf)
Daniel Berwick-Evans, Pedro Boavida de Brito, Dmitri Pavlov, Classifying spaces of infinity-sheaves (arXiv:1912.10544)
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.