Spahn internal formulation of cohesion (Rev #1)

category: cohesion

The axioms

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

Subtopos

Reflective subfibration

github

Stable factorization system

github

Lex-reflective subcategory

github

Lex-reflective subcategory of codiscrete objects

github

Local topos

github

Cohesive topos

github

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