coinvariantsMk_comp_opcyclesIso₀_inv

English

The morphism pOpcycles composed with opcyclesIso₀ is the same as the chainsIso₀ composed with coinvariants app.

Русский

Составление pOpcycles с opcyclesIso₀ равно композиции chainsIso₀ с coinvariants app.

LaTeX

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

Lean4

@[reassoc (attr := simp), elementwise (attr := simp)]
theorem coinvariantsMk_comp_opcyclesIso₀_inv :
    (coinvariantsMk k G).app A ≫ (opcyclesIso₀ A).inv = (chainsIso₀ A).inv ≫ (inhomogeneousChains A).pOpcycles 0 :=
  (CommSq.vert_inv ⟨pOpcycles_comp_opcyclesIso_hom A⟩).w

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