mapOpcyclesIso_inv_naturality — Mathlib

English

Naturality for the inverse direction of cycles maps: the inverse of cyclesMap commutes with the hom component of mapCyclesIso.

Русский

Натурализм для обратной стороны отображения циклов: обратное отображение cyclesMap коммутирует с компонентом гомоморфизма mapCyclesIso.

LaTeX

$$$F.map( cyclesMap(\varphi) ) \; \circ\; (S_2.mapCyclesIso F).inv = (S_1.mapCyclesIso F).inv \circ\; cyclesMap'(F.mapShortComplex.map(\varphi))$$$

Lean4

@[reassoc]
theorem mapOpcyclesIso_inv_naturality [S₁.HasRightHomology] [S₂.HasRightHomology] [F.PreservesRightHomologyOf S₁]
    [F.PreservesRightHomologyOf S₂] :
    F.map (opcyclesMap φ) ≫ (S₂.mapOpcyclesIso F).inv =
      (S₁.mapOpcyclesIso F).inv ≫ opcyclesMap (F.mapShortComplex.map φ) :=
  by
  rw [← cancel_epi (S₁.mapOpcyclesIso F).hom, ← mapOpcyclesIso_hom_naturality_assoc, Iso.hom_inv_id, comp_id,
    Iso.hom_inv_id_assoc]

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