opcyclesIsoRightHomology_inv_hom_id

English

If the same hypothesis as above holds (g = 0), then the inverse component of the right homology isomorphism composes to the identity with the forward component.

Русский

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

LaTeX

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

Lean4

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

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