opcyclesIsoRightHomology_hom_inv_id

English

If g = 0, then the inverse of the right-homology iso composes to the identity on the left with the forward map.

Русский

Если g = 0, то обратная компонента изоморфизма правой гомологии компонуется с прямой картой в единицу слева.

LaTeX

$$$S.g = 0 \Rightarrow (S.opcyclesIsoRightHomology hg).hom \circ S.rightHomologyι = \mathrm{id}_{S.rightHomology}$$$

Lean4

@[reassoc (attr := simp)]
theorem opcyclesIsoRightHomology_hom_inv_id (hg : S.g = 0) :
    (S.opcyclesIsoRightHomology hg).hom ≫ S.rightHomologyι = 𝟙 _ :=
  (S.opcyclesIsoRightHomology hg).hom_inv_id

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