oneCochain

Mathlib.Algebra.Lie.Cochain

URI: https://scilib.ai/kg/mathlib#LieModule.Cohomology.oneCochain

English

There is a FunLike instance for the subobject twoCochain R L M, with evaluation given by a x ↦ a.1 x.

Русский

Существуют инстанты FunLike для подобъекта twoCochain, где действие определяется как a x = a.1 x.

LaTeX

$$TwoCochain R L M is a FunLike object with coe(a, x) = a.1 x.$$

Lean4

/-- Lie algebra 1-cochains over `L` with coefficients in the module `M`. -/
abbrev oneCochain :=
  L →ₗ[R] M

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

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

Разделы

Аффилиация

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