sheafifyLift_unique — Mathlib

English

Given η, hQ, and γ : sheafify J P ⟶ Q, if toSheafify J P ≫ γ = η then γ = sheafifyLift J η hQ.

Русский

Если для отображений в композиции число равенств, то существует единственный lift.

LaTeX

$$toSheafify J P ≫ γ = η \Rightarrow γ = \mathrm{sheafifyLift} J η hQ$$

Lean4

theorem sheafifyLift_unique {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (hQ : Presheaf.IsSheaf J Q) (γ : sheafify J P ⟶ Q) :
    toSheafify J P ≫ γ = η → γ = sheafifyLift J η hQ := by
  intro h
  rw [toSheafify] at h
  rw [sheafifyLift]
  let γ' : (presheafToSheaf J D).obj P ⟶ ⟨Q, hQ⟩ := ⟨γ⟩
  change γ'.val = _
  rw [← Sheaf.Hom.ext_iff, ← Adjunction.homEquiv_apply_eq, Adjunction.homEquiv_unit]
  exact h

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