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).

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).toPrefunctor.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.

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.comp (CategoryTheory.Functor.const Cᵒᵖ) (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).toPrefunctor.obj (Opposite.op T)

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

Equations

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