mapLeftHomologyIso_inv_naturality

English

Naturality of leftHomologyMapIso with respect to φ and F: the hom components commute with the left map under F.

Русский

Натурализм leftHomologyMapIso по φ и F: компоненты гомоморфизмов разворачиваются через левую мапу.

LaTeX

$$$leftHomologyMap( F.mapShortComplex.map(\varphi) )\; \circ\; (S_2.mapLeftHomologyIso F).hom = (S_1.mapLeftHomologyIso F).hom \circ\; F.map( leftHomologyMap(\varphi) )$$$

Lean4

@[reassoc]
theorem mapLeftHomologyIso_inv_naturality [S₁.HasLeftHomology] [S₂.HasLeftHomology] [F.PreservesLeftHomologyOf S₁]
    [F.PreservesLeftHomologyOf S₂] :
    F.map (leftHomologyMap φ) ≫ (S₂.mapLeftHomologyIso F).inv =
      (S₁.mapLeftHomologyIso F).inv ≫ leftHomologyMap (F.mapShortComplex.map φ) :=
  by
  rw [← cancel_epi (S₁.mapLeftHomologyIso F).hom, ← mapLeftHomologyIso_hom_naturality_assoc, Iso.hom_inv_id, comp_id,
    Iso.hom_inv_id_assoc]

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