Documentation

Orbifolds.Cohesive.CohesiveSite

Cohesive sites #

Cohesive sites are sites with a number of useful properties that make their sheaf topos into a cohesive topos. See https://ncatlab.org/nlab/show/cohesive+site.

Every cohesive site is in particular local and locally connected, and every cosifted category with a terminal object that admits morphisms to every object is cohesive when equipped with the trivial topology.

TODO: generalise universe levels from max u v to max u v w again once that is possible.

A cohesive site is a cosifted locally connected site with a terminal object that admits morphisms to every other object. This guarantees that the sheaf topos is a cohesive topos.

Instances

    Every cohesive site is in particular a local site.

    Every cosifted category with a terminal object that admits morphisms to every other object becomes a cohesive site when equipped with the trivial topology.

    The cohesive structure of the sheaf topos on a cohesive site.

    Equations
    • One or more equations did not get rendered due to their size.
    theorem CategoryTheory.Cohesive.Sheaf.discToCodisc_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.IsCohesiveSite] [HasWeakSheafify J (Type (max u v))] {X : Type (max u v)} :
    (discToCodisc (Sheaf J (Type (max u v))) (Type (max u v))).app X = { val := CategoryStruct.comp (inv (toSheafify J ((Functor.const Cᵒᵖ).obj X))) { app := fun (Y : Cᵒᵖ) (x : ((Functor.const Cᵒᵖ).obj X).obj Y) (y : Opposite.unop (((coyoneda.obj (Opposite.op (⊤_ C))).comp uliftFunctor.{max u v, v}).op.obj Y)) => { down := x }, naturality := } }

    In sheaf topoi on cohesive sites, pieces have points in the sense that the components of the canonical points-to-pieces transformation Γ ⟶ π₀ are epic.