pOpcycles_comp_opcyclesIso_hom — Mathlib

English

The application of coinvariantsMk followed by the inverse opcycles iso equals the inverse chains iso composed with pOpcycles at degree 0.

Русский

Применение coinvariantsMk далее через обратное отображение opcycles_iso₀ совпадает с обратным отображением chainsIso0, затем с pOpcycles на степени 0.

LaTeX

$$$ (\mathrm{coinvariantsMk}\ k\ G).app A \circ (\mathrm{opcyclesIso}_0 A)^{-1} = (\mathrm{chainsIso}_0 A)^{-1} \circ (\mathrm{inhomogeneousChains} A).pOpcycles 0$$

Lean4

@[reassoc (attr := simp), elementwise (attr := simp)]
theorem pOpcycles_comp_opcyclesIso_hom :
    (inhomogeneousChains A).pOpcycles 0 ≫ (opcyclesIso₀ A).hom = (chainsIso₀ A).hom ≫ (coinvariantsMk k G).app A :=
  CokernelCofork.π_mapOfIsColimit (φ := (d₁₀ArrowIso A).hom) _ _

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