opcyclesIso₀ — Mathlib

English

The inverse of the cycles isomorphism composed with iCycles0 equals the inverse of the homogeneous chains isomorphism composed with pOpcycles at degree 0.

Русский

Обратное изоморфизма циклов, композиция с iCycles0, равна композиции обратного отображения цепочек с pOpcycles на степени 0.

LaTeX

$$$ (\text{cycles}^{-1}_0 A) \circ iCycles(A,0) = (\text{shortComplexH0 A}).moduleCatLeftHomologyData.i \circ (\text{chainsIso}_0 A)^{-1} $$$

Lean4

/-- The 0-cycles of the complex of inhomogeneous chains of `A` are isomorphic to
`A.ρ.coinvariants`, which is a simpler type. -/
def opcyclesIso₀ : (inhomogeneousChains A).opcycles 0 ≅ (coinvariantsFunctor k G).obj A :=
  CokernelCofork.mapIsoOfIsColimit ((inhomogeneousChains A).opcyclesIsCokernel 1 0 (by simp))
    (shortComplexH0_exact A).gIsCokernel (d₁₀ArrowIso A)

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