leftHomology_ext

Mathlib.Algebra.Homology.ShortComplex.LeftHomology

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.leftHomology_ext

← MathLib Explorer

English

If S.leftHomologyπ ≫ f1 = S.leftHomologyπ ≫ f2, then f1 = f2.

Русский

Если S.leftHomologyπ ≫ f1 = S.leftHomologyπ ≫ f2, то f1 = f2.

LaTeX

$$$ S.leftHomologyπ \\gg f_1 = S.leftHomologyπ \\gg f_2 \\Rightarrow f_1 = f_2 $$$

Lean4

@[ext]
theorem leftHomology_ext {A : C} (f₁ f₂ : S.leftHomology ⟶ A) (h : S.leftHomologyπ ≫ f₁ = S.leftHomologyπ ≫ f₂) :
    f₁ = f₂ := by simpa only [leftHomology_ext_iff] using h

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru