Local sites

A site (C,J) 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 makes them an important stepping stone to cohesive sites.

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

Main definitions / results

• J.IsLocalSite: typeclass stating that (C,J) is a local site.
• coconstantSheaf: the coconstant sheaf functor Type w ⥤ Sheaf J (Type max v w) defined on any local site.
• ΓCoconstantSheafAdj: the adjunction between the global sections functor Γ and coconstantSheaf.
• fullyFaithfulCoconstantSheaf: coconstantSheaf is fully faithful.
• fullyFaithfulConstantSheaf: on local sites, the constant sheaf functor is fully faithful. All together this shows that for local sites Sheaf J (Type max u v w) forms a local topos, but since we don't yet have local topoi this can't be stated yet.

We also define a Grothendieck topology localTopology C on any category C with a terminal object, and show that it is the largest topology making C into a local site.

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

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.LocalSite.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.instIsLocalSiteTrivialOfHasTerminal {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] : (GrothendieckTopology.trivial C).IsLocalSite

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

noncomputable def CategoryTheory.Presheaf.coconst {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] : Functor (Type w) (Functor Cᵒᵖ (Type (max v w)))

The functor that sends any type A to the functor Cᵒᵖ → Type _ that sends any X : C to the type of all functions (⊤_ C ⟶ X) → A. This can be defined on any site with a terminal object, but has values in sheaves in the case of local sites.

Equations

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

theorem CategoryTheory.Presheaf.coconst_isSheaf {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.IsLocalSite] (X : Type w) : IsSheaf J (coconst.obj X)

On local sites, Presheaf.coconst actually takes values in sheaves.

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

The right adjoint to the global sections functor that exists over any local site. Takes a type X to the sheaf that sends each Y : C to the type of functions Y → X.

Equations

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

noncomputable def CategoryTheory.IsLocalSite.ΓCoconstantSheafAdj {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.IsLocalSite] : Sheaf.Γ J (Type (max u v)) ⊣ coconstantSheaf J

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.

@[simp]

theorem CategoryTheory.IsLocalSite.ΓCoconstantSheafAdj_counit_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.IsLocalSite] (Y : Type (max u v)) (a✝ : (Sheaf.Γ J (Type (max u v))).obj ((coconstantSheaf J).obj Y)) : (ΓCoconstantSheafAdj J).counit.app Y a✝ = (Adjunction.equivHomsetLeftOfNatIso (Sheaf.ΓNatIsoSheafSections J (Type (max u v)) Limits.terminalIsTerminal)).symm (({ unit := { app := fun (X : Sheaf J (Type (max u v))) => { val := { app := fun (Y : Cᵒᵖ) (x : X.val.obj Y) (y : ULift.{max u v, v} (⊤_ C ⟶ Opposite.unop Y)) => { down := X.val.map (Opposite.op y.down) x }, naturality := ⋯ } }, naturality := ⋯ }, counit := { app := fun (X : Type (max u v)) (f : ULift.{max u v, v} (⊤_ C ⟶ ⊤_ C) → ULift.{v, max u v} X) => (f default).down, naturality := ⋯ }, left_triangle_components := ⋯, right_triangle_components := ⋯ }.homEquiv ((coconstantSheaf J).obj Y) Y).symm (CategoryStruct.id ((coconstantSheaf J).obj Y))) a✝

@[simp]

theorem CategoryTheory.IsLocalSite.ΓCoconstantSheafAdj_unit_app_val_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.IsLocalSite] (X : Sheaf J (Type (max u v))) (X✝ : Cᵒᵖ) (a✝ : X.val.obj X✝) : ((ΓCoconstantSheafAdj J).unit.app X).val.app X✝ a✝ = ((coconstantSheaf J).map ((Adjunction.equivHomsetLeftOfNatIso (Sheaf.ΓNatIsoSheafSections J (Type (max u v)) Limits.terminalIsTerminal)) (CategoryStruct.id ((Sheaf.Γ J (Type (max u v))).obj X)))).val.app X✝ fun (y : ULift.{max u v, v} (⊤_ C ⟶ Opposite.unop X✝)) => { down := X.val.map (Opposite.op y.down) a✝ }

