leftHomologyMap'_comp — Mathlib

English

Composition compatibly respects leftHomology maps: leftHomologyMap' (φ1 ≫ φ2) h1 h3 equals leftHomologyMap φ1 h1 h2 composed with leftHomologyMap' φ2 h2 h3.

Русский

Составление совместимо сохраняет отображения leftHomologyMap': leftHomologyMap' (φ1 ≫ φ2) h1 h3 равно leftHomologyMap' φ1 h1 h2 затем leftHomologyMap' φ2 h2 h3.

LaTeX

$$leftHomologyMap'(φ1 ≫ φ2) h1 h3 = leftHomologyMap'(φ1) h1 h2 ≫ leftHomologyMap'(φ2) h2 h3$$

Lean4

@[reassoc]
theorem leftHomologyMap'_comp (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃) (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData)
    (h₃ : S₃.LeftHomologyData) :
    leftHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = leftHomologyMap' φ₁ h₁ h₂ ≫ leftHomologyMap' φ₂ h₂ h₃ :=
  by
  let γ₁ := leftHomologyMapData φ₁ h₁ h₂
  let γ₂ := leftHomologyMapData φ₂ h₂ h₃
  rw [γ₁.leftHomologyMap'_eq, γ₂.leftHomologyMap'_eq, (γ₁.comp γ₂).leftHomologyMap'_eq, LeftHomologyMapData.comp_φH]

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