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.

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 set A to the functor Cᵒᵖ → Type _ that sends any X : C to the set of all functions A → (⊤_ C ⟶ X). 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.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.Γ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.Γ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.Γ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.instIsLeftAdjointSheafTypeΓOfIsLocalSite {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.IsLocalSite] : (Sheaf.Γ J (Type (max u v))).IsLeftAdjoint

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

noncomputable def CategoryTheory.coconstantSheafΓNatIsoId {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.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] : (coconstantSheaf J).FullyFaithful

coconstantSheaf is fully faithful.

Equations

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

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

instance CategoryTheory.instFaithfulSheafTypeCoconstantSheaf {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.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