rightHomology_ext_iff — Mathlib

English

For any A, f1, f2: A → S.rightHomology, f1 = f2 iff f1 ≫ S.rightHomologyι = f2 ≫ S.rightHomologyι.

Русский

Для любых A, f1, f2: A → S.rightHomology, f1 = f2 тогда и только тогда, когда f1 ≫ S.rightHomologyι = f2 ≫ S.rightHomologyι.

LaTeX

$$$ f_1 = f_2 \iff f_1 \circ S.rightHomology\iota = f_2 \circ S.rightHomology\iota $$$

Lean4

theorem rightHomology_ext_iff {A : C} (f₁ f₂ : A ⟶ S.rightHomology) :
    f₁ = f₂ ↔ f₁ ≫ S.rightHomologyι = f₂ ≫ S.rightHomologyι := by rw [cancel_mono]

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