π_comp_H0Iso_hom — Mathlib

English

For a representation A, the natural compatibility relation holds between π, H0Iso and cyclesIso₀: the composition π_A0 followed by the hom of H0Iso A equals the hom of cyclesIso₀ A followed by the app of coinvariantsMk.

Русский

Для представления A выполняется естественное соотношение совместимости между π, H0Iso и cyclesIso₀: композиция π_A0 с гомоморфизмом H0Iso A равна композиции гомоморфизма cyclesIso₀ A с приложением coinvariantsMk.

LaTeX

$$$\\pi_A0 \\;\\circ\\; (H_0\\mathrm{Iso}\\, A)_{\\mathrm{hom}} = (\\mathrm{cyclesIso}_0\\, A)_{\\mathrm{hom}} \\;\\circ\\; (\\mathrm{coinvariantsMk}\\ k\\ G)_{\\mathrm{app}} A$$$

Lean4

@[reassoc (attr := simp), elementwise (attr := simp)]
theorem π_comp_H0Iso_hom : π A 0 ≫ (H0Iso A).hom = (cyclesIso₀ A).hom ≫ (coinvariantsMk k G).app A := by
  simp [H0Iso, cyclesIso₀]

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