map₁_one

Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

URI: https://scilib.ai/kg/mathlib#groupCohomology.map₁_one

English

The first level map sends identity data to zero.

Русский

Отображение на первом уровне отправляет данные единицы в нуль.

LaTeX

$$$\mathrm{map}_1(1)\varphi_1 = 0$$$

Lean4

@[simp]
theorem map₁_one (φ : (Action.res _ 1).obj A ⟶ B) : map 1 φ 1 = 0 := by simp [← cancel_epi (H1π _)]

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

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

Разделы

Аффилиация

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