English
If the L-module is trivial, then a ∈ twoCocycle iff ∀ x,y,z, a(x,[y,z]) = a([x,y], z) + a(y,[x,z]).
Русский
При тривиальном действии модуля L над M для any a ∈ twoCochain выполняется: a(x,[y,z]) = a([x,y], z) + a(y,[x,z]).
LaTeX
$$$a\\in twoCocycle \\;\\Rightarrow\\; \\forall x,y,z:\\ a(x,[y,z])=a([x,y],z)+a(y,[x,z]).$$$
Lean4
theorem mem_twoCocycle_iff_of_trivial [LieModule.IsTrivial L M] (a : twoCochain R L M) :
a ∈ twoCocycle R L M ↔ ∀ (x y z : L), a x ⁅y, z⁆ = a ⁅x, y⁆ z + a y ⁅x, z⁆ :=
by
constructor
· intro h x y z
rw [mem_twoCocycle_iff] at h
have : (d₂₃ R L M) a x y z = 0 := (congrArg (fun b ↦ b x y z = 0) h).mpr rfl
simp only [d₂₃_apply, trivial_lie_zero, sub_self, add_zero, zero_sub] at this
rw [sub_eq_zero] at this
rw [← twoCochain_skew a _ x, ← twoCochain_skew a _ y, ← this]
abel
· intro h
ext x y z
simp only [d₂₃_apply, trivial_lie_zero, sub_self, add_zero, zero_sub, LinearMap.zero_apply]
rw [← twoCochain_skew a x, ← twoCochain_skew a y, h x y z]
abel
