Spahn internal formulation of cohesion (Rev #10)

category: cohesion

For generalities on the translation Ho CT-Ho TT see dictionary HoCT-HoTT.

For generalities on the formulation of Ho TT in Coq see HoTT-Coq - references.

For generalities on cohesive toposes see Urs Schreiber, differential cohomology in a cohesive topos

For a blog comment on the internal formulation of cohesion, see Mike Shulman

  • internalizing the external - the joy of codiscreteness, ncafé

  • discreteness, concreteness, fibrations, and scones, ncafé

Notation

We assume that

(ΠDiscΓcoDisc):GrpdcoDiscH(\Pi\dashv Disc\dashv \Gamma\dashv co Disc):\infty Grpd\stackrel{co Disc}{\hookrightarrow}H

is an adjoint quadruple, where we assume that Π\Pi preserves finite products and DiscDisc and coDiscco Disc are full and faithful.

This adjoint quadruple gives rise to an adjoint triple

(Π):=(DiscΠDiscΓcoDiscΓ):HH(\mathbf{\Pi}\dashv \flat\dashv\sharp):=(Disc \Pi \dashv Disc \Gamma\dashv co Disc \Gamma):H\to H

The Ho CT-axioms of cohesion

theorem

For Disc:BHDisc : \mathbf{B} \hookrightarrow \mathbf{H} a sub-(∞,1)-category, the inclusion extends to an adjoint quadruple of the form

HcoDiscΓDiscΠB \mathbf{H} \stackrel{\overset{\Pi}{\to}}{\stackrel{\overset{Disc}{\hookleftarrow}}{\stackrel{\overset{\Gamma}{\to}}{\underset{coDisc}{\hookleftarrow}}}} \mathbf{B}

precisely if there exists for each object XHX \in \mathbf{H}

  1. a morphism XΠ(X)X \to \mathbf{\Pi}(X) with Π(X)BDiscH\mathbf{\Pi}(X) \in \mathbf{B} \stackrel{Disc}{\hookrightarrow} \mathbf{H};

  2. a morphism XX\mathbf{\flat} X \to X with XBDiscH\mathbf{\flat} X \in \mathbf{B} \stackrel{Disc}{\hookrightarrow} \mathbf{H};

  3. a morphism X#XX \to #X with #XBcoDiscH# X \in \mathbf{B} \stackrel{coDisc}{\hookrightarrow} \mathbf{H}

such that for all YBDiscHY \in \mathbf{B} \stackrel{Disc}{\hookrightarrow} \mathbf{H} and Y˜BcoDiscH\tilde Y \in \mathbf{B} \stackrel{coDisc}{\hookrightarrow} \mathbf{H} the induced morphisms

  1. H(ΠX,Y)H(X,Y)\mathbf{H}(\mathbf{\Pi}X , Y) \stackrel{\simeq}{\to} \mathbf{H}(X,Y);

  2. H(Y,X)H(Y,X)\mathbf{H}(Y, \mathbf{\flat}X) \stackrel{\simeq}{\to} \mathbf{H}(Y,X);

  3. H(#X,Y˜)H(X,Y˜)\mathbf{H}(# X , \tilde Y) \stackrel{\simeq}{\to} \mathbf{H}(X,\tilde Y);

  4. #(XX)# (\flat X \to X);

  5. (X#X)\flat (X \to # X)

are equivalences (the first three of ∞-groupoids the last two in H\mathbf{H}).

Moreover, if H\mathbf{H} is a cartesian closed category, then Π\Pi preserves finite products precisely if the DiscDisc-inclusion is an exponential ideal.

The last statement follows from the (,1)(\infty,1)-category analog of the discussion here.

Coq

This section is on the Coq formalization of axiomatic homotopy cohesion. It draws from Mike Shulman, Internalizing the external, or The Joys of Codiscreteness (blog post). The corresponding Coq-code library is at Mike Shulman, HoTT/Coq/Subcatgeories

Subtopos

Reflective subfibration

This section comments on the code ReflectiveSubfibration.v.

It codes the axiom that

(ΓcoDisc):GrpdH(\Gamma\dashv \co Disc):\infty Grpd\to H

exhibits the codiscrete objects as reflective subcategory of HH.

For plain types

The following axioms characterize in type theoretical language the relations between objects of a reflective subcategory by means of the endofunctor

=coDiscΓ:HH\sharp= co Disc \Gamma: H\to H
  1. A:TypeinRsc(A):Prop.A:Type\vdash in Rsc(A):Prop. This says that for any type AA, we have a proposition inRsc(A)in Rsc(A) (expressing the assertion that AA is in our putative reflective subcategory).

  2. A:TypeA:Type.A:Type\dashv \sharp A:Type. This says that for any AA, we have another type A\sharp A (its reflection into the subcategory).

  3. A:TypeinRsc(A).A:Type\dashv in Rsc(\sharp A). This says that for any AA, the type A\sharp A is in the subcategory.

  4. A:Typeη A:AAA:Type\dashv \eta_A:A\to \sharp A. This says that for any AA, we have a map η A:AA\eta_A:A\to \sharp A (which we can think of as the unit of the adjunction).

  5. A,B:Type,inRsc(B)isEquiv(λg.gη A)A,B:Type,inRsc(B)\dashv is Equiv(\lambda g.g\circ\eta_A). This says that for any types A and B, where B is in the subcategory, precomposing with η A\eta_A yields an equivalence between B AB^{\sharp A} and B AB^A (which we can think of as the adjunction isomorphism since precomposition ggη Ag\mapsto g\circ \eta_A with the adjunction-unit assigns the adjunct).

For dependent types

The previous axioms are given for plain types but one can impose them also on dependent types x:AP(x):Typex:A\dashv P(x):Type in that we require

x:AP(x):Type.x:A \dashv \sharp P(x):Type.

In category theory this means that

P(x) P * x A\array{ \sharp P(x)&\rightarrow &\sharp P \\ \downarrow&&\downarrow \\ *&\xrightarrow{x}&A }

is a pullback and the right arrow is a fibration. The operation \sharp commutes with pullbacks and gives an operation on every overcategory H/AH/A . There are axioms expressing the requirement that \sharp is a reflection.

Relation to factorization systems

(1) The following statements are equivalent:

  • (E,M)(E,M) is a reflective factorization system.

  • There is a reflective subcategory CHC\hookrightarrow H with reflector \sharp, EE is the class of morphisms whose \sharp-image is invertible in CC, and C=M/1C=M/1.

  • (E,M)(E,M) is a factorization system and EE satisfies 2-out -of-3.

(2) The following statements are equivalent:

  • (E,M)(E,M) is a factorization system in HH.

  • The class (E,M) ×:={M/x|xH,M/xH/xisreflective,fact.refl}(E,M)^\times:=\{M/x|x\in H,\M/x\hookrightarrow H/x\,is\,reflective,\,fact.refl\} is pullback-stable where fact.reflfact.refl means that each reflection is given by (E,M)(E,M)-factorization.

Here

Stable factorization system

github

Lex-reflective subcategory

Theorem

Let CC be a ccc. Let ICI\hookrightarrow C be a reflective subcategory.

Then II is an exponential ideal iff the reflector preserves finite products.

github

Lex-reflective subcategory of codiscrete objects

github

Local topos

HH being local means that we have a geometric morphism with extra right adjoint

github

Cohesive topos

(Discrete objects are reflectively- and coreflectively embedded.)

github

References

  • Mike Shulman, Discreteness, Concreteness, Fibrations, and Scones, blog

  • Mike Shulman, Internalizing the External, or The Joys of Codiscreteness, blog

  • Mike Shulman, Reflective Subfibrations, Factorization Systems, and Stable Units, blog

Revision on November 29, 2012 at 18:44:20 by Stephan Alexander Spahn?. See the history of this page for a list of all contributions to it.