English
The same trace vanishing statement holds for the endomorphism associated with Lie algebra elements via the Geck construction.
Русский
Тождественный нулевой след сохраняется для соответствующего преобразования Ли-алгебры через Geck конструкцию.
LaTeX
$$tr( toEnd_R (b.support ⊕ ι → R) x ) = 0$$
Lean4
theorem isNilpotent_e : IsNilpotent (e i) := by
classical
have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
have : NoZeroSMulDivisors ℤ M := .int_of_charZero R M
letI := P.indexNeg
rw [Matrix.isNilpotent_iff_forall_col]
have case_inl (j : b.support) : (e i ^ 2).col (Sum.inl j) = 0 :=
by
ext (k | k)
· simp [e, sq, ne_neg P i, -indexNeg_neg]
· have aux : ∀ x : ι, x ∈ Finset.univ → ¬(x = i ∧ P.root k = P.root i + P.root x) :=
by
suffices P.root k ≠ (2 : ℕ) • P.root i by simpa [two_smul]
exact fun contra ↦ P.nsmul_notMem_range_root (n := 2) (i := i) ⟨k, contra⟩
simp [e, sq, -indexNeg_neg, ← ite_and, Finset.sum_ite_of_false aux]
rintro (j | j)
· exact ⟨2, case_inl j⟩
· by_cases hij : j = -i
· use 2 + 1
replace hij : (e i).col (Sum.inr j) = u i := by
ext (k | k)
· simp [e, -indexNeg_neg, Pi.single_apply, hij]
· have hk : P.root k ≠ P.root i + P.root j := by simp [hij, P.ne_zero k]
simp [e, -indexNeg_neg, hk]
rw [pow_succ, ← Matrix.mulVec_single_one, ← Matrix.mulVec_mulVec]
simp [hij, case_inl i]
use P.chainTopCoeff i j + 1
rcases isNilpotent_e_aux i (P.chainTopCoeff i j + 1) hij with this | ⟨k, x, hk₁, -⟩
· assumption
exfalso
replace hk₁ : P.root j + (P.chainTopCoeff i j + 1) • P.root i ∈ range P.root := ⟨k, hk₁⟩
have hij' : LinearIndependent R ![P.root i, P.root j] :=
by
apply IsReduced.linearIndependent P ?_ ?_
· rintro rfl
apply P.nsmul_notMem_range_root (n := P.chainTopCoeff i i + 2) (i := i)
convert hk₁ using 1
module
· contrapose! hij
rw [root_eq_neg_iff] at hij
rw [hij, ← indexNeg_neg, neg_neg]
rw [root_add_nsmul_mem_range_iff_le_chainTopCoeff hij'] at hk₁
cutsat
