leftHomologyπ_naturality — Mathlib

English

The leftHomologyπ morphism is natural with respect to φ: S1.leftHomologyπ ≫ leftHomologyMap φ = cyclesMap φ ≫ S2.leftHomologyπ.

Русский

Гомоморфизм leftHomologyπ натурален по отношению к φ: S1.leftHomologyπ ≫ leftHomologyMap φ = cyclesMap φ ≫ S2.leftHomologyπ.

LaTeX

$$$S_1.\mathrm{leftHomology}\pi \circ leftHomologyMap(\phi) = \mathrm{cyclesMap}(\phi) \circ S_2.\mathrm{leftHomology}\pi$$$

Lean4

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

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