English
If N is acted on trivially by I (i.e., [LieModule.IsTrivial I N]), then for all x,y in L the trace of φ_x ∘ φ_y on M is zero.
Русский
Если N над I действует тривиально (IsTrivial I N), тогда для всех x,y ∈ L след от φ_x ∘ φ_y на M равен нулю.
LaTeX
$$$\forall x,y\in L:\; tr(φ_x \circ φ_y) = 0$ under the hypothesis of trivial action on N$$
Lean4
/-- Note that this result is slightly stronger than it might look at first glance: we only assume
that `N` is trivial over `I` rather than all of `L`. This means that it applies in the important
case of an Abelian ideal (which has `M = L` and `N = I`). -/
theorem traceForm_eq_zero_of_isTrivial [LieModule.IsTrivial I N] : trace R M (φ x ∘ₗ φ y) = 0 :=
by
let hy' : ∀ m ∈ N, (φ x ∘ₗ φ y) m ∈ N := fun m _ ↦ N.lie_mem (N.mem_idealizer.mp (h hy) m)
suffices (φ x ∘ₗ φ y).restrict hy' = 0 by simp [this, N.trace_eq_trace_restrict_of_le_idealizer I h x hy]
ext (n : N)
suffices ⁅y, (n : M)⁆ = 0 by simp [this]
exact Submodule.coe_eq_zero.mpr (LieModule.IsTrivial.trivial (⟨y, hy⟩ : I) n)
