H0IsoOfIsTrivial_hom

Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

URI: https://scilib.ai/kg/mathlib#groupCohomology.H0IsoOfIsTrivial_hom

English

If A is a trivial G-representation, then H0(A) is naturally isomorphic to the underlying module A.V.

Русский

Если A — тривиальное представление G, то H0(A) естественно изоморфно базовому модулю A.V.

LaTeX

$$def H0IsoOfIsTrivial : H0 A ≅ A.V$$

Lean4

@[simp, elementwise]
theorem H0IsoOfIsTrivial_hom : (H0IsoOfIsTrivial A).hom = (H0Iso A).hom ≫ (shortComplexH0 A).f :=
  rfl

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

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

Разделы

Аффилиация

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