cyclesOpIso_hom_naturality — Mathlib

English

For φ: S1 ⟶ S2 with right homology, the equality cyclesMap (opMap φ) ≫ (S1.cyclesOpIso).hom = S2.cyclesOpIso.hom ≫ (opcyclesMap φ).op holds.

Русский

Для φ: S1 ⟶ S2 с правой гомологией выполняется равенство cyclesMap (opMap φ) ≫ (S1.cyclesOpIso).hom = S2.cyclesOpIso.hom ≫ (opcyclesMap φ).op.

LaTeX

$$cyclesMap (opMap(φ)) ≫ (S1.cyclesOpIso).hom = (S2.cyclesOpIso.hom) ≫ (opcyclesMap φ).op$$

Lean4

@[reassoc]
theorem cyclesOpIso_hom_naturality (φ : S₁ ⟶ S₂) [S₁.HasRightHomology] [S₂.HasRightHomology] :
    cyclesMap (opMap φ) ≫ (S₁.cyclesOpIso).hom = S₂.cyclesOpIso.hom ≫ (opcyclesMap φ).op := by
  rw [← cancel_mono (S₁.cyclesOpIso).inv, assoc, assoc, Iso.hom_inv_id, comp_id, cyclesOpIso_inv_naturality,
    Iso.hom_inv_id_assoc]

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