trace_toEnd_eq_zero — Mathlib

English

This confirms the vanishing trace in the matrix representation of Lie algebra actions via toEnd.

Русский

Это подтверждает исчезновение следа в матричном представлении действий Ли-алгебры через toEnd.

LaTeX

$$$\\mathrm{trace}(\\mathrm{toEnd}(x)) = 0$$$

Lean4

/-- This is the main result of lemma 4.1 from [Geck](Geck2017). -/
theorem trace_toEnd_eq_zero (x : lieAlgebra b) : trace R _ (toEnd R _ (b.support ⊕ ι → R) x) = 0 :=
  by
  obtain ⟨x, hx⟩ := x
  suffices trace R _ x.toLin' = 0 by simpa
  refine LieAlgebra.trace_toEnd_eq_zero ?_ hx
  rintro - ((⟨i, rfl⟩ | ⟨i, rfl⟩) | ⟨i, rfl⟩)
  · simp
  · simpa using Matrix.isNilpotent_trace_of_isNilpotent (isNilpotent_e i)
  · simpa using Matrix.isNilpotent_trace_of_isNilpotent (isNilpotent_f i)

Похожие утверждения