instance CategoryTheory.instIsRightAdjointSheafTypeCoconstantSheaf {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.IsLocalSite] : (IsLocalSite.coconstantSheaf J).IsRightAdjoint

instance CategoryTheory.instHasCoconstantSheafTypeOfIsLocalSite {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.IsLocalSite] : HasCoconstantSheaf J (Type (max u v))

noncomputable def CategoryTheory.coconstantSheafΓNatIsoId {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.IsLocalSite] : (IsLocalSite.coconstantSheaf J).comp (Sheaf.Γ J (Type (max u v))) ≅ Functor.id (Type (max u v))

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.fullyFaithfulCoconstantSheaf {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.IsLocalSite] : (IsLocalSite.coconstantSheaf J).FullyFaithful

coconstantSheaf is fully faithful.

Equations

• CategoryTheory.fullyFaithfulCoconstantSheaf J = (CategoryTheory.IsLocalSite.ΓCoconstantSheafAdj J).fullyFaithfulROfCompIsoId (CategoryTheory.coconstantSheafΓNatIsoId J)

instance CategoryTheory.instFullSheafTypeCoconstantSheaf {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.IsLocalSite] : (IsLocalSite.coconstantSheaf J).Full

instance CategoryTheory.instFaithfulSheafTypeCoconstantSheaf {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.IsLocalSite] : (IsLocalSite.coconstantSheaf J).Faithful

noncomputable def CategoryTheory.fullyFaithfulConstantSheaf {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [HasWeakSheafify J (Type (max u v))] [J.IsLocalSite] : (constantSheaf J (Type (max u v))).FullyFaithful

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

Equations

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

instance CategoryTheory.instFullSheafTypeConstantSheafOfIsLocalSite {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [HasWeakSheafify J (Type (max u v))] [J.IsLocalSite] : (constantSheaf J (Type (max u v))).Full

instance CategoryTheory.instFaithfulSheafTypeConstantSheafOfIsLocalSite {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [HasWeakSheafify J (Type (max u v))] [J.IsLocalSite] : (constantSheaf J (Type (max u v))).Faithful

def CategoryTheory.localTopology (C : Type u_1) [Category.{u_2, u_1} C] [Limits.HasTerminal C] : GrothendieckTopology C

The largest topology making a category with a terminal object a local site. Lacking an established name, we call it the local topology.

Equations

• CategoryTheory.localTopology C = (CategoryTheory.MorphismProperty.morphismsThrough (⊤_ C)).generatedTopology

theorem CategoryTheory.localTopology.mem_sieves_iff {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] {X : C} {S : Sieve X} : S ∈ (localTopology C) X ↔ ∀ (x : ⊤_ C ⟶ X), S.arrows x

theorem CategoryTheory.GrothendieckTopology.IsLocalSite.tfae {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [Limits.HasTerminal C] : [J.IsLocalSite, ∀ (X : C), ∀ S ∈ J X, ∀ (x : ⊤_ C ⟶ X), S.arrows x, J ≤ localTopology C, Presieve.IsSheaf J (Presheaf.coconst.obj PEmpty.{max (u + 1) (v + 1)}), ∀ (X : Type (max u v)), Presieve.IsSheaf J (Presheaf.coconst.obj X)].TFAE

For any site with a terminal object, the following are equivalent:

• the site is local, i.e. the only covering sieve of the terminal object is the trivial one
• every covering sieve contains all morphisms from the terminal object
• the coconstant presheaf on the empty type is a sheaf
• every coconstant presheaf is a sheaf.

I don't yet know how exactly HasCoconstantSheaf J (Type max u v) fits into this - every local site has a coconstant sheaf functor, and every subcanonical site with a coconstant sheaf functor is local, but it's not clear to me what can be said in the non-subcanonical case. Maybe having a fully faithful coconstant sheaf functor could be strong enough? TODO: figure this out

instance CategoryTheory.instIsLocalSiteLocalTopology {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] : (localTopology C).IsLocalSite