cyclesIsoLeftHomology_hom_inv_id — Mathlib

English

Let S be a Short Complex with left homology data. If S.f = 0, then the left homology projection composed with the inverse of the cycles-LeftHomology is the identity on the appropriate object.

Русский

Пусть S — короткая комплексная система с левым гомологическим данными. При выполнении S.f = 0 композиция левого гомологического проекции с обратной стороной циклов-левого гомологического изоморфизма дает тождественный отображение.

LaTeX

$$$\pi_{\mathrm{L}} \circ (\mathrm{cyclesIsoLeftHomology}(hf))^{-1} = \mathrm{id}$$$

Lean4

@[reassoc (attr := simp)]
theorem cyclesIsoLeftHomology_hom_inv_id (hf : S.f = 0) : S.leftHomologyπ ≫ (S.cyclesIsoLeftHomology hf).inv = 𝟙 _ :=
  (S.cyclesIsoLeftHomology hf).hom_inv_id

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