leftHomologyπ_naturality' — Mathlib

English

Naturality of the left homology projection with respect to a morphism φ: h1.π followed by leftHomologyMap' equals cyclesMap' followed by h2.π.

Русский

Натуральность проекции левой гомологии по отношению к отображению φ: h1.π затем leftHomologyMap' равно cyclesMap' затем h2.π.

LaTeX

$$$h_1.\pi \circ leftHomologyMap'(\phi,h_1,h_2) = cyclesMap'(\phi,h_1,h_2) \circ h_2.\pi$$$

Lean4

@[reassoc (attr := simp)]
theorem leftHomologyπ_naturality' : h₁.π ≫ leftHomologyMap' φ h₁ h₂ = cyclesMap' φ h₁ h₂ ≫ h₂.π :=
  LeftHomologyMapData.commπ _

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