English
The operator d23: twoCochain → L → L → L → M sends a 2-cochain a to the 4-argument map given by a certain Lie-bracket expression involving x, y, z and a.
Русский
Оператор d23: двакоцепь $\to$ трёхцепь, отображает двук цепь a в четырехаргументную карту через скобки Ли.
LaTeX
$$$d_{23} a(x,y,z) = [x, a(y,z)] - [y, a(x,z)] + [z, a(x,y)] - a([x,y])z + a([x,z])y - a([y,z])x.$$$
Lean4
/-- The coboundary operator taking degree 2 cochains to a space containing degree 3 cochains. -/
def d₂₃ : twoCochain R L M →ₗ[R] L →ₗ[R] L →ₗ[R] L →ₗ[R] M
where
toFun := d₂₃_aux R L M
map_add' _ _ := by ext; simp [d₂₃_aux]; abel
map_smul' _ _ := by ext; simp [d₂₃_aux]; abel_nf; simp
