CategoryTheory.sheafifyLift_unique

theorem CategoryTheory.sheafifyLift_unique : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [inst_1 : CategoryTheory.Category.{u_2, u_1} D] [inst_2 : CategoryTheory.HasWeakSheafify J D] {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q) (γ : CategoryTheory.sheafify J P ⟶ Q), CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J P) γ = η → γ = CategoryTheory.sheafifyLift J η hQ

The theorem `CategoryTheory.sheafifyLift_unique` states that for any category type `C` with the category instance `inst`, Grothendieck topology `J`, category type `D` with the category instance `inst_1`, and the condition `inst_2` that the inclusion functor from sheaves to presheaves admits a left adjoint, given functors `P` and `Q` from the opposite of `C` to `D`, a natural transformation `η` from `P` to `Q`, where `Q` is a sheaf for the topology `J` and a natural transformation `γ` from the sheafification of `P` to `Q`. The theorem asserts that if the composition of the canonical map from `P` to its sheafification and `γ` equals `η`, then `γ` is equal to the lift of `η` to the sheafification of `P`. In other words, the lift of `η` is the unique morphism making the diagram commute if `Q` is a sheaf.

More concisely: Given a category `C` with instance `inst`, Grothendieck topology `J`, category `D` with instance `inst_1`, and functors `P` and `Q` from `C°` to `D`, if `η: P ⟶ Q` is a natural transformation with `γ: Sh(P) ⟶ Q` such that the composition `P ➔ Sh(P) ⟶ Q` equals `η`, then `γ` is the lift of `η` to `Sh(P)`.