cocyclesIso₀ — Mathlib

English

The 0-cocycles are isomorphic to iCocycles via cochainsIso0.

Русский

0-коциклы изоморфны iCocycles через cochainsIso0.

LaTeX

$$cocyclesIso_0 : cocycles_0(A) ≅ ModuleCat.of k (Subtype ... )$$

Lean4

/-- The 0-cocycles of the complex of inhomogeneous cochains of `A` are isomorphic to
`A.ρ.invariants`, which is a simpler type. -/
def cocyclesIso₀ : cocycles A 0 ≅ ModuleCat.of k A.ρ.invariants :=
  KernelFork.mapIsoOfIsLimit ((inhomogeneousCochains A).cyclesIsKernel 0 1 (by simp)) (shortComplexH0_exact A).fIsKernel
    (dArrowIso₀₁ A)

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