sheafifyLift_unique — Mathlib

English

If two morphisms η, γ : J.sheafify P ⟶ Q agree after composing with the canonical map, then η = γ.

Русский

Если два морфизма η, γ : J.sheafify P ⟶ Q совпадают после композиции с каноническим отображением, то η = γ.

LaTeX

$$sheafify_hom_ext {P Q} (η γ) (hQ) (h) : (J.toSheafify P ≫ η = J.toSheafify P ≫ γ) → η = γ$$

Lean4

theorem sheafifyLift_unique {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (hQ : Presheaf.IsSheaf J Q) (γ : J.sheafify P ⟶ Q) :
    J.toSheafify P ≫ γ = η → γ = sheafifyLift J η hQ := by
  intro h
  apply plusLift_unique
  apply plusLift_unique
  rw [← Category.assoc, ← plusMap_toPlus]
  exact h

Похожие утверждения