cyclesMap'_comp — Mathlib

English

The composition of cycles maps respects composition: cyclesMap'(φ1 ≫ φ2) h1 h3 equals cyclesMap'(φ1) h1 h2 composed with cyclesMap'(φ2) h2 h3.

Русский

Составление циклических отображений сохраняет композицию: cyclesMap'(φ1 ≫ φ2) h1 h3 равно cyclesMap'(φ1) h1 h2 затем cyclesMap'(φ2) h2 h3.

LaTeX

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

Lean4

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

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