isoShortComplexH1 — Mathlib

English

There is an isomorphism between the 1st shifted inhomogeneous chain and the short complex H1.

Русский

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

LaTeX

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

Lean4

/-- The short complex `(G² →₀ A) --d₂₁--> (G →₀ A) --d₁₀--> A` is isomorphic to the 1st
short complex associated to the complex of inhomogeneous chains of `A`. -/
@[simps! hom inv]
def isoShortComplexH1 : (inhomogeneousChains A).sc 1 ≅ shortComplexH1 A :=
  (inhomogeneousChains A).isoSc' 2 1 0 (by simp) (by simp) ≪≫
    isoMk (chainsIso₂ A) (chainsIso₁ A) (chainsIso₀ A) (comp_d₂₁_eq A) (comp_d₁₀_eq A)

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