sheafify_hom_ext — Mathlib

English

A two-hom extension property: if equalities of compositions hold, then the two morphisms are equal.

Русский

Свойство уникальности гомоморфизмов: равенства композиции влекут равенство морфизмов.

LaTeX

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

Lean4

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

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