instFunLikeSubtypeForallCarrierVModuleCatMemSubmoduleCocycles₁

Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

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

English

The 1-cocycles Z^1(G,A) carry a natural FunLike structure as a G-indexed family of A-valued functions.

Русский

1-циклы Z^1(G,A) естественно образуют структуру FunLike — семейство функций из G в A с индексом G.

LaTeX

$$instance : FunLike (cocycles_1 A) G A := ⟨Subtype.val, Subtype.val_injective⟩$$

Lean4

instance : FunLike (cocycles₁ A) G A :=
  ⟨Subtype.val, Subtype.val_injective⟩

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

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

Разделы

Аффилиация

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