sheafify_hom_ext — Mathlib

English

If two morphisms η, γ : P ⟶ Q between sheaves become equal after postcomposing with toSheafify, then they are equal after precomposition with toSheafify.

Русский

Если две морфизмы совпадают после композиции с toSheafify, то они совпадают до композиции с toSheafify.

LaTeX

$$toSheafify J P ≫ η = toSheafify J P ≫ γ ⟹ η = γ$$

Lean4

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

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