lie_e_f_same — Mathlib

English

The trace of the endomorphism induced by any Lie algebra element x on the weight space vanishes.

Русский

След линейного отображения, порождённого элементом Ли, на весовом пространстве равен нулю.

LaTeX

$$$\\operatorname{trace}(\\mathrm{toEnd}(x)) = 0$ for all $x$ in the Lie algebra$$

Lean4

/-- Lemma 3.4 from [Geck](Geck2017). -/
theorem lie_e_f_same : ⁅e i, f i⁆ = h i := by
  letI := P.indexNeg
  have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
  have : NoZeroSMulDivisors ℤ M := .int_of_charZero R M
  classical
  ext (k | k) (l | l)
  · simp [e, f, h]
  · have h₁ (x : ι) : ¬(P.root x = P.root l - P.root i ∧ k = i ∧ x = -i) :=
      by
      simp only [not_and]
      rintro contra rfl rfl
      simp [P.ne_zero, sub_eq_add_neg] at contra
    have h₂ (x : ι) : ¬(P.root x = P.root i + P.root l ∧ k = i ∧ x = i) :=
      by
      simp only [not_and]
      rintro contra rfl rfl
      simp [P.ne_zero] at contra
    simp [e, f, h, h₁, h₂, -indexNeg_neg, ← ite_and]
  · simp [e, f, h]
  · rcases eq_or_ne k i with rfl | hki
    · have hx (x : ι) : ¬(P.root x = P.root i + P.root l ∧ P.root i = P.root x - P.root i) :=
        by
        rintro ⟨-, contra⟩
        refine P.nsmul_notMem_range_root (n := 2) (i := i) ⟨x, ?_⟩
        rwa [eq_sub_iff_add_eq, ← two_smul ℕ, eq_comm] at contra
      simp only [e, f, h, P.ne_zero, P.ne_neg, Ring.lie_def, Fintype.sum_sum_type, Matrix.sub_apply, Matrix.mul_apply,
        Matrix.fromBlocks_apply₂₁, Matrix.of_apply, Matrix.fromBlocks_apply₂₂, left_eq_add, zero_mul, mul_zero, ite_mul,
        mul_ite, ← ite_and]
      rw [Finset.sum_eq_single_of_mem i (Finset.mem_univ _) (by aesop)]
      simp [hx, eq_comm]
    rcases eq_or_ne k (-i) with rfl | hki'
    · have hx (x : ι) : ¬(P.root x = P.root l - P.root i ∧ P.root (-i) = P.root i + P.root x) :=
        by
        rintro ⟨-, contra⟩
        refine P.nsmul_notMem_range_root (n := 2) (i := -i) ⟨x, ?_⟩
        replace contra : P.root x = -(P.root i + P.root i) := by
          simpa [neg_eq_iff_add_eq_zero, ← add_assoc, add_eq_zero_iff_eq_neg'] using contra
        simp [contra, two_smul]
      have aux (x : ι) : ¬P.root (-i) = P.root x - P.root i := by simp [P.ne_zero x, eq_comm]
      simp only [e, f, h, Ring.lie_def, Matrix.sub_apply, Matrix.mul_apply, Fintype.sum_sum_type,
        Matrix.fromBlocks_apply₂₁, Matrix.of_apply, hki, reduceIte, zero_mul, Finset.sum_const_zero,
        Matrix.fromBlocks_apply₂₂, mul_ite, ite_mul, mul_zero, ← ite_and, if_neg (hx _), add_zero, aux, zero_sub,
        Matrix.diagonal_apply]
      rw [Finset.sum_eq_single_of_mem i (Finset.mem_univ _) (by aesop)]
      simp [eq_comm, apply_ite ((-·) : R → R)]
    rcases eq_or_ne k l with rfl | hkl
    · exact lie_e_f_same_aux i k hki hki'
    · simp_all [h, e, f]

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