comm — Mathlib

English

For any HomologyMapData φ h1 h2, the left φH commutes with the right map after suitable isomorphisms.

Русский

Для данных гомологического отображения φ h1 h2 левая часть φH коммутирует с правой после подходящих изоморфизмов.

LaTeX

$$$ h.left.\varphiH \;\; ≫ \; h_2.iso.hom = h_1.iso.hom ≫ h.right.\varphiH $$$

Lean4

@[reassoc]
theorem comm (h : HomologyMapData φ h₁ h₂) : h.left.φH ≫ h₂.iso.hom = h₁.iso.hom ≫ h.right.φH := by
  simp only [← cancel_epi h₁.left.π, ← cancel_mono h₂.right.ι, assoc, LeftHomologyMapData.commπ_assoc,
    HomologyData.comm, LeftHomologyMapData.commi_assoc, RightHomologyMapData.commι, HomologyData.comm_assoc,
    RightHomologyMapData.commp]

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