Locally connected sites

Locally connected sites are sites for which all covering sieves are connected as subcategories of the corresponding slice category. This is useful because it guarantees the existence of a further left adjoint π₀ of the constant sheaf functor, making sheaf topoi on locally connected sites locally connected.

See https://ncatlab.org/nlab/show/locally+connected+site.

Main definitions / results

• J.IsLocallyConnectedSite: typeclass stating that (C,J) is locally connected.
• Every trivial site is locally connected.
• isSheaf_const_obj: on locally connected sites, every constant presheaf is a sheaf.
• Sheaf.π₀ J: the connected components functor on locally connected sites, sending each sheaf to the colimit of its underlying presheaf.
• π₀ConstantSheafAdj: the adjunction between π₀ J and the constant sheaf functor. This shows that sheaf topoi on locally connected sites are locally connected.
• uniqueπ₀Obj_of_isRepresentable: π₀ sends representable sheaves to singleton types, i.e. all representable sheaves are connected.
• On locally connected sites with a terminal object, π₀ preserves the terminal object, i.e. the terminal sheaf is connected. This is enough to show that the sheaf topos is connected.
• On cosifted locally connected sites, π₀ preserves all finite products, i.e. the sheaf topos is strongly connected. This is not yet sorry-free because it depends on a characterisation of sifted categories.

class CategoryTheory.GrothendieckTopology.IsLocallyConnectedSite {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) : Prop

A locally connected site is a site with the property that every covering sieve is connected as a full subcategory of the corresponding slice category. In particular, every covering sieve is nonempty.

• isConnected_of_mem {X : C} (S : Sieve X) : S ∈ J X → IsConnected S.arrows.category

  Every covering sieve S ∈ J X is connected when interpreted as a full subcategory of the slice category Over X.

instance CategoryTheory.instNonemptyOfHasTerminal_orbifolds {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] : Nonempty C

Every category with a terminal object is nonempty. TODO: add a similar instance for HasInitial and move both to another file.

instance CategoryTheory.isConnected_of_hasTerminal {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] : IsConnected C

Every category with a terminal object is connected. TODO: add a similar instance for HasInitial and move both to another file.

instance CategoryTheory.instIsLocallyConnectedSiteTrivial {C : Type u} [Category.{v, u} C] : (GrothendieckTopology.trivial C).IsLocallyConnectedSite

Every category becomes a locally connected site with the trivial topology.

theorem CategoryTheory.isSheaf_const_obj {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.IsLocallyConnectedSite] {X : Type w} : Presheaf.IsSheaf J ((Functor.const Cᵒᵖ).obj X)

On locally connected sites, every constant presheaf is a sheaf.

instance CategoryTheory.instIsIsoFunctorOppositeTypeToSheafifyObjConst_orbifolds {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.IsLocallyConnectedSite] {X : Type w} [HasWeakSheafify J (Type w)] : IsIso (toSheafify J ((Functor.const Cᵒᵖ).obj X))

For constant presheaves on locally connected sites, toSheafify is an isomorphism. TODO: remove HasSheafify instance.

noncomputable def CategoryTheory.Sheaf.π₀ {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) : Functor (Sheaf J (Type (max u w))) (Type (max u w))

The connected components functor on sheaves of types on any local site, defined as taking colimits of the underlying presheaves.

Equations

• CategoryTheory.Sheaf.π₀ J = (CategoryTheory.sheafToPresheaf J (Type (max ?u.27 ?u.25))).comp CategoryTheory.Limits.colim

noncomputable def CategoryTheory.π₀ConstantSheafAdj {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.IsLocallyConnectedSite] [HasWeakSheafify J (Type (max u w))] : Sheaf.π₀ J ⊣ constantSheaf J (Type (max u w))

The connected components functor on local sites is left-adjoint to the constant sheaf functor. TODO: remove HasSheafify instance.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Limits.IsTerminal.isTerminalObj_functor {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasLimits D] {F : Functor C D} (hF : IsTerminal F) (X : C) : IsTerminal (F.obj X)

Evaluating a terminal functor yields terminal objects. TODO: move somewhere else

Equations

• hF.isTerminalObj_functor X = CategoryTheory.Limits.IsTerminal.isTerminalObj ((CategoryTheory.evaluation C D).obj X) F hF

noncomputable def CategoryTheory.Limits.IsTerminal.isTerminalSheafVal {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u₂} [Category.{v₂, u₂} A] [HasLimits A] {X : Sheaf J A} (hX : IsTerminal X) : IsTerminal X.val

A terminal sheaf is also terminal as a presheaf.

Equations

• hX.isTerminalSheafVal = CategoryTheory.Limits.IsTerminal.isTerminalObj (CategoryTheory.sheafToPresheaf J A) X hX

noncomputable def CategoryTheory.Limits.IsTerminal.isTerminalSheafValObj {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u₂} [Category.{v₂, u₂} A] [HasLimits A] {X : Sheaf J A} (hX : IsTerminal X) (Y : Cᵒᵖ) : IsTerminal (X.val.obj Y)

Sections of a terminal sheaf are terminal objects.

Equations

• hX.isTerminalSheafValObj Y = hX.isTerminalSheafVal.isTerminalObj_functor Y

noncomputable instance CategoryTheory.Sheaf.instUniqueTerminalValObjForget {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u₂} [Category.{v₂, u₂} A] [Limits.HasLimits A] [HasForget A] [Limits.PreservesLimit (Functor.empty A) (forget A)] (Y : Cᵒᵖ) : Unique ((forget A).obj ((⊤_ Sheaf J A).val.obj Y))

For sheaves valued in a concrete category whose terminal object is a point, sections of the terminal sheaf are unique.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Limits.IsTerminal.unique {X : Type u} (h : IsTerminal X) : Unique X

Terminal types are singletons.

Equations

• h.unique = (CategoryTheory.Limits.Types.isTerminalEquivUnique X) h

noncomputable instance CategoryTheory.Sheaf.instUniqueTerminalValObj {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Y : Cᵒᵖ) : Unique ((⊤_ Sheaf J (Type w)).val.obj Y)

Sections of the terminal sheaf are unique.

Equations

• CategoryTheory.Sheaf.instUniqueTerminalValObj Y = (CategoryTheory.Limits.terminalIsTerminal.isTerminalSheafValObj Y).unique

noncomputable def CategoryTheory.Limits.IsTerminal.uniqueHom {C : Type u} [Category.{v, u} C] {T : C} (hT : IsTerminal T) (X : C) : Unique (X ⟶ T)

Morphisms to a terminal object are unique.

Equations

• hT.uniqueHom X = { default := hT.from X, uniq := ⋯ }

noncomputable def CategoryTheory.Limits.IsTerminal.representableBy_isTerminal {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} (hF : IsTerminal F) {T : C} (hT : IsTerminal T) : F.RepresentableBy T

Terminal functors are represented by any terminal object.

Equations

• hF.representableBy_isTerminal hT = { homEquiv := fun {x : C} => Equiv.ofUnique (x ⟶ T) (F.obj (Opposite.op x)), homEquiv_comp := ⋯ }

instance CategoryTheory.instIsRepresentableTerminalFunctorOppositeTypeOfHasTerminal_orbifolds {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] : (⊤_ Functor Cᵒᵖ (Type w)).IsRepresentable

On categories with a terminal object, the terminal presheaf is representable.

instance CategoryTheory.Sheaf.isRepresentable_terminal {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] {J : GrothendieckTopology C} : (⊤_ Sheaf J (Type w)).val.IsRepresentable

On sites with a terminal object, the terminal sheaf is representable.

noncomputable def CategoryTheory.unique_colimit_representable {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type (max u w))) [F.IsRepresentable] : Unique (Limits.colimit F)

The colimit of any representable functor is a singleton type.

Equations

• CategoryTheory.unique_colimit_representable F = (CategoryTheory.Limits.Types.colimitEquivQuot F).unique

noncomputable def CategoryTheory.uniqueπ₀Obj_of_isRepresentable {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (X : Sheaf J (Type (max u w))) [X.val.IsRepresentable] : Unique ((Sheaf.π₀ J).obj X)

Sheaf.π₀ sends representable sheaves to singleton types.

Equations

• CategoryTheory.uniqueπ₀Obj_of_isRepresentable J X = CategoryTheory.unique_colimit_representable X.val

instance CategoryTheory.instPreservesLimitSheafTypeDiscretePEmptyEmptyπ₀OfHasTerminal {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [Limits.HasTerminal C] : Limits.PreservesLimit (Functor.empty (Sheaf J (Type (max u w)))) (Sheaf.π₀ J)

On locally connected sites with a terminal object, Sheaf.π₀ preserves the terminal object.

instance CategoryTheory.colimPreservesFiniteProductsOfIsSifted {C : Type u} [Category.{v, u} C] : Limits.PreservesFiniteProducts Limits.colim

If C is sifted, the colim functor (C ⥤ Type) ⥤ Type preserves finite products. Taken from mathlib PR #17781. TODO: remove once #17781 or a similar result has landed in mathlib.

instance CategoryTheory.instPreservesFiniteProductsSheafTypeπ₀OfIsSiftedOpposite {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [IsSifted Cᵒᵖ] : Limits.PreservesFiniteProducts (Sheaf.π₀ J)

Sheaf topoi on cosifted locally connected sites are strongly connected, in the sense that π₀ preserves all finite products. TODO: generalise universe levels.