cyclesIsoLeftHomology_inv_hom_id — Mathlib

English

Let hf be as above. The inverse of cyclesIsoLeftHomology hf composed with leftHomologyπ yields the identity on the left homology target.

Русский

Пусть hf удовлетворяет условиям. Обратный цикл cyclesIsoLeftHomology hf, затем композиция с leftHomologyπ дает тождественный отображение.

LaTeX

$$$(\mathrm{cyclesIsoLeftHomology}(hf))^{-1} \circ \mathrm{leftHomology}\pi = \mathrm{id}$$$

Lean4

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

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