noncomputable def Proposition15.sheafification_adjunction (X : TopCat) : CategoryTheory.presheafToSheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat ⊣ CategoryTheory.sheafToPresheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat

The sheafification adjunction: presheafification ⊣ inclusion of sheaves into presheaves, instantiated for abelian-group-valued (pre)sheaves on a topological space X.

theorem Proposition15.sheafification_isLeftAdjoint (X : TopCat) : (CategoryTheory.presheafToSheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat).IsLeftAdjoint

The sheafification functor is a left adjoint (instance form).

theorem Proposition15.sheafification_universal_factorization {C : Type u} [CategoryTheory.Category.{u, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{u, u_1} D] [CategoryTheory.HasWeakSheafify J D] {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q) : CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J P) (CategoryTheory.sheafifyLift J η hQ) = η

Universal property of sheafification (existence): any morphism η : P → Q to a sheaf Q factors through the sheafification map P → P⁺ via sheafifyLift.

theorem Proposition15.sheafification_universal_uniqueness {C : Type u} [CategoryTheory.Category.{u, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{u, u_1} D] [CategoryTheory.HasWeakSheafify J D] {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q) (γ : CategoryTheory.sheafify J P ⟶ Q) (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J P) γ = η) : γ = CategoryTheory.sheafifyLift J η hQ

Universal property of sheafification (uniqueness): the factorization through the sheafification is unique.

theorem Proposition15.sheafification_iso_of_isSheaf {C : Type u} [CategoryTheory.Category.{u, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{u, u_1} D] [CategoryTheory.HasWeakSheafify J D] {P : CategoryTheory.Functor Cᵒᵖ D} (hP : CategoryTheory.Presheaf.IsSheaf J P) : CategoryTheory.IsIso (CategoryTheory.toSheafify J P)

A presheaf that is already a sheaf is isomorphic to its sheafification.

theorem Proposition15.sheafification_exact (X : TopCat) : (CategoryTheory.presheafToSheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat).PreservesHomology

Exactness of sheafification: the sheafification functor preserves homology (equivalently, finite limits and finite colimits) on abelian-group-valued presheaves.

theorem Proposition15.stalkFunctor_preservesHomology (X : TopCat) (x : ↑X) : ((TopCat.Sheaf.forget AddCommGrpCat X).comp (TopCat.Presheaf.stalkFunctor AddCommGrpCat x)).PreservesHomology

The composition "take underlying presheaf, then take stalk at x" preserves homology. This is what makes "exactness can be checked on stalks" work for sheaves of abelian groups.

theorem Proposition15.exact_iff_stalkwise_exact (X : TopCat) (S : CategoryTheory.ShortComplex (TopCat.Sheaf AddCommGrpCat X)) : S.Exact ↔ ∀ (x : ↑X), (S.map ((TopCat.Sheaf.forget AddCommGrpCat X).comp (TopCat.Presheaf.stalkFunctor AddCommGrpCat x))).Exact

Exactness on stalks: a short complex of sheaves of abelian groups on X is exact if and only if its stalk at every x ∈ X is exact.