isoCycles₁ — Mathlib

English

The 1-cycles of the inhomogeneous chain are isomorphic to cycles₁ A as a k-module.

Русский

1‑циклы неоднородного цепного комплекса изоморфны cycles₁ A как k-модуль.

LaTeX

$$$\text{isoCycles}_1 : \ text{cycles } A\ 1 \cong \mathrm{ModuleCat.of}\ k\ (\text{cycles}_1 A)$$$

Lean4

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

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