Global sections of sheaves

In this file we define a global sections functor Sheaf.Γ : Sheaf J A ⥤ A and show that it is isomorphic to several other constructions when they exist, most notably evaluation of sheaves on a terminal object and Functor.sectionsFunctor.

Main definitions / results

• HasGlobalSectionsFunctor J A: typeclass stating that the constant sheaf functor A ⥤ Sheaf J A has a right-adjoint.
• Sheaf.Γ J A: the global sections functor Sheaf J A ⥤ A, defined as the right-adjoint of the constant sheaf functor, whenever that exists.
• constantSheafΓAdj J A: the adjunction between the constant sheaf functor and Sheaf.Γ J A.
• Sheaf.ΓNatIsoSheafSections J A hT: on sites with a terminal object T, Sheaf.Γ J A exists and is isomorphic to the functor evaluating sheaves at T.
• Sheaf.ΓNatIsoLim J A: when A has limits of shape Cᵒᵖ, Sheaf.Γ J A exists and is isomorphic to the functor taking each sheaf to the limit of its underlying presheaf.
• Sheaf.isLimitConeΓ F: global sections are limits even when not all limits of shape Cᵒᵖ exist.
• Sheaf.ΓRes F U: the restriction morphism from global sections of F to sections of F on U.
• Sheaf.natTransΓRes J A U: the natural transformation from the global sections functor to the sections functor on U.
• Sheaf.ΓNatIsoSectionsFunctor J: for sheaves of types, Sheaf.Γ J A is isomorphic to the functor taking each sheaf to the type of sections of its underlying presheaf in the sense of Functor.sections.
• Sheaf.ΓNatIsoCoyoneda J: for sheaves of types, Sheaf.Γ J A is isomorphic to the coyoneda embedding of the terminal sheaf, i.e. the functor sending each sheaf F to the type of morphisms from the terminal sheaf to F.

TODO

• Generalise Sheaf.ΓNatIsoSectionsFunctor and Sheaf.ΓNatIsoCoyoneda from Type max u v to Type max u v w. This should hopefully be doable by relaxing the universe constraints of instHasSheafifyOfHasFiniteLimits.

@[reducible, inline]

abbrev CategoryTheory.HasGlobalSectionsFunctor {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u₂) [Category.{v₂, u₂} A] [HasWeakSheafify J A] : Prop

Typeclass stating that the constant sheaf functor has a right adjoint. This right adjoint will then be called the global sections functor and written Sheaf.Γ.

Equations

• CategoryTheory.HasGlobalSectionsFunctor J A = (CategoryTheory.constantSheaf J A).IsLeftAdjoint

noncomputable def CategoryTheory.Sheaf.Γ {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u₂) [Category.{v₂, u₂} A] [HasWeakSheafify J A] [HasGlobalSectionsFunctor J A] : Functor (Sheaf J A) A

We define the global sections functor as the right-adjoint of the constant sheaf functor whenever it exists.

Equations

• CategoryTheory.Sheaf.Γ J A = (CategoryTheory.constantSheaf J A).rightAdjoint

noncomputable def CategoryTheory.constantSheafΓAdj {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u₂) [Category.{v₂, u₂} A] [HasWeakSheafify J A] [HasGlobalSectionsFunctor J A] : constantSheaf J A ⊣ Sheaf.Γ J A

The constant sheaf functor is by definition left-adjoint to the global sections functor.

Equations

• CategoryTheory.constantSheafΓAdj J A = CategoryTheory.Adjunction.ofIsLeftAdjoint (CategoryTheory.constantSheaf J A)

instance CategoryTheory.instIsRightAdjointSheafΓ {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u₂) [Category.{v₂, u₂} A] [HasWeakSheafify J A] [HasGlobalSectionsFunctor J A] : (Sheaf.Γ J A).IsRightAdjoint

instance CategoryTheory.hasGlobalSectionsFunctor_of_hasTerminal {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u₂) [Category.{v₂, u₂} A] [HasWeakSheafify J A] [Limits.HasTerminal C] : HasGlobalSectionsFunctor J A

Sites with a terminal object admit a global sections functor.

noncomputable def CategoryTheory.Sheaf.ΓNatIsoSheafSections {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u₂) [Category.{v₂, u₂} A] [HasWeakSheafify J A] [Limits.HasTerminal C] {T : C} (hT : Limits.IsTerminal T) : Γ J A ≅ (sheafSections J A).obj (Opposite.op T)

On sites with a terminal object, the global sections functor is isomorphic to the functor of sections on that object.

Equations

• CategoryTheory.Sheaf.ΓNatIsoSheafSections J A hT = (CategoryTheory.constantSheafΓAdj J A).rightAdjointUniq (CategoryTheory.constantSheafAdj J A hT)

instance CategoryTheory.hasGlobalSectionsFunctor_of_hasLimitsOfShape {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u₂) [Category.{v₂, u₂} A] [HasWeakSheafify J A] [Limits.HasLimitsOfShape Cᵒᵖ A] : HasGlobalSectionsFunctor J A

Every site C admits a global sections functor for A-valued sheaves when A has limits of shape Cᵒᵖ.

noncomputable def CategoryTheory.Sheaf.ΓNatIsoLim {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u₂) [Category.{v₂, u₂} A] [HasWeakSheafify J A] [Limits.HasLimitsOfShape Cᵒᵖ A] : Γ J A ≅ (sheafToPresheaf J A).comp Limits.lim

Global sections of sheaves are naturally isomorphic to the limits of the underlying presheaves. Note that while HasLimitsOfShape Cᵒᵖ A is needed here to talk about lim as a functor, global sections are still limits without it - see Sheaf.isLimitConeΓ.

Equations

• CategoryTheory.Sheaf.ΓNatIsoLim J A = (CategoryTheory.constantSheafΓAdj J A).rightAdjointUniq (CategoryTheory.Limits.constLimAdj.comp (CategoryTheory.sheafificationAdjunction J A))

noncomputable def CategoryTheory.Sheaf.ΓHomEquiv {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u₂} [Category.{v₂, u₂} A] [HasWeakSheafify J A] [HasGlobalSectionsFunctor J A] {X : A} {F : Sheaf J A} : ((Functor.const Cᵒᵖ).obj X ⟶ F.val) ≃ (X ⟶ (Γ J A).obj F)

Natural transformations from a constant presheaf into a sheaf correspond to morphisms to its global sections.

Equations

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

theorem CategoryTheory.Sheaf.ΓHomEquiv_naturality_left {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u₂} [Category.{v₂, u₂} A] [HasWeakSheafify J A] [HasGlobalSectionsFunctor J A] {X' X : A} {F : Sheaf J A} (f : X' ⟶ X) (g : (Functor.const Cᵒᵖ).obj X ⟶ F.val) : ΓHomEquiv (CategoryStruct.comp ((Functor.const Cᵒᵖ).map f) g) = CategoryStruct.comp f (ΓHomEquiv g)

Naturality lemma for ΓHomEquiv analogous to Adjunction.homEquiv_naturality_left.

theorem CategoryTheory.Sheaf.ΓHomEquiv_naturality_left_symm {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u₂} [Category.{v₂, u₂} A] [HasWeakSheafify J A] [HasGlobalSectionsFunctor J A] {X' X : A} {F : Sheaf J A} (f : X' ⟶ X) (g : X ⟶ (Γ J A).obj F) : ΓHomEquiv.symm (CategoryStruct.comp f g) = CategoryStruct.comp ((Functor.const Cᵒᵖ).map f) (ΓHomEquiv.symm g)

Naturality lemma for ΓHomEquiv analogous to Adjunction.homEquiv_naturality_left_symm.

theorem CategoryTheory.Sheaf.ΓHomEquiv_naturality_right {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u₂} [Category.{v₂, u₂} A] [HasWeakSheafify J A] [HasGlobalSectionsFunctor J A] {X : A} {F F' : Sheaf J A} (f : (Functor.const Cᵒᵖ).obj X ⟶ F.val) (g : F ⟶ F') : ΓHomEquiv (CategoryStruct.comp f g.val) = CategoryStruct.comp (ΓHomEquiv f) ((Γ J A).map g)

Naturality lemma for ΓHomEquiv analogous to Adjunction.homEquiv_naturality_right.

theorem CategoryTheory.Sheaf.ΓHomEquiv_naturality_right_symm {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u₂} [Category.{v₂, u₂} A] [HasWeakSheafify J A] [HasGlobalSectionsFunctor J A] {X : A} {F F' : Sheaf J A} (f : X ⟶ (Γ J A).obj F) (g : F ⟶ F') : ΓHomEquiv.symm (CategoryStruct.comp f ((Γ J A).map g)) = CategoryStruct.comp (ΓHomEquiv.symm f) g.val

Naturality lemma for ΓHomEquiv analogous to Adjunction.homEquiv_naturality_right_symm.

noncomputable def CategoryTheory.Sheaf.coneΓ {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u₂} [Category.{v₂, u₂} A] [HasWeakSheafify J A] [HasGlobalSectionsFunctor J A] (F : Sheaf J A) : Limits.Cone F.val

The cone over a given sheaf whose cone point are the global sections and whose components are the restriction maps.

Equations

• F.coneΓ = { pt := (CategoryTheory.Sheaf.Γ J A).obj F, π := CategoryTheory.Sheaf.ΓHomEquiv.symm (CategoryTheory.CategoryStruct.id ((CategoryTheory.Sheaf.Γ J A).obj F)) }

@[simp]

theorem CategoryTheory.Sheaf.coneΓ_pt {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u₂} [Category.{v₂, u₂} A] [HasWeakSheafify J A] [HasGlobalSectionsFunctor J A] (F : Sheaf J A) : F.coneΓ.pt = (Γ J A).obj F

noncomputable def CategoryTheory.Sheaf.isLimitConeΓ {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u₂} [Category.{v₂, u₂} A] [HasWeakSheafify J A] [HasGlobalSectionsFunctor J A] (F : Sheaf J A) : Limits.IsLimit F.coneΓ

The global sections cone Sheaf.coneΓ is limiting - that is, global sections are limits even when not all limits of shape Cᵒᵖ exist in A.

Equations

• F.isLimitConeΓ = { lift := fun (c : CategoryTheory.Limits.Cone F.val) => CategoryTheory.Sheaf.ΓHomEquiv c.π, fac := ⋯, uniq := ⋯ }

noncomputable def CategoryTheory.Sheaf.ΓRes {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u₂} [Category.{v₂, u₂} A] [HasWeakSheafify J A] [HasGlobalSectionsFunctor J A] (F : Sheaf J A) (U : Cᵒᵖ) : (Γ J A).obj F ⟶ F.val.obj U

The restriction map from global sections of F to sections on U.

Equations

• F.ΓRes U = F.coneΓ.π.app U

@[simp]

theorem CategoryTheory.Sheaf.ΓRes_map {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u₂} [Category.{v₂, u₂} A] [HasWeakSheafify J A] [HasGlobalSectionsFunctor J A] (F : Sheaf J A) {V U : Cᵒᵖ} (f : U ⟶ V) : CategoryStruct.comp (F.ΓRes U) (F.val.map f) = F.ΓRes V

@[simp]

theorem CategoryTheory.Sheaf.ΓRes_map_assoc {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u₂} [Category.{v₂, u₂} A] [HasWeakSheafify J A] [HasGlobalSectionsFunctor J A] (F : Sheaf J A) {V U : Cᵒᵖ} (f : U ⟶ V) {Z : A} (h : F.val.obj V ⟶ Z) : CategoryStruct.comp (F.ΓRes U) (CategoryStruct.comp (F.val.map f) h) = CategoryStruct.comp (F.ΓRes V) h

@[simp]

theorem CategoryTheory.Sheaf.coneΓ_π_app {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u₂} [Category.{v₂, u₂} A] [HasWeakSheafify J A] [HasGlobalSectionsFunctor J A] (F : Sheaf J A) (U : Cᵒᵖ) : F.coneΓ.π.app U = F.ΓRes U

theorem CategoryTheory.Sheaf.ΓRes_naturality {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u₂} [Category.{v₂, u₂} A] [HasWeakSheafify J A] [HasGlobalSectionsFunctor J A] {F G : Sheaf J A} (f : F ⟶ G) (U : Cᵒᵖ) : CategoryStruct.comp ((Γ J A).map f) (G.ΓRes U) = CategoryStruct.comp (F.ΓRes U) (f.val.app U)

noncomputable def CategoryTheory.Sheaf.natTransΓRes {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u₂) [Category.{v₂, u₂} A] [HasWeakSheafify J A] [HasGlobalSectionsFunctor J A] (U : Cᵒᵖ) : Γ J A ⟶ (sheafSections J A).obj U

The natural transformation from the global sections functor to the sections functor on any object U.

Equations

• CategoryTheory.Sheaf.natTransΓRes J A U = { app := fun (F : CategoryTheory.Sheaf J A) => F.ΓRes U, naturality := ⋯ }

@[simp]

theorem CategoryTheory.Sheaf.natTransΓRes_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u₂) [Category.{v₂, u₂} A] [HasWeakSheafify J A] [HasGlobalSectionsFunctor J A] (U : Cᵒᵖ) (F : Sheaf J A) : (natTransΓRes J A U).app F = F.ΓRes U

noncomputable def CategoryTheory.Sheaf.ΓObjEquivSections {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [HasWeakSheafify J (Type w)] [HasGlobalSectionsFunctor J (Type w)] (F : Sheaf J (Type w)) : (Γ J (Type w)).obj F ≃ ↑F.val.sections

Global sections of a sheaf of types correspond to sections of the underlying presheaf.

Equations

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

theorem CategoryTheory.Sheaf.ΓObjEquivSections_naturality {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [HasWeakSheafify J (Type w)] [HasGlobalSectionsFunctor J (Type w)] {F G : Sheaf J (Type w)} (f : F ⟶ G) (x : (Γ J (Type w)).obj F) : (ΓObjEquivSections J G) ((Γ J (Type w)).map f x) = (Functor.sectionsFunctor Cᵒᵖ).map f.val ((ΓObjEquivSections J F) x)

theorem CategoryTheory.Sheaf.ΓObjEquivSections_naturality_symm {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [HasWeakSheafify J (Type w)] [HasGlobalSectionsFunctor J (Type w)] {F G : Sheaf J (Type w)} (f : F ⟶ G) (x : ↑F.val.sections) : (ΓObjEquivSections J G).symm ((Functor.sectionsFunctor Cᵒᵖ).map f.val x) = (Γ J (Type w)).map f ((ΓObjEquivSections J F).symm x)

noncomputable def CategoryTheory.Sheaf.ΓNatIsoSectionsFunctor {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) : Γ J (Type (max u v)) ≅ (sheafToPresheaf J (Type (max u v))).comp (Functor.sectionsFunctor Cᵒᵖ)

For sheaves of types, the global sections functor is isomorphic to the sections functor on presheaves.

Equations

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

noncomputable def CategoryTheory.Sheaf.ΓObjEquivHom {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [HasWeakSheafify J (Type w)] [HasGlobalSectionsFunctor J (Type w)] (F : Sheaf J (Type w)) (X : Type w) [Unique X] : (Γ J (Type w)).obj F ≃ ((constantSheaf J (Type w)).obj X ⟶ F)

Global sections of a sheaf of types F correspond to morphisms from a terminal sheaf to F. We use the constant sheaf on a singleton type as a specific choice of terminal sheaf here.

Equations

• CategoryTheory.Sheaf.ΓObjEquivHom J F X = (Equiv.funUnique X ((CategoryTheory.Sheaf.Γ J (Type ?u.70)).obj F)).symm.trans ((CategoryTheory.constantSheafΓAdj J (Type ?u.70)).homEquiv X F).symm

theorem CategoryTheory.Sheaf.ΓObjEquivHom_naturality {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [HasWeakSheafify J (Type w)] [HasGlobalSectionsFunctor J (Type w)] (X : Type w) [Unique X] {F G : Sheaf J (Type w)} (f : F ⟶ G) (x : (Γ J (Type w)).obj F) : (ΓObjEquivHom J G X) ((Γ J (Type w)).map f x) = CategoryStruct.comp ((ΓObjEquivHom J F X) x) f

theorem CategoryTheory.Sheaf.ΓObjEquivHom_naturality_symm {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [HasWeakSheafify J (Type w)] [HasGlobalSectionsFunctor J (Type w)] {X : Type w} [Unique X] {F G : Sheaf J (Type w)} (f : F ⟶ G) (x : (constantSheaf J (Type w)).obj X ⟶ F) : (ΓObjEquivHom J G X).symm (CategoryStruct.comp x f) = (Γ J (Type w)).map f ((ΓObjEquivHom J F X).symm x)

noncomputable def CategoryTheory.Sheaf.ΓNatIsoCoyoneda {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (X : Type (max u v)) [Unique X] : Γ J (Type (max u v)) ≅ coyoneda.obj (Opposite.op ((constantSheaf J (Type (max u v))).obj X))

For sheaves of types, the global sections functor is isomorphic to the covariant hom functor of the terminal sheaf.

Equations

• CategoryTheory.Sheaf.ΓNatIsoCoyoneda J X = CategoryTheory.NatIso.ofComponents (fun (F : CategoryTheory.Sheaf J (Type (max ?u.56 ?u.55))) => (CategoryTheory.Sheaf.ΓObjEquivHom J F X).toIso) ⋯