coinvariantsMk_comp_H0Iso_inv — Mathlib

English

For any A, the composite of coinvariantsMk with the inverse of H0Iso A recovers the map H0π A: H0 A → A_G.

Русский

Для любого A композиция coinvariantsMk с обратной H0Iso(A) восстанавливает отображение H0π A: H0(G,A) → A_G.

LaTeX

$$$(\\mathrm{coinvariantsMk}\\ k\\ G).app A \\;\\circ\\; (\\mathrm{H0Iso}\\, A)^{-1} = H_0\\pi A$$$

Lean4

@[reassoc (attr := simp), elementwise (attr := simp)]
theorem coinvariantsMk_comp_H0Iso_inv : (coinvariantsMk k G).app A ≫ (H0Iso A).inv = H0π A :=
  (CommSq.vert_inv ⟨π_comp_H0Iso_hom A⟩).w

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