leftHomologyMap'_eq

Mathlib.Algebra.Homology.ShortComplex.LeftHomology

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

English

For a given LeftHomologyMapData γ, the morphism leftHomologyMap' φ h1 h2 equals γ.φH.

Русский

Для данного данных LeftHomologyMapData γ отображение leftHomologyMap' φ h1 h2 равно γ.φH.

LaTeX

$$leftHomologyMap'(\phi,h_1,h_2) = γ.φH$$

Lean4

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

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

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

Разделы

Аффилиация

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