cyclesMap_comp_isoCycles₂_hom — Mathlib

English

Composition of maps f and g yields the expected composition on H2: mapShortComplexH2 (g ∘ f) (φ ≫ (Res f).map ψ) equals (mapShortComplexH2 f φ) ≫ (mapShortComplexH2 g ψ).

Русский

Сложение отображений f и g даёт ожидаемую композицию на H2: mapShortComplexH2 (g ∘ f) (φ ≫ (Res f).map ψ) = mapShortComplexH2 f φ ∘ mapShortComplexH2 g ψ.

LaTeX

$$$ mapShortComplexH2(g \cdot f)(\varphi \;\mathrm{≫}\; (\mathrm{Res}\, f).map(\psi)) = (mapShortComplexH2 f \varphi) \;\mathrm{≫}\; (mapShortComplexH2 g \psi) $$$

Lean4

@[reassoc (attr := simp), elementwise (attr := simp)]
theorem cyclesMap_comp_isoCycles₂_hom : cyclesMap f φ 2 ≫ (isoCycles₂ B).hom = (isoCycles₂ A).hom ≫ mapCycles₂ f φ := by
  simp [← cancel_mono (moduleCatLeftHomologyData (shortComplexH2 B)).i, mapShortComplexH2,
    chainsMap_f_2_comp_chainsIso₂ f]

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