Local sites

A site is called local if it has a terminal object whose only covering sieve is trivial - this makes it possible to define coconstant sheaves on it, giving its sheaf topos the structure of a local topos. This is one of the conditions of cohesive sites.

Sheaves of types on any local site form a local topos (i.e. a topos whose global sections functor has a fully faithful right adjoint), and a subcanonical site is local if and only if its topos of sheaves of types is (see TODOs).

Main definitions / results

• J.IsLocalSite: typeclass stating that J makes the category it is defined on into a local site.
• IsLocalSite.point J: the canonical point of any local site, whose fibre functor is given by the coyoneda embedding of the terminal object and extends to the global sections functors on presheaves and sheaves.
• coconstantSheaf J A: the coconstant sheaf functor A ⥤ Sheaf J A for any local site and sufficiently nice target category A, defined as the skyscraper sheaf functor of the canonical point.
• ΓCoconstantSheafAdj J A: the adjunction between the global sections functor Γ J A and coconstantSheaf J A.
• fullyFaithfulCoconstantSheaf: coconstantSheaf is fully faithful.
• fullyFaithfulConstantSheaf: on local sites, the constant sheaf functor is fully faithful.

References

• https://ncatlab.org/nlab/show/local+site

TODO

• Define local topoi and prove that sheaves on any local site form a local topos
• Show that a subcanonical site is local if and only if its global sections functor has a fully faithful right adjoint

class CategoryTheory.GrothendieckTopology.IsLocalSite {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) extends CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) C : Prop

A local site is a site that has a terminal object with only a single covering sieve.

• has_limit (F : Functor (Discrete PEmpty.{1}) C) : HasLimit F
• eq_top_of_mem (S : Sieve (⊤_ C)) : S ∈ J (⊤_ C) → S = ⊤

  The only covering sieve of the terminal object is the trivial sieve.

theorem CategoryTheory.GrothendieckTopology.IsLocalSite.from_terminal_mem_of_mem {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.IsLocalSite] {X : C} (f : ⊤_ C ⟶ X) {S : Sieve X} (hS : S ∈ J X) : S.arrows f

On a local site, every covering sieve contains every morphism from the terminal object.

instance CategoryTheory.GrothendieckTopology.IsLocalSite.instTrivialOfHasTerminal {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] : (trivial C).IsLocalSite

Every category with a terminal object becomes a local site with the trivial topology.

noncomputable def CategoryTheory.GrothendieckTopology.IsLocalSite.point {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [LocallySmall.{w, v, u} C] [J.IsLocalSite] : J.Point

Every local site has a canonical point, given as a fibre functor by the coyoneda embedding of the terminal object ⊤_ C.

Equations

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

noncomputable def CategoryTheory.GrothendieckTopology.IsLocalSite.coconstantSheaf {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [LocallySmall.{w, v, u} C] [J.IsLocalSite] (A : Type u') [Category.{v', u'} A] [Limits.HasProducts A] : Functor A (Sheaf J A)

The right adjoint to the global sections functor that exists over any local site. This is implemented as the skyscraper functor associated to point.{w} J, but can be thought of as taking any object X : A to the sheaf that sends each Y : C to the product over copies of A indexed by the points ⊤_ C ⟶ Y of Y.

Note this takes in an extra universe parameter w that does not appear in the output type A ⥤ Sheaf J A but is required for the construction; it should always be given explicitly when referring to this functor, as in e.g. coconstantSheaf.{w} J A.

Equations

• CategoryTheory.GrothendieckTopology.IsLocalSite.coconstantSheaf J A = (CategoryTheory.GrothendieckTopology.IsLocalSite.point J).skyscraperSheafFunctor

noncomputable def CategoryTheory.GrothendieckTopology.IsLocalSite.pointPresheafFiberIso {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [LocallySmall.{w, v, u} C] [J.IsLocalSite] {A : Type u'} [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] (P : Functor Cᵒᵖ A) : (point J).presheafFiber.obj P ≅ P.obj (Opposite.op (⊤_ C))

The fibre of any presheaf P : Cᵒᵖ ⥤ A at point J is just P evaluated at the terminal object.

Equations

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

@[simp]

theorem CategoryTheory.GrothendieckTopology.IsLocalSite.toPresheafFiber_pointPresheafFiberIso_hom {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [LocallySmall.{w, v, u} C] [J.IsLocalSite] {A : Type u'} [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] {P : Functor Cᵒᵖ A} (X : C) (x : (point J).fiber.obj X) : CategoryStruct.comp ((point J).toPresheafFiber X x P) (pointPresheafFiberIso J P).hom = P.map (shrinkCoyonedaObjObjEquiv x).op

@[simp]

theorem CategoryTheory.GrothendieckTopology.IsLocalSite.toPresheafFiber_pointPresheafFiberIso_hom_assoc {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [LocallySmall.{w, v, u} C] [J.IsLocalSite] {A : Type u'} [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] {P : Functor Cᵒᵖ A} (X : C) (x : (point J).fiber.obj X) {Z : A} (h : P.obj (Opposite.op (⊤_ C)) ⟶ Z) : CategoryStruct.comp ((point J).toPresheafFiber X x P) (CategoryStruct.comp (pointPresheafFiberIso J P).hom h) = CategoryStruct.comp (P.map (shrinkCoyonedaObjObjEquiv x).op) h

@[simp]

theorem CategoryTheory.GrothendieckTopology.IsLocalSite.pointPresheafFiberIso_naturality {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [LocallySmall.{w, v, u} C] [J.IsLocalSite] {A : Type u'} [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] {P P' : Functor Cᵒᵖ A} (F : P ⟶ P') : CategoryStruct.comp ((point J).presheafFiber.map F) (pointPresheafFiberIso J P').hom = CategoryStruct.comp (pointPresheafFiberIso J P).hom (F.app (Opposite.op (⊤_ C)))

@[simp]

theorem CategoryTheory.GrothendieckTopology.IsLocalSite.pointPresheafFiberIso_naturality_assoc {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [LocallySmall.{w, v, u} C] [J.IsLocalSite] {A : Type u'} [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] {P P' : Functor Cᵒᵖ A} (F : P ⟶ P') {Z : A} (h : P'.obj (Opposite.op (⊤_ C)) ⟶ Z) : CategoryStruct.comp ((point J).presheafFiber.map F) (CategoryStruct.comp (pointPresheafFiberIso J P').hom h) = CategoryStruct.comp (pointPresheafFiberIso J P).hom (CategoryStruct.comp (F.app (Opposite.op (⊤_ C))) h)

noncomputable def CategoryTheory.GrothendieckTopology.IsLocalSite.pointPresheafFiberNatIso {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [LocallySmall.{w, v, u} C] [J.IsLocalSite] (A : Type u') [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] : (point J).presheafFiber ≅ (evaluation Cᵒᵖ A).obj (Opposite.op (⊤_ C))

The presheaf fibre functor of point J is given by evaluation at the terminal object.

Equations

• CategoryTheory.GrothendieckTopology.IsLocalSite.pointPresheafFiberNatIso J A = CategoryTheory.NatIso.ofComponents (CategoryTheory.GrothendieckTopology.IsLocalSite.pointPresheafFiberIso J) ⋯

noncomputable def CategoryTheory.GrothendieckTopology.IsLocalSite.pointSheafFiberIso {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [LocallySmall.{w, v, u} C] [J.IsLocalSite] (A : Type u') [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] [HasWeakSheafify J A] : (point J).sheafFiber ≅ Sheaf.Γ J A

The sheaf fibre functor of point J is the global sections functor.

Equations

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

noncomputable def CategoryTheory.GrothendieckTopology.IsLocalSite.ΓCoconstantSheafAdj {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [LocallySmall.{w, v, u} C] [J.IsLocalSite] (A : Type u') [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] [Limits.HasProducts A] [HasWeakSheafify J A] : Sheaf.Γ J A ⊣ coconstantSheaf J A

On local sites, the global sections functor Γ is left-adjoint to the coconstant functor.

Equations

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

theorem CategoryTheory.GrothendieckTopology.IsLocalSite.Γ_isLeftAdjoint {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [LocallySmall.{w, v, u} C] [J.IsLocalSite] (A : Type u') [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] [Limits.HasProducts A] [HasWeakSheafify J A] : (Sheaf.Γ J A).IsLeftAdjoint

On any locally w-small local site, the global sections functor to any category with colimits and products of size w is a left adjoint. A variant of this without the universe parameter w is registered as an instance.

instance CategoryTheory.GrothendieckTopology.IsLocalSite.instIsLeftAdjointSheafΓOfHasColimitsOfSizeOfHasProducts {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.IsLocalSite] (A : Type u') [Category.{v', u'} A] [Limits.HasColimitsOfSize.{v, v, v', u'} A] [Limits.HasProducts A] [HasWeakSheafify J A] : (Sheaf.Γ J A).IsLeftAdjoint

On any local site with morphism types in Type v, the global sections functor to any category with colimits and products of size v is a left adjoint. See ΓIsLeftAdjoint for a version for w-locally small sites that can't be registered as an instance because of the extra universe parameter w.

instance CategoryTheory.GrothendieckTopology.IsLocalSite.instIsRightAdjointSheafCoconstantSheaf {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [LocallySmall.{w, v, u} C] [J.IsLocalSite] (A : Type u') [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] [Limits.HasProducts A] [HasWeakSheafify J A] : (coconstantSheaf J A).IsRightAdjoint

noncomputable def CategoryTheory.GrothendieckTopology.IsLocalSite.coconstantSheafΓNatIsoId {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [LocallySmall.{w, v, u} C] [J.IsLocalSite] (A : Type u') [Category.{v', u'} A] [Limits.HasProducts A] [HasWeakSheafify J A] : (coconstantSheaf J A).comp (Sheaf.Γ J A) ≅ Functor.id A

The global sections of the coconstant sheaf on a type are naturally isomorphic to that type.

Equations

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

noncomputable def CategoryTheory.GrothendieckTopology.IsLocalSite.fullyFaithfulCoconstantSheaf {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [LocallySmall.{w, v, u} C] [J.IsLocalSite] (A : Type u') [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] [Limits.HasProducts A] [HasWeakSheafify J A] : (coconstantSheaf J A).FullyFaithful

coconstantSheaf is fully faithful.

Equations

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

instance CategoryTheory.GrothendieckTopology.IsLocalSite.instFullSheafCoconstantSheaf {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [LocallySmall.{w, v, u} C] [J.IsLocalSite] (A : Type u') [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] [Limits.HasProducts A] [HasWeakSheafify J A] : (coconstantSheaf J A).Full

instance CategoryTheory.GrothendieckTopology.IsLocalSite.instFaithfulSheafCoconstantSheaf {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [LocallySmall.{w, v, u} C] [J.IsLocalSite] (A : Type u') [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] [Limits.HasProducts A] [HasWeakSheafify J A] : (coconstantSheaf J A).Faithful

@[reducible, inline]

noncomputable abbrev CategoryTheory.GrothendieckTopology.IsLocalSite.constantΓCoconstantTriple {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [LocallySmall.{w, v, u} C] [J.IsLocalSite] (A : Type u') [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] [Limits.HasProducts A] [HasWeakSheafify J A] : Adjunction.Triple (constantSheaf J A) (Sheaf.Γ J A) (coconstantSheaf J A)

The adjoint triple constantSheaf J A ⊣ Γ J A ⊣ coconstantSheaf J A on any local site.

Equations

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

noncomputable def CategoryTheory.GrothendieckTopology.IsLocalSite.fullyFaithfulConstantSheaf {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [LocallySmall.{w, v, u} C] [J.IsLocalSite] (A : Type u') [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] [Limits.HasProducts A] [HasWeakSheafify J A] : (constantSheaf J A).FullyFaithful

On local sites, the constant sheaf functor is fully faithful.

Equations

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

theorem CategoryTheory.GrothendieckTopology.IsLocalSite.full_constantSheaf {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [LocallySmall.{w, v, u} C] [J.IsLocalSite] (A : Type u') [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] [Limits.HasProducts A] [HasWeakSheafify J A] : (constantSheaf J A).Full

theorem CategoryTheory.GrothendieckTopology.IsLocalSite.faithful_constantSheaf {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [LocallySmall.{w, v, u} C] [J.IsLocalSite] (A : Type u') [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] [Limits.HasProducts A] [HasWeakSheafify J A] : (constantSheaf J A).Faithful

instance CategoryTheory.GrothendieckTopology.IsLocalSite.instFullSheafConstantSheafOfHasColimitsOfSizeOfHasProducts {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.IsLocalSite] (A : Type u') [Category.{v', u'} A] [Limits.HasColimitsOfSize.{v, v, v', u'} A] [Limits.HasProducts A] [HasWeakSheafify J A] : (constantSheaf J A).Full

See IsLocalSite.full_constantSheaf for a version for w-locally small sites.

instance CategoryTheory.GrothendieckTopology.IsLocalSite.instFaithfulSheafConstantSheafOfHasColimitsOfSizeOfHasProducts {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.IsLocalSite] (A : Type u') [Category.{v', u'} A] [Limits.HasColimitsOfSize.{v, v, v', u'} A] [Limits.HasProducts A] [HasWeakSheafify J A] : (constantSheaf J A).Faithful

See IsLocalSite.faithful_constantSheaf for a version for w-locally small sites.