cyclesMap'_eq

Mathlib.Algebra.Homology.ShortComplex.LeftHomology

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.LeftHomologyMapData.cyclesMap'_eq

English

For a LeftHomologyMapData γ, cyclesMap' φ h1 h2 equals γ.φK.

Русский

Для данных LeftHomologyMapData γ, cyclesMap'(φ,h1,h2) равно γ.φK.

LaTeX

$$cyclesMap'(\phi,h_1,h_2) = γ.φK$$

Lean4

theorem cyclesMap'_eq : cyclesMap' φ h₁ h₂ = γ.φK :=
  LeftHomologyMapData.congr_φK (Subsingleton.elim _ _)

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

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

Разделы

Аффилиация

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