cyclesIso₀_comp_H0π

Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

URI: https://scilib.ai/kg/mathlib#groupHomology.cyclesIso₀_comp_H0π

English

The composition of cyclesIso₀ A with H0π A equals π A 0.

Русский

Сложение cyclesIso₀ A с H0π A равно π A 0.

LaTeX

$$$(cyclesIso_0 A)_{\\mathrm{hom}} \\circ H_0\\pi A = \\pi A 0$$

Lean4

@[reassoc (attr := simp), elementwise (attr := simp)]
theorem cyclesIso₀_comp_H0π : (cyclesIso₀ A).hom ≫ H0π A = π A 0 := by simp [H0π]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru