d₁₂_apply_apply

Mathlib.Algebra.Lie.Cochain

URI: https://scilib.ai/kg/mathlib#LieModule.Cohomology.d₁₂_apply_apply

English

For any 1-cochain f and x,y in L, d12 f x y equals the explicit Lie-bracket expression: [x, f y] − [y, f x] − f [x,y].

Русский

Для любой 1-коцепи f и x,y в L имеем: d12 f x y = [x, f y] − [y, f x] − f [x,y].

LaTeX

$$$d_{12} f(x,y) = [x,f(y)] - [y,f(x)] - f([x,y]).$$$

Lean4

@[simp]
theorem d₁₂_apply_apply (f : oneCochain R L M) (x y : L) : d₁₂ R L M f x y = ⁅x, f y⁆ - ⁅y, f x⁆ - f ⁅x, y⁆ :=
  rfl

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

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

Разделы

Аффилиация

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