English
The image of the adjoint action ad: L → Der(L) forms an ideal in the Lie algebra of derivations; equivalently, it is an ideal morphism range.
Русский
Образ отображения сопряжённого действия ad: L → Der(L) является идеалом в алгебре Ли производных.
LaTeX
$$ad: L → Der(L) has range which is an ideal of Der(L).$$
Lean4
theorem d₂₃_comp_d₁₂ : (d₂₃ R L M) ∘ₗ (d₁₂ R L M) = 0 :=
by
ext a x y z
have (a : oneCochain R L M) (x : L) : d₁₂ R L M a x = (d₁₂ R L M a).val x := rfl
simp only [LinearMap.comp_apply, d₂₃_apply, LinearMap.zero_apply, this, d₁₂_apply_coe_apply_apply R L M, lie_sub,
lie_lie]
rw [leibniz_lie y x, leibniz_lie z x, leibniz_lie z y]
have : a ⁅y, ⁅z, x⁆⁆ = a ⁅x, ⁅z, y⁆⁆ + a ⁅z, ⁅y, x⁆⁆ := by
rw [congr_arg a (leibniz_lie y z x), ← lie_skew, ← lie_skew z y, lie_neg, map_add]
simp only [lie_lie, sub_add_cancel, map_sub, ← lie_skew x y, ← lie_skew x z, ← lie_skew y z, lie_neg, map_neg, this]
abel
