iCyclesIso_hom_inv_id — Mathlib

English

Under suitable conditions, the map homologyπ j is an isomorphism.

Русский

При определённых условиях отображение homologyπ j является изоморфизмом.

LaTeX

$$$$ \mathrm{homology\}\pi_j: K.X_j \to \mathrm{Homology}_j(K) \quad \text{is an isomorphism} $$$$

Lean4

@[reassoc (attr := simp)]
theorem iCyclesIso_hom_inv_id : K.iCycles i ≫ (K.iCyclesIso i j hj h).inv = 𝟙 _ :=
  (K.iCyclesIso i j hj h).hom_inv_id

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