Coconstant sheaves

In this file we define a coconstant sheaf functor A ⥤ Sheaf J A as a right adjoint to the global sections functor Γ : Sheaf J A ⥤ A when one exists.

@[reducible, inline]

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

Typeclass stating that the global sections functor has a right adjoint. This right adjoint will then be called the coconstant sheaf functor and written coconstantSheaf J A.

Equations

• CategoryTheory.HasCoconstantSheaf J A = (CategoryTheory.Sheaf.Γ J A).IsLeftAdjoint

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

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

Equations

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

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

The global sections functor is by definition left-adjoint to the coconstant sheaf functor whenever both exist.

Equations

• CategoryTheory.ΓCoconstantSheafAdj J A = CategoryTheory.Adjunction.ofIsLeftAdjoint (CategoryTheory.Sheaf.Γ J A)

instance CategoryTheory.instIsRightAdjointSheafCoconstantSheaf {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u₂) [Category.{v₂, u₂} A] [HasWeakSheafify J A] [HasGlobalSectionsFunctor J A] [HasCoconstantSheaf J A] : (coconstantSheaf J A).IsRightAdjoint

noncomputable def CategoryTheory.Sheaf.constΓCoconstTriple {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u₂) [Category.{v₂, u₂} A] [HasWeakSheafify J A] [HasGlobalSectionsFunctor J A] [HasCoconstantSheaf J A] : Adjunction.Triple (constantSheaf J A) (Γ J A) (coconstantSheaf J A)

Equations

• CategoryTheory.Sheaf.constΓCoconstTriple J A = { adj₁ := CategoryTheory.constantSheafΓAdj J A, adj₂ := CategoryTheory.ΓCoconstantSheafAdj J A }

instance CategoryTheory.instFullSheafCoconstantSheafOfFaithfulConstantSheaf {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u₂) [Category.{v₂, u₂} A] [HasWeakSheafify J A] [HasGlobalSectionsFunctor J A] [HasCoconstantSheaf J A] [(constantSheaf J A).Full] [(constantSheaf J A).Faithful] : (coconstantSheaf J A).Full

instance CategoryTheory.instFaithfulSheafCoconstantSheafOfFullOfConstantSheaf {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u₂) [Category.{v₂, u₂} A] [HasWeakSheafify J A] [HasGlobalSectionsFunctor J A] [HasCoconstantSheaf J A] [(constantSheaf J A).Full] [(constantSheaf J A).Faithful] : (coconstantSheaf J A).Faithful