cycles_ext

Mathlib.Algebra.Homology.ShortComplex.LeftHomology

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

English

If f1 ≫ iCycles = f2 ≫ iCycles, then f1 = f2.

Русский

Если f1 ≫ iCycles = f2 ≫ iCycles, тогда f1 = f2.

LaTeX

$$$ (f_1 \\circ iCycles) = (f_2 \\circ iCycles) \\Rightarrow f_1 = f_2 $$$

Lean4

@[ext]
theorem cycles_ext {A : C} (f₁ f₂ : A ⟶ S.cycles) (h : f₁ ≫ S.iCycles = f₂ ≫ S.iCycles) : f₁ = f₂ := by
  simpa only [cycles_ext_iff] using h

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

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

Разделы

Аффилиация

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