opcyclesMap'_comp — Mathlib

English

The opcyclesMap' is compatible with composition of morphisms φ₁ and φ₂, i.e., opcyclesMap'(φ₁ ≫ φ₂) equals opcyclesMap' φ₁ then opcyclesMap' φ₂.

Русский

opcyclesMap'(φ₁ ≫ φ₂) = opcyclesMap' φ₁ ∘ opcyclesMap' φ₂.

LaTeX

$$$opcyclesMap' (φ_1 ≫ φ_2) h_1 h_3 = opcyclesMap' φ_1 h_1 h_2 ≫ opcyclesMap' φ_2 h_2 h_3$$$

Lean4

@[reassoc]
theorem opcyclesMap'_comp (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData)
    (h₃ : S₃.RightHomologyData) : opcyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = opcyclesMap' φ₁ h₁ h₂ ≫ opcyclesMap' φ₂ h₂ h₃ :=
  by
  let γ₁ := rightHomologyMapData φ₁ h₁ h₂
  let γ₂ := rightHomologyMapData φ₂ h₂ h₃
  rw [γ₁.opcyclesMap'_eq, γ₂.opcyclesMap'_eq, (γ₁.comp γ₂).opcyclesMap'_eq, RightHomologyMapData.comp_φQ]

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