rightHomologyIso_hom_comp_homologyι

English

For any k: A → S.opcycles with hk: k ≫ S.fromOpcycles = 0, the lift homology map followed by homologyι equals k.

Русский

Для любого k: A → S.opcycles с условием hk: k ≫ S.fromOpcycles = 0, подъём гомологии после отображения гомологииι даёт k.

LaTeX

$$$S.liftHomology(k,hk) \;\;\; S.homologyι = k$$$

Lean4

@[reassoc (attr := simp)]
theorem rightHomologyIso_hom_comp_homologyι : S.rightHomologyIso.hom ≫ S.homologyι = S.rightHomologyι :=
  by
  dsimp only [homologyι]
  simp only [Iso.hom_inv_id_assoc]

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