rightHomologyMap'_comp — Mathlib

English

The rightHomologyMap' is compatible with composition: for φ₁, φ₂, the map for φ₁ ≫ φ₂ equals the composition of the maps for φ₁ and φ₂.

Русский

RightHomologyMap' совместим с построением по композиции: отображение для φ₁ ≫ φ₂ равно композиции отображений для φ₁ и φ₂.

LaTeX

$$$rightHomologyMap' (φ_1 \gg φ_2) h_1 h_3 = rightHomologyMap' φ_1 h_1 h_2 \gg rightHomologyMap' φ_2 h_2 h_3$$$

Lean4

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

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