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} [CategoryTheory.Category.{u_3, u_1} C] (D : Type u_2) [CategoryTheory.Category.{u_4, u_2} D] {T : C} (hT : CategoryTheory.Limits.IsTerminal T) : CategoryTheory.Functor.const Cᵒᵖ ⊣ (CategoryTheory.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} [CategoryTheory.Category.{u_3, u_1} C] (D : Type u_2) [CategoryTheory.Category.{u_4, u_2} D] {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (X : D) : (CategoryTheory.constantPresheafAdj D hT).unit.app X = CategoryTheory.CategoryStruct.id X

@[simp]

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

noncomputable def CategoryTheory.constantSheaf {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type u_2) [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.HasWeakSheafify J D] : CategoryTheory.Functor D (CategoryTheory.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} [CategoryTheory.Category.{u_3, u_1} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type u_2) [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.HasWeakSheafify J D] {T : C} (hT : CategoryTheory.Limits.IsTerminal T) : CategoryTheory.constantSheaf J D ⊣ (CategoryTheory.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} [CategoryTheory.Category.{u_3, u_1} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type u_2) [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.HasWeakSheafify J D] {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (X : CategoryTheory.Sheaf J D) : (CategoryTheory.constantSheafAdj J D hT).counit.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.presheafToSheaf J D).map ((CategoryTheory.constantPresheafAdj D hT).counit.app X.val)) ((CategoryTheory.sheafificationAdjunction J D).counit.app X)

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

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

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

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

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

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

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

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

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

Equations

• ⋯ = ⋯

theorem CategoryTheory.Sheaf.isConstant_iff_isIso_counit_app {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.HasWeakSheafify J D] [(CategoryTheory.constantSheaf J D).Faithful] [(CategoryTheory.constantSheaf J D).Full] (F : CategoryTheory.Sheaf J D) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) : CategoryTheory.Sheaf.IsConstant J F ↔ CategoryTheory.IsIso ((CategoryTheory.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} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.HasWeakSheafify J D] {L : CategoryTheory.Functor D (CategoryTheory.Sheaf J D)} {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (adj : L ⊣ (CategoryTheory.sheafSections J D).obj (Opposite.op T)) [L.Faithful] [L.Full] (F : CategoryTheory.Sheaf J D) : CategoryTheory.Sheaf.IsConstant J F ↔ CategoryTheory.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} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type u_2) [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasWeakSheafify J D] {C' : Type u_3} [CategoryTheory.Category.{u_6, u_3} C'] (K : CategoryTheory.GrothendieckTopology C') [CategoryTheory.HasWeakSheafify K D] (G : CategoryTheory.Functor C C') [∀ (X : C'ᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) D] [CategoryTheory.Functor.IsDenseSubsite J K G] {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (hT' : CategoryTheory.Limits.IsTerminal (G.obj T)) : (CategoryTheory.constantSheaf J D).comp (CategoryTheory.Functor.IsDenseSubsite.sheafEquiv G J K D).functor ≅ CategoryTheory.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} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type u_2) [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasWeakSheafify J D] {C' : Type u_3} [CategoryTheory.Category.{u_6, u_3} C'] (K : CategoryTheory.GrothendieckTopology C') [CategoryTheory.HasWeakSheafify K D] (G : CategoryTheory.Functor C C') [∀ (X : C'ᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) D] [CategoryTheory.Functor.IsDenseSubsite J K G] {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (hT' : CategoryTheory.Limits.IsTerminal (G.obj T)) : CategoryTheory.constantSheaf J D ≅ (CategoryTheory.constantSheaf K D).comp (CategoryTheory.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} [CategoryTheory.Category.{u_6, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasWeakSheafify J D] {C' : Type u_3} [CategoryTheory.Category.{u_4, u_3} C'] (K : CategoryTheory.GrothendieckTopology C') [CategoryTheory.HasWeakSheafify K D] (G : CategoryTheory.Functor C C') [∀ (X : C'ᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) D] [CategoryTheory.Functor.IsDenseSubsite J K G] {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (hT' : CategoryTheory.Limits.IsTerminal (G.obj T)) (F : CategoryTheory.Sheaf K D) : CategoryTheory.Sheaf.IsConstant J ((CategoryTheory.Functor.IsDenseSubsite.sheafEquiv G J K D).inverse.obj F) ↔ CategoryTheory.Sheaf.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} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasWeakSheafify J D] {B : Type u_3} [CategoryTheory.Category.{u_6, u_3} B] (U : CategoryTheory.Functor D B) [CategoryTheory.HasWeakSheafify J B] [J.PreservesSheafification U] [J.HasSheafCompose U] : (CategoryTheory.constantSheaf J D).comp (CategoryTheory.sheafCompose J U) ≅ U.comp (CategoryTheory.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} [CategoryTheory.Category.{u_5, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{u_6, u_2} D] [CategoryTheory.HasWeakSheafify J D] {B : Type u_3} [CategoryTheory.Category.{u_4, u_3} B] (U : CategoryTheory.Functor D B) [CategoryTheory.HasWeakSheafify J B] [J.PreservesSheafification U] [J.HasSheafCompose U] (X : D) : ((CategoryTheory.constantCommuteCompose J U).hom.app X).val = CategoryTheory.CategoryStruct.comp (CategoryTheory.sheafifyComposeIso J U ((CategoryTheory.Functor.const Cᵒᵖ).obj X)).inv (CategoryTheory.sheafifyMap J (CategoryTheory.Functor.constComp Cᵒᵖ X U).hom)

theorem CategoryTheory.constantSheafAdj_counit_w {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{u_6, u_2} D] [CategoryTheory.HasWeakSheafify J D] {B : Type u_3} [CategoryTheory.Category.{u_5, u_3} B] (U : CategoryTheory.Functor D B) [CategoryTheory.HasWeakSheafify J B] [J.PreservesSheafification U] [J.HasSheafCompose U] (F : CategoryTheory.Sheaf J D) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.constantCommuteCompose J U).hom.app (F.val.obj (Opposite.op T))) ((CategoryTheory.constantSheafAdj J B hT).counit.app ((CategoryTheory.sheafCompose J U).obj F)) = (CategoryTheory.sheafCompose J U).map ((CategoryTheory.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} [CategoryTheory.Category.{u_5, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.HasWeakSheafify J D] {B : Type u_3} [CategoryTheory.Category.{u_6, u_3} B] (U : CategoryTheory.Functor D B) [CategoryTheory.HasWeakSheafify J B] [J.PreservesSheafification U] [J.HasSheafCompose U] (F : CategoryTheory.Sheaf J D) [(CategoryTheory.constantSheaf J D).Faithful] [(CategoryTheory.constantSheaf J D).Full] [(CategoryTheory.constantSheaf J B).Faithful] [(CategoryTheory.constantSheaf J B).Full] [(CategoryTheory.sheafCompose J U).ReflectsIsomorphisms] [CategoryTheory.Sheaf.IsConstant J ((CategoryTheory.sheafCompose J U).obj F)] {T : C} (hT : CategoryTheory.Limits.IsTerminal T) : CategoryTheory.Sheaf.IsConstant J F

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

Equations

• ⋯ = ⋯

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