plusLift_unique — Mathlib

English

If a morphism γ: J.plusObj P → Q satisfies J.toPlus P ≫ γ = η for some η: P → Q, then γ is uniquely determined by η via plusLift; namely, γ = J.plusLift η hQ.

Русский

Если φ: J.plusObj P → Q удовлетворяет J.toPlus P ≫ φ = η, то φ уникально задаётся через plusLift: φ = J.plusLift η hQ.

LaTeX

$$$ J.toPlus P \\circ γ = η \\Rightarrow γ = J.plusLift η h_Q $$$

Lean4

theorem plusLift_unique {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (hQ : Presheaf.IsSheaf J Q) (γ : J.plusObj P ⟶ Q)
    (hγ : J.toPlus P ≫ γ = η) : γ = J.plusLift η hQ :=
  by
  dsimp only [plusLift]
  rw [Iso.eq_comp_inv, ← hγ, plusMap_comp]
  simp

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