H2π_eq_iff

Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

URI: https://scilib.ai/kg/mathlib#groupCohomology.H2π_eq_iff

English

Equivalent criterion for zero of H2π on a cocycle: H2π A x = 0 iff x is coboundary.

Русский

Эквивалентное утверждение: H2π A x = 0 тогда же, когда x является coboundary.

LaTeX

$$$H2\pi_A(x) = 0 \iff x \in coboundaries_2(A)$$$

Lean4

theorem H2π_eq_iff (x y : cocycles₂ A) : H2π A x = H2π A y ↔ ⇑x - ⇑y ∈ coboundaries₂ A :=
  by
  rw [← sub_eq_zero, ← map_sub, H2π_eq_zero_iff]
  rfl

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

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

Разделы

Аффилиация

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