|
| 1 | +/- |
| 2 | +Copyright (c) 2025 Oliver Nash. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Oliver Nash |
| 5 | +-/ |
| 6 | +import Mathlib.Algebra.Lie.Matrix |
| 7 | +import Mathlib.Algebra.Lie.Semisimple.Lemmas |
| 8 | +import Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic |
| 9 | +import Mathlib.RingTheory.Finiteness.Nilpotent |
| 10 | + |
| 11 | +/-! |
| 12 | +# Geck's construction of a Lie algebra associated to a root system yields semisimple algebras |
| 13 | +
|
| 14 | +This file contains a proof that `RootPairing.GeckConstruction.lieAlgebra` yields semisimple Lie |
| 15 | +algebras. |
| 16 | +
|
| 17 | +## Main definitions: |
| 18 | +
|
| 19 | +* `RootPairing.GeckConstruction.trace_toEnd_eq_zero`: the Geck construction yields trace-free |
| 20 | + matrices. |
| 21 | +
|
| 22 | +-/ |
| 23 | + |
| 24 | +noncomputable section |
| 25 | + |
| 26 | +namespace RootPairing.GeckConstruction |
| 27 | + |
| 28 | +open Function Module.End |
| 29 | +open Set hiding diagonal |
| 30 | +open scoped Matrix |
| 31 | + |
| 32 | +attribute [local simp] Ring.lie_def Matrix.mul_apply Matrix.one_apply Matrix.diagonal_apply |
| 33 | + |
| 34 | +variable {ι R M N : Type*} [CommRing R] [IsDomain R] [CharZero R] |
| 35 | + [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] |
| 36 | + {P : RootPairing ι R M N} [P.IsCrystallographic] [P.IsReduced] {b : P.Base} |
| 37 | + [Fintype ι] [DecidableEq ι] (i : b.support) |
| 38 | + |
| 39 | +/-- An auxiliary lemma en route to `RootPairing.GeckConstruction.isNilpotent_e`. -/ |
| 40 | +private lemma isNilpotent_e_aux {j : ι} (n : ℕ) (h : letI _i := P.indexNeg; j ≠ -i) : |
| 41 | + (e i ^ n).col (.inr j) = 0 ∨ |
| 42 | + ∃ (k : ι) (x : ℕ), P.root k = P.root j + n • P.root i ∧ |
| 43 | + (e i ^ n).col (.inr j) = x • Pi.single (.inr k) 1 := by |
| 44 | + have _i : NoZeroSMulDivisors ℤ M := by have := P.reflexive_left; exact .int_of_charZero R M |
| 45 | + letI _i := P.indexNeg |
| 46 | + have aux (n : ℕ) : (e i ^ (n + 1)).col (.inr j) = (e i).mulVec ((e i ^ n).col (.inr j)) := by |
| 47 | + rw [pow_succ', ← Matrix.mulVec_single_one, ← Matrix.mulVec_mulVec]; simp |
| 48 | + induction n with |
| 49 | + | zero => exact Or.inr ⟨j, 1, by simp, by ext; simp [Pi.single_apply]⟩ |
| 50 | + | succ n ih => |
| 51 | + rcases ih with hn | ⟨k, x, hk₁, hk₂⟩ |
| 52 | + · left; simp [aux, hn] |
| 53 | + rw [aux, hk₂, Matrix.mulVec_smul] |
| 54 | + have hki : k ≠ -i := by |
| 55 | + rintro rfl |
| 56 | + replace hk₁ : P.root (-j) = (n + 1) • P.root i := by |
| 57 | + simp only [indexNeg_neg, root_reflectionPerm, reflection_apply_self, neg_eq_iff_add_eq_zero, |
| 58 | + add_smul, one_smul] at hk₁ ⊢ |
| 59 | + rw [← hk₁] |
| 60 | + module |
| 61 | + rcases n.eq_zero_or_pos with rfl | hn |
| 62 | + · apply h |
| 63 | + rw [zero_add, one_smul, EmbeddingLike.apply_eq_iff_eq] at hk₁ |
| 64 | + simp [← hk₁, -indexNeg_neg] |
| 65 | + · have _i : (n + 1).AtLeastTwo := ⟨by omega⟩ |
| 66 | + exact P.nsmul_notMem_range_root (n := n + 1) (i := i) ⟨-j, hk₁⟩ |
| 67 | + by_cases hij : P.root j + (n + 1) • P.root i ∈ range P.root |
| 68 | + · obtain ⟨l, hl⟩ := hij |
| 69 | + right |
| 70 | + refine ⟨l, x * (P.chainBotCoeff i k + 1), hl, ?_⟩ |
| 71 | + ext (m | m) |
| 72 | + · simp [e, -indexNeg_neg, hki] |
| 73 | + · rcases eq_or_ne m l with rfl | hml |
| 74 | + · replace hl : P.root m = P.root i + P.root k := by rw [hl, hk₁]; module |
| 75 | + simp [e, -indexNeg_neg, hl, mul_add] |
| 76 | + · replace hl : P.root m ≠ P.root i + P.root k := |
| 77 | + fun contra ↦ hml (P.root.injective <| by rw [hl, contra, hk₁]; module) |
| 78 | + simp [e, -indexNeg_neg, hml, hl] |
| 79 | + · left |
| 80 | + ext (l | l) |
| 81 | + · simp [e, -indexNeg_neg, hki] |
| 82 | + · replace hij : P.root l ≠ P.root i + P.root k := |
| 83 | + fun contra ↦ hij ⟨l, by rw [contra, hk₁]; module⟩ |
| 84 | + simp [e, -indexNeg_neg, hij] |
| 85 | + |
| 86 | +lemma isNilpotent_e : |
| 87 | + IsNilpotent (e i) := by |
| 88 | + classical |
| 89 | + have _i : NoZeroSMulDivisors ℤ M := by have := P.reflexive_left; exact .int_of_charZero R M |
| 90 | + letI _i := P.indexNeg |
| 91 | + rw [Matrix.isNilpotent_iff_forall_col] |
| 92 | + have case_inl (j : b.support) : (e i ^ 2).col (Sum.inl j) = 0 := by |
| 93 | + ext (k | k) |
| 94 | + · simp [e, sq, ne_neg P i, -indexNeg_neg] |
| 95 | + · have aux : ∀ x : ι, x ∈ Finset.univ → ¬ (x = i ∧ P.root k = P.root i + P.root x) := by |
| 96 | + suffices P.root k ≠ (2 : ℕ) • P.root i by simpa [two_smul] |
| 97 | + exact fun contra ↦ P.nsmul_notMem_range_root (n := 2) (i := i) ⟨k, contra⟩ |
| 98 | + simp [e, sq, -indexNeg_neg, ← ite_and, Finset.sum_ite_of_false aux] |
| 99 | + rintro (j | j) |
| 100 | + · exact ⟨2, case_inl j⟩ |
| 101 | + · by_cases hij : j = -i |
| 102 | + · use 2 + 1 |
| 103 | + replace hij : (e i).col (Sum.inr j) = Pi.single (Sum.inl i) 1 := by |
| 104 | + ext (k | k) |
| 105 | + · simp [e, -indexNeg_neg, Pi.single_apply, hij] |
| 106 | + · have hk : P.root k ≠ P.root i + P.root j := by simp [hij, P.ne_zero k] |
| 107 | + simp [e, -indexNeg_neg, hk] |
| 108 | + rw [pow_succ, ← Matrix.mulVec_single_one, ← Matrix.mulVec_mulVec] |
| 109 | + simp [hij, case_inl i] |
| 110 | + use P.chainTopCoeff i j + 1 |
| 111 | + rcases isNilpotent_e_aux i (P.chainTopCoeff i j + 1) hij with this | ⟨k, x, hk₁, -⟩ |
| 112 | + · assumption |
| 113 | + exfalso |
| 114 | + replace hk₁ : P.root j + (P.chainTopCoeff i j + 1) • P.root i ∈ range P.root := ⟨k, hk₁⟩ |
| 115 | + have hij' : LinearIndependent R ![P.root i, P.root j] := by |
| 116 | + apply IsReduced.linearIndependent P ?_ ?_ |
| 117 | + · rintro rfl |
| 118 | + apply P.nsmul_notMem_range_root (n := P.chainTopCoeff i i + 2) (i := i) |
| 119 | + convert hk₁ using 1 |
| 120 | + module |
| 121 | + · contrapose! hij |
| 122 | + rw [root_eq_neg_iff] at hij |
| 123 | + rw [hij, ← indexNeg_neg, neg_neg] |
| 124 | + rw [root_add_nsmul_mem_range_iff_le_chainTopCoeff hij'] at hk₁ |
| 125 | + omega |
| 126 | + |
| 127 | +lemma isNilpotent_f : |
| 128 | + IsNilpotent (f i) := by |
| 129 | + obtain ⟨n, hn⟩ := isNilpotent_e i |
| 130 | + suffices (ω b) * (f i ^ n) = 0 from ⟨n, by simpa [← mul_assoc] using congr_arg (ω b * ·) this⟩ |
| 131 | + suffices (ω b) * (f i ^ n) = (e i ^ n) * (ω b) by simp [this, hn] |
| 132 | + clear hn |
| 133 | + induction n with |
| 134 | + | zero => simp |
| 135 | + | succ n ih => rw [pow_succ, pow_succ, ← mul_assoc, ih, mul_assoc, ω_mul_f, ← mul_assoc] |
| 136 | + |
| 137 | +omit [P.IsReduced] [IsDomain R] in |
| 138 | +@[simp] lemma trace_h_eq_zero : |
| 139 | + (h i).trace = 0 := by |
| 140 | + letI _i := P.indexNeg |
| 141 | + suffices ∑ j, P.pairingIn ℤ j i = 0 by |
| 142 | + simp only [h_eq_diagonal, Matrix.trace_diagonal, Fintype.sum_sum_type, Finset.univ_eq_attach, |
| 143 | + Sum.elim_inl, Pi.zero_apply, Finset.sum_const_zero, Sum.elim_inr, zero_add] |
| 144 | + norm_cast |
| 145 | + suffices ∑ j, P.pairingIn ℤ (-j) i = ∑ j, P.pairingIn ℤ j i from |
| 146 | + eq_zero_of_neg_eq <| by simpa using this |
| 147 | + let σ : ι ≃ ι := Function.Involutive.toPerm _ neg_involutive |
| 148 | + exact σ.sum_comp (P.pairingIn ℤ · i) |
| 149 | + |
| 150 | +open LinearMap LieModule in |
| 151 | +/-- This is the main result of lemma 4.1 from [Geck](Geck2017). -/ |
| 152 | +lemma trace_toEnd_eq_zero (x : lieAlgebra b) : |
| 153 | + trace R _ (toEnd R _ (b.support ⊕ ι → R) x) = 0 := by |
| 154 | + obtain ⟨x, hx⟩ := x |
| 155 | + suffices trace R _ x.toLin' = 0 by simpa |
| 156 | + refine LieAlgebra.trace_toEnd_eq_zero ?_ hx |
| 157 | + rintro - ((⟨i, rfl⟩ | ⟨i, rfl⟩) | ⟨i, rfl⟩) |
| 158 | + · simp |
| 159 | + · simpa using Matrix.isNilpotent_trace_of_isNilpotent (isNilpotent_e i) |
| 160 | + · simpa using Matrix.isNilpotent_trace_of_isNilpotent (isNilpotent_f i) |
| 161 | + |
| 162 | +end RootPairing.GeckConstruction |
0 commit comments