isoCycles₂ — Mathlib

English

The 2-cycles of the inhomogeneous chain are isomorphic to cycles₂ A as a module.

Русский

2‑циклы неоднородного цепного комплекса изоморфны cycles₂ A как модулю.

LaTeX

$$$\text{isoCycles}_2 : \ cycles A\ 2 \cong \mathrm{ModuleCat.of}\ k (\ cycles_2 A)$$$

Lean4

/-- The 2-cycles of the complex of inhomogeneous chains of `A` are isomorphic to
`cycles₂ A`, which is a simpler type. -/
def isoCycles₂ : cycles A 2 ≅ ModuleCat.of k (cycles₂ A) :=
  cyclesMapIso' (isoShortComplexH2 A) ((inhomogeneousChains A).sc 2).leftHomologyData
    (shortComplexH2 A).moduleCatLeftHomologyData

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