cocycles₂_map_one_snd

Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

URI: https://scilib.ai/kg/mathlib#groupCohomology.cocycles₂_map_one_snd

← MathLib Explorer

English

For g ∈ G, f(g,1) = ρ_g(f(1,1)).

Русский

Для любого g ∈ G выполняется f(g,1) = ρ_g(f(1,1)).

LaTeX

$$$$ \\forall f \\in cocycles_2(A), \\forall g \\in G,\ \ f(g,1) = A.\\\\rho(g)(f(1,1)). $$$$

Lean4

theorem cocycles₂_map_one_snd (f : cocycles₂ A) (g : G) : f (g, 1) = A.ρ g (f (1, 1)) :=
  by
  have := (mem_cocycles₂_iff f).1 f.2 g 1 1
  simpa only [mul_one, add_left_inj, this]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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