isoShortComplexH2 — Mathlib

English

There is an isomorphism between the 2nd shifted inhomogeneous chain and the short complex H2.

Русский

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

LaTeX

$$$ (\mathrm{inhomogeneousChains} A).sc 2 \cong \mathrm{shortComplexH2} A$$$

Lean4

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

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