English
The upper and lower central series of L are orthogonal with respect to the trace form on any Lie module M.
Русский
Верхний и нижний центральный ряды Lie-алгебры L ортогональны относительно trace-form на любом Ли-модуле M.
LaTeX
$$$$ \text{traceForm}_{M}(\text{top- lcs}, \text{bot- ucs}) = 0.$$$$
Lean4
/-- The upper and lower central series of `L` are orthogonal w.r.t. the trace form of any Lie module
`M`. -/
theorem traceForm_eq_zero_if_mem_lcs_of_mem_ucs {x y : L} (k : ℕ) (hx : x ∈ (⊤ : LieIdeal R L).lcs L k)
(hy : y ∈ (⊥ : LieIdeal R L).ucs k) : traceForm R L M x y = 0 := by
induction k generalizing x y with
| zero =>
replace hy : y = 0 := by simpa using hy
simp [hy]
| succ k ih =>
rw [LieSubmodule.ucs_succ, LieSubmodule.mem_normalizer] at hy
simp_rw [LieIdeal.lcs_succ, ← LieSubmodule.mem_toSubmodule, LieSubmodule.lieIdeal_oper_eq_linear_span',
LieSubmodule.mem_top, true_and] at hx
refine Submodule.span_induction ?_ ?_ (fun z w _ _ hz hw ↦ ?_) (fun t z _ hz ↦ ?_) hx
· rintro - ⟨z, w, hw, rfl⟩
rw [← lie_skew, map_neg, LinearMap.neg_apply, neg_eq_zero, traceForm_apply_lie_apply]
exact ih hw (hy _)
· simp
· simp [hz, hw]
· simp [hz]
