isoHomologyι_inv_hom_id — Mathlib

English

The inverse of pOpcyclesIso composed with pOpcycles yields the identity map on the target.

Русский

Обратное pOpcyclesIso в композиции с pOpcycles даёт тождество на целевом объекте.

LaTeX

$$$$ (K.pOpcyclesIso i j hi h)^{-1} \\circ K.pOpcycles j = \\mathrm{Id} $$$$

Lean4

@[reassoc (attr := simp)]
theorem isoHomologyι_inv_hom_id : (K.isoHomologyι i j hj h).inv ≫ K.homologyι i = 𝟙 _ :=
  (K.isoHomologyι i j hj h).inv_hom_id

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