English
The coboundary operator d1→2 sends a 1-cochain f to a 2-cochain with formula (d12 f)(x,y) = [x, f(y)] − [y, f(x)] − f([x,y]).
Русский
Кобоундари оператор d1→2 отправляет 1-коCHAIN в 2-коCHAIN по формуле (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
/-- The coboundary operator taking degree 1 cochains to degree 2 cochains. -/
@[simps]
def d₁₂ : oneCochain R L M →ₗ[R] twoCochain R L M
where
toFun
f :=
{ val :=
{ toFun
x :=
{ toFun y := ⁅x, f y⁆ - ⁅y, f x⁆ - f ⁅x, y⁆
map_add' _ _ := by simp; abel
map_smul' _ _ := by simp [smul_sub] }
map_add' _ _ := by ext; simp; abel
map_smul' _ _ := by ext; simp [smul_sub] }
property x := by simp }
map_add' _ _ := by ext; simp; abel
map_smul' _ _ := by ext; simp [smul_sub]
