The constant sheaf

We define the constant sheaf functor (the sheafification of the constant presheaf) constantSheaf : D ⥤ Sheaf J D and prove that it is left adjoint to evaluation at a terminal object (see constantSheafAdj).

We also define a predicate on sheaves, Sheaf.IsConstant, saying that a sheaf is in the essential image of the constant sheaf functor.

Main results

• Sheaf.isConstant_iff_isIso_counit_app: Provided that the constant sheaf functor is fully faithful, a sheaf is constant if and only if the counit of the constant sheaf adjunction applied to it is an isomorphism.

• Sheaf.isConstant_iff_of_equivalence : The property of a sheaf of being constant is invariant under equivalence of sheaf categories.

• Sheaf.isConstant_iff_forget : Given a "forgetful" functor U : D ⥤ B a sheaf F : Sheaf J D is constant if and only if the sheaf given by postcomposition with U is constant.

noncomputable def CategoryTheory.constantPresheafAdj {C : Type u_1} [Category.{u_3, u_1} C] (D : Type u_2) [Category.{u_4, u_2} D] {T : C} (hT : Limits.IsTerminal T) : Functor.const Cᵒᵖ ⊣ (evaluation Cᵒᵖ D).obj (Opposite.op T)

The constant presheaf functor is left adjoint to evaluation at a terminal object.

Equations

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

@[simp]

theorem CategoryTheory.constantPresheafAdj_unit_app {C : Type u_1} [Category.{u_3, u_1} C] (D : Type u_2) [Category.{u_4, u_2} D] {T : C} (hT : Limits.IsTerminal T) (X : D) : (constantPresheafAdj D hT).unit.app X = CategoryStruct.id X

@[simp]

theorem CategoryTheory.constantPresheafAdj_counit_app_app {C : Type u_1} [Category.{u_3, u_1} C] (D : Type u_2) [Category.{u_4, u_2} D] {T : C} (hT : Limits.IsTerminal T) (F : Functor Cᵒᵖ D) (x✝ : Cᵒᵖ) : ((constantPresheafAdj D hT).counit.app F).app x✝ = F.map (hT.from (Opposite.unop x✝)).op

noncomputable def CategoryTheory.constantSheaf {C : Type u_1} [Category.{u_3, u_1} C] (J : GrothendieckTopology C) (D : Type u_2) [Category.{u_4, u_2} D] [HasWeakSheafify J D] : Functor D (Sheaf J D)

The functor which maps an object of D to the constant sheaf at that object, i.e. the sheafification of the constant presheaf.

Equations

• CategoryTheory.constantSheaf J D = (CategoryTheory.Functor.const Cᵒᵖ).comp (CategoryTheory.presheafToSheaf J D)

noncomputable def CategoryTheory.constantSheafAdj {C : Type u_1} [Category.{u_3, u_1} C] (J : GrothendieckTopology C) (D : Type u_2) [Category.{u_4, u_2} D] [HasWeakSheafify J D] {T : C} (hT : Limits.IsTerminal T) : constantSheaf J D ⊣ (sheafSections J D).obj (Opposite.op T)

The constant sheaf functor is left adjoint to evaluation at a terminal object.

Equations

• CategoryTheory.constantSheafAdj J D hT = (CategoryTheory.constantPresheafAdj D hT).comp (CategoryTheory.sheafificationAdjunction J D)

@[simp]

theorem CategoryTheory.constantSheafAdj_counit_app {C : Type u_1} [Category.{u_3, u_1} C] (J : GrothendieckTopology C) (D : Type u_2) [Category.{u_4, u_2} D] [HasWeakSheafify J D] {T : C} (hT : Limits.IsTerminal T) (X : Sheaf J D) : (constantSheafAdj J D hT).counit.app X = CategoryStruct.comp ((presheafToSheaf J D).map ((constantPresheafAdj D hT).counit.app X.val)) ((sheafificationAdjunction J D).counit.app X)

class CategoryTheory.Sheaf.IsConstant {C : Type u_1} [Category.{u_3, u_1} C] (J : GrothendieckTopology C) {D : Type u_2} [Category.{u_4, u_2} D] [HasWeakSheafify J D] (F : Sheaf J D) : Prop

A sheaf is constant if it is in the essential image of the constant sheaf functor.

• mem_essImage : F ∈ (constantSheaf J D).essImage

theorem CategoryTheory.Sheaf.mem_essImage_of_isConstant {C : Type u_1} [Category.{u_3, u_1} C] (J : GrothendieckTopology C) {D : Type u_2} [Category.{u_4, u_2} D] [HasWeakSheafify J D] (F : Sheaf J D) [IsConstant J F] : F ∈ (constantSheaf J D).essImage

theorem CategoryTheory.Sheaf.isConstant_congr {C : Type u_1} [Category.{u_3, u_1} C] (J : GrothendieckTopology C) {D : Type u_2} [Category.{u_4, u_2} D] [HasWeakSheafify J D] {F G : Sheaf J D} (i : F ≅ G) [IsConstant J F] : IsConstant J G

theorem CategoryTheory.Sheaf.isConstant_of_iso {C : Type u_1} [Category.{u_3, u_1} C] (J : GrothendieckTopology C) {D : Type u_2} [Category.{u_4, u_2} D] [HasWeakSheafify J D] {F : Sheaf J D} {X : D} (i : F ≅ (constantSheaf J D).obj X) : IsConstant J F

theorem CategoryTheory.Sheaf.isConstant_iff_mem_essImage {C : Type u_1} [Category.{u_4, u_1} C] (J : GrothendieckTopology C) {D : Type u_2} [Category.{u_3, u_2} D] [HasWeakSheafify J D] {L : Functor D (Sheaf J D)} {T : C} (hT : Limits.IsTerminal T) (adj : L ⊣ (sheafSections J D).obj (Opposite.op T)) (F : Sheaf J D) : IsConstant J F ↔ F ∈ L.essImage

theorem CategoryTheory.Sheaf.isConstant_of_isIso_counit_app {C : Type u_1} [Category.{u_3, u_1} C] (J : GrothendieckTopology C) {D : Type u_2} [Category.{u_4, u_2} D] [HasWeakSheafify J D] (F : Sheaf J D) [Limits.HasTerminal C] [IsIso ((constantSheafAdj J D Limits.terminalIsTerminal).counit.app F)] : IsConstant J F

instance CategoryTheory.Sheaf.instIsIsoAppCounitConstantSheafAdjOfFaithfulOfFullConstantSheafOfIsConstant {C : Type u_1} [Category.{u_4, u_1} C] (J : GrothendieckTopology C) {D : Type u_2} [Category.{u_3, u_2} D] [HasWeakSheafify J D] [(constantSheaf J D).Faithful] [(constantSheaf J D).Full] (F : Sheaf J D) [IsConstant J F] {T : C} (hT : Limits.IsTerminal T) : IsIso ((constantSheafAdj J D hT).counit.app F)

theorem CategoryTheory.Sheaf.isConstant_iff_isIso_counit_app {C : Type u_1} [Category.{u_4, u_1} C] (J : GrothendieckTopology C) {D : Type u_2} [Category.{u_3, u_2} D] [HasWeakSheafify J D] [(constantSheaf J D).Faithful] [(constantSheaf J D).Full] (F : Sheaf J D) {T : C} (hT : Limits.IsTerminal T) : IsConstant J F ↔ IsIso ((constantSheafAdj J D hT).counit.app F)

If the constant sheaf functor is fully faithful, then a sheaf is constant if and only if the counit of the constant sheaf adjunction applied to it is an isomorphism.

theorem CategoryTheory.Sheaf.isConstant_iff_isIso_counit_app' {C : Type u_1} [Category.{u_4, u_1} C] (J : GrothendieckTopology C) {D : Type u_2} [Category.{u_3, u_2} D] [HasWeakSheafify J D] {L : Functor D (Sheaf J D)} {T : C} (hT : Limits.IsTerminal T) (adj : L ⊣ (sheafSections J D).obj (Opposite.op T)) [L.Faithful] [L.Full] (F : Sheaf J D) : IsConstant J F ↔ IsIso (adj.counit.app F)

A variant of isConstant_iff_isIso_counit_app for a general left adjoint to evaluation at a terminal object.

noncomputable def CategoryTheory.equivCommuteConstant {C : Type u_1} [Category.{u_4, u_1} C] (J : GrothendieckTopology C) (D : Type u_2) [Category.{u_5, u_2} D] [HasWeakSheafify J D] {C' : Type u_3} [Category.{u_6, u_3} C'] (K : GrothendieckTopology C') [HasWeakSheafify K D] (G : Functor C C') [∀ (X : C'ᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) D] [Functor.IsDenseSubsite J K G] {T : C} (hT : Limits.IsTerminal T) (hT' : Limits.IsTerminal (G.obj T)) : (constantSheaf J D).comp (Functor.IsDenseSubsite.sheafEquiv G J K D).functor ≅ constantSheaf K D

The constant sheaf functor commutes up to isomorphism the equivalence of sheaf categories induced by a dense subsite.

Equations

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

noncomputable def CategoryTheory.equivCommuteConstant' {C : Type u_1} [Category.{u_4, u_1} C] (J : GrothendieckTopology C) (D : Type u_2) [Category.{u_5, u_2} D] [HasWeakSheafify J D] {C' : Type u_3} [Category.{u_6, u_3} C'] (K : GrothendieckTopology C') [HasWeakSheafify K D] (G : Functor C C') [∀ (X : C'ᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) D] [Functor.IsDenseSubsite J K G] {T : C} (hT : Limits.IsTerminal T) (hT' : Limits.IsTerminal (G.obj T)) : constantSheaf J D ≅ (constantSheaf K D).comp (Functor.IsDenseSubsite.sheafEquiv G J K D).inverse

The constant sheaf functor commutes up to isomorphism the inverse equivalence of sheaf categories induced by a dense subsite.

Equations

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

theorem CategoryTheory.Sheaf.isConstant_iff_of_equivalence {C : Type u_1} [Category.{u_6, u_1} C] (J : GrothendieckTopology C) {D : Type u_2} [Category.{u_5, u_2} D] [HasWeakSheafify J D] {C' : Type u_3} [Category.{u_4, u_3} C'] (K : GrothendieckTopology C') [HasWeakSheafify K D] (G : Functor C C') [∀ (X : C'ᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) D] [Functor.IsDenseSubsite J K G] {T : C} (hT : Limits.IsTerminal T) (hT' : Limits.IsTerminal (G.obj T)) (F : Sheaf K D) : IsConstant J ((Functor.IsDenseSubsite.sheafEquiv G J K D).inverse.obj F) ↔ IsConstant K F

The property of a sheaf of being constant is invariant under equivalence of sheaf categories.

noncomputable def CategoryTheory.constantCommuteCompose {C : Type u_1} [Category.{u_4, u_1} C] (J : GrothendieckTopology C) {D : Type u_2} [Category.{u_5, u_2} D] [HasWeakSheafify J D] {B : Type u_3} [Category.{u_6, u_3} B] (U : Functor D B) [HasWeakSheafify J B] [J.PreservesSheafification U] [J.HasSheafCompose U] : (constantSheaf J D).comp (sheafCompose J U) ≅ U.comp (constantSheaf J B)

The constant sheaf functor commutes with sheafCompose J U up to isomorphism, provided that U preserves sheafification.

Equations

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

theorem CategoryTheory.constantCommuteCompose_hom_app_val {C : Type u_1} [Category.{u_5, u_1} C] (J : GrothendieckTopology C) {D : Type u_2} [Category.{u_6, u_2} D] [HasWeakSheafify J D] {B : Type u_3} [Category.{u_4, u_3} B] (U : Functor D B) [HasWeakSheafify J B] [J.PreservesSheafification U] [J.HasSheafCompose U] (X : D) : ((constantCommuteCompose J U).hom.app X).val = CategoryStruct.comp (sheafifyComposeIso J U ((Functor.const Cᵒᵖ).obj X)).inv (sheafifyMap J (Functor.constComp Cᵒᵖ X U).hom)

theorem CategoryTheory.constantSheafAdj_counit_w {C : Type u_1} [Category.{u_4, u_1} C] (J : GrothendieckTopology C) {D : Type u_2} [Category.{u_6, u_2} D] [HasWeakSheafify J D] {B : Type u_3} [Category.{u_5, u_3} B] (U : Functor D B) [HasWeakSheafify J B] [J.PreservesSheafification U] [J.HasSheafCompose U] (F : Sheaf J D) {T : C} (hT : Limits.IsTerminal T) : CategoryStruct.comp ((constantCommuteCompose J U).hom.app (F.val.obj (Opposite.op T))) ((constantSheafAdj J B hT).counit.app ((sheafCompose J U).obj F)) = (sheafCompose J U).map ((constantSheafAdj J D hT).counit.app F)

The counit of constantSheafAdj factors through the isomorphism constantCommuteCompose.

theorem CategoryTheory.Sheaf.isConstant_of_forget {C : Type u_1} [Category.{u_5, u_1} C] (J : GrothendieckTopology C) {D : Type u_2} [Category.{u_4, u_2} D] [HasWeakSheafify J D] {B : Type u_3} [Category.{u_6, u_3} B] (U : Functor D B) [HasWeakSheafify J B] [J.PreservesSheafification U] [J.HasSheafCompose U] (F : Sheaf J D) [(constantSheaf J D).Faithful] [(constantSheaf J D).Full] [(constantSheaf J B).Faithful] [(constantSheaf J B).Full] [(sheafCompose J U).ReflectsIsomorphisms] [IsConstant J ((sheafCompose J U).obj F)] {T : C} (hT : Limits.IsTerminal T) : IsConstant J F

instance CategoryTheory.instIsConstantObjSheafSheafCompose {C : Type u_1} [Category.{u_4, u_1} C] (J : GrothendieckTopology C) {D : Type u_2} [Category.{u_5, u_2} D] [HasWeakSheafify J D] {B : Type u_3} [Category.{u_6, u_3} B] (U : Functor D B) [HasWeakSheafify J B] [J.PreservesSheafification U] [J.HasSheafCompose U] (F : Sheaf J D) [h : Sheaf.IsConstant J F] : Sheaf.IsConstant J ((sheafCompose J U).obj F)

theorem CategoryTheory.Sheaf.isConstant_iff_forget {C : Type u_1} [Category.{u_5, u_1} C] (J : GrothendieckTopology C) {D : Type u_2} [Category.{u_4, u_2} D] [HasWeakSheafify J D] {B : Type u_3} [Category.{u_6, u_3} B] (U : Functor D B) [HasWeakSheafify J B] [J.PreservesSheafification U] [J.HasSheafCompose U] (F : Sheaf J D) [(constantSheaf J D).Faithful] [(constantSheaf J D).Full] [(constantSheaf J B).Faithful] [(constantSheaf J B).Full] [(sheafCompose J U).ReflectsIsomorphisms] {T : C} (hT : Limits.IsTerminal T) : IsConstant J F ↔ IsConstant J ((sheafCompose J U).obj F)