plus_hom_ext — Mathlib

English

If two arrows η, γ : J.plusObj P → Q satisfy J.toPlus P ≫ η = J.toPlus P ≫ γ, then η = γ; i.e., the plus-extension is faithful on arrows from P⁺.

Русский

Если два морфизма η, γ : J.plusObj P → Q удовлетворяют J.toPlus P ≫ η = J.toPlus P ≫ γ, то η = γ; то есть плюс-расширение верно по стрелам из P⁺.

LaTeX

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

Lean4

theorem plus_hom_ext {P Q : Cᵒᵖ ⥤ D} (η γ : J.plusObj P ⟶ Q) (hQ : Presheaf.IsSheaf J Q)
    (h : J.toPlus P ≫ η = J.toPlus P ≫ γ) : η = γ :=
  by
  have : γ = J.plusLift (J.toPlus P ≫ γ) hQ := by
    apply plusLift_unique
    rfl
  rw [this]
  apply plusLift_unique
  exact h

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