toCycles_comp_isoCycles₁_hom — Mathlib

English

Definition: there is an isomorphism between the 1st shifted inhomogeneous chain and the short complex H1.

Русский

Определение: существует изоморфизм между первой сдвинутой неоднородной цепью и коротким комплексом H1.

LaTeX

$$$\mathrm{isoShortComplexH1} : (\mathrm{inhomogeneousChains} A).sc 1 \cong \mathrm{shortComplexH1} A$$$

Lean4

@[reassoc (attr := simp), elementwise (attr := simp)]
theorem toCycles_comp_isoCycles₁_hom :
    toCycles A 2 1 ≫ (isoCycles₁ A).hom = (chainsIso₂ A).hom ≫ (shortComplexH1 A).moduleCatLeftHomologyData.f' := by
  simp [← cancel_mono (shortComplexH1 A).moduleCatLeftHomologyData.i, comp_d₂₁_eq, shortComplexH1_f]

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