mapCyclesIso_inv_naturality — Mathlib

English

Naturality of cycles map with respect to a morphism φ and a functor F: the diagram with cycles maps and the map induced by φ commutes.

Русский

Натуральность отображения циклов по отношению к φ и F: диаграмма с отображениями циклов и отображением φ натурализуется.

LaTeX

$$$\operatorname{cyclesMap}(\,F.mapShortComplex.map(\varphi)\,) \;\;\mathrm{hom} = \mathrm{hom} \;\circ\; F.map(\operatorname{cyclesMap}(\varphi))$$$

Lean4

@[reassoc]
theorem mapCyclesIso_inv_naturality [S₁.HasLeftHomology] [S₂.HasLeftHomology] [F.PreservesLeftHomologyOf S₁]
    [F.PreservesLeftHomologyOf S₂] :
    F.map (cyclesMap φ) ≫ (S₂.mapCyclesIso F).inv = (S₁.mapCyclesIso F).inv ≫ cyclesMap (F.mapShortComplex.map φ) := by
  rw [← cancel_epi (S₁.mapCyclesIso F).hom, ← mapCyclesIso_hom_naturality_assoc, Iso.hom_inv_id, comp_id,
    Iso.hom_inv_id_assoc]

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