The root system associated with a Lie algebra

We show that the roots of a finite dimensional splitting semisimple Lie algebra over a field of characteristic 0 form a root system. We achieve this by studying root chains.

Main results

• LieAlgebra.IsKilling.apply_coroot_eq_cast: If β - qα ... β ... β + rα is the α-chain through β, then β (coroot α) = q - r. In particular, it is an integer.

• LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iff: The α-chain through β (β - qα ... β ... β + rα) are the only roots of the form β + kα.

• LieAlgebra.IsKilling.eq_neg_or_eq_of_eq_smul: ±α are the only K-multiples of a root α that are also (non-zero) roots.

• LieAlgebra.IsKilling.rootSystem: The root system of a finite-dimensional Lie algebra with non-degenerate Killing form over a field of characteristic zero, relative to a splitting Cartan subalgebra.

def LieAlgebra.IsKilling.chainLength {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L) : ℕ

The length of the α-chain through β. See chainBotCoeff_add_chainTopCoeff.

theorem LieAlgebra.IsKilling.chainLength_of_isZero {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L) (hα : α.IsZero) : chainLength α β = 0

theorem LieAlgebra.IsKilling.chainLength_nsmul {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L) {x : L} (hx : x ∈ rootSpace H ⇑(LieModule.chainTop (⇑α) β)) : chainLength α β • x = ⁅coroot α, x⁆

theorem LieAlgebra.IsKilling.chainLength_smul {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L) {x : L} (hx : x ∈ rootSpace H ⇑(LieModule.chainTop (⇑α) β)) : ↑(chainLength α β) • x = ⁅coroot α, x⁆

theorem LieAlgebra.IsKilling.apply_coroot_eq_cast' {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L) : β (coroot α) = ↑(↑(chainLength α β) - 2 * ↑(LieModule.chainTopCoeff (⇑α) β))

theorem LieAlgebra.IsKilling.rootSpace_neg_nsmul_add_chainTop_of_le {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L) {n : ℕ} (hn : n ≤ chainLength α β) : rootSpace H (-(n • ⇑α) + ⇑(LieModule.chainTop (⇑α) β)) ≠ ⊥

theorem LieAlgebra.IsKilling.rootSpace_neg_nsmul_add_chainTop_of_lt {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L) (hα : α.IsNonZero) {n : ℕ} (hn : chainLength α β < n) : rootSpace H (-(n • ⇑α) + ⇑(LieModule.chainTop (⇑α) β)) = ⊥

theorem LieAlgebra.IsKilling.chainTopCoeff_le_chainLength {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L) : LieModule.chainTopCoeff (⇑α) β ≤ chainLength α β

theorem LieAlgebra.IsKilling.chainBotCoeff_add_chainTopCoeff {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L) : LieModule.chainBotCoeff (⇑α) β + LieModule.chainTopCoeff (⇑α) β = chainLength α β

theorem LieAlgebra.IsKilling.chainTopCoeff_add_chainBotCoeff {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L) : LieModule.chainTopCoeff (⇑α) β + LieModule.chainBotCoeff (⇑α) β = chainLength α β

theorem LieAlgebra.IsKilling.chainBotCoeff_le_chainLength {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L) : LieModule.chainBotCoeff (⇑α) β ≤ chainLength α β

@[simp]

theorem LieAlgebra.IsKilling.chainLength_neg {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L) : chainLength (-α) β = chainLength α β

@[simp]

theorem LieAlgebra.IsKilling.chainLength_zero {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (β : LieModule.Weight K (↥H) L) [Nontrivial L] : chainLength 0 β = 0

theorem LieAlgebra.IsKilling.apply_coroot_eq_cast {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L) : β (coroot α) = ↑(↑(LieModule.chainBotCoeff (⇑α) β) - ↑(LieModule.chainTopCoeff (⇑α) β))

If β - qα ... β ... β + rα is the α-chain through β, then β (coroot α) = q - r. In particular, it is an integer.

theorem LieAlgebra.IsKilling.le_chainBotCoeff_of_rootSpace_ne_top {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L) (hα : α.IsNonZero) (n : ℤ) (hn : rootSpace H (-n • ⇑α + ⇑β) ≠ ⊥) : n ≤ ↑(LieModule.chainBotCoeff (⇑α) β)

theorem LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iff {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L) (hα : α.IsNonZero) (n : ℤ) : rootSpace H (n • ⇑α + ⇑β) ≠ ⊥ ↔ n ≤ ↑(LieModule.chainTopCoeff (⇑α) β) ∧ -n ≤ ↑(LieModule.chainBotCoeff (⇑α) β)

Members of the α-chain through β are the only roots of the form β - kα.

theorem LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iff_mem {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L) (hα : α.IsNonZero) (n : ℤ) : rootSpace H (n • ⇑α + ⇑β) ≠ ⊥ ↔ n ∈ Finset.Icc (-↑(LieModule.chainBotCoeff (⇑α) β)) ↑(LieModule.chainTopCoeff (⇑α) β)

theorem LieAlgebra.IsKilling.chainTopCoeff_of_eq_zsmul_add {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L) (hα : α.IsNonZero) (β' : LieModule.Weight K (↥H) L) (n : ℤ) (hβ' : ⇑β' = n • ⇑α + ⇑β) : ↑(LieModule.chainTopCoeff (⇑α) β') = ↑(LieModule.chainTopCoeff (⇑α) β) - n

theorem LieAlgebra.IsKilling.chainBotCoeff_of_eq_zsmul_add {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L) (hα : α.IsNonZero) (β' : LieModule.Weight K (↥H) L) (n : ℤ) (hβ' : ⇑β' = n • ⇑α + ⇑β) : ↑(LieModule.chainBotCoeff (⇑α) β') = ↑(LieModule.chainBotCoeff (⇑α) β) + n

theorem LieAlgebra.IsKilling.chainLength_of_eq_zsmul_add {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (α β β' : LieModule.Weight K (↥H) L) (n : ℤ) (hβ' : ⇑β' = n • ⇑α + ⇑β) : chainLength α β' = chainLength α β

theorem LieAlgebra.IsKilling.chainTopCoeff_zero_right {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (α : LieModule.Weight K (↥H) L) [Nontrivial L] (hα : α.IsNonZero) : LieModule.chainTopCoeff (⇑α) 0 = 1

theorem LieAlgebra.IsKilling.chainBotCoeff_zero_right {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (α : LieModule.Weight K (↥H) L) [Nontrivial L] (hα : α.IsNonZero) : LieModule.chainBotCoeff (⇑α) 0 = 1

theorem LieAlgebra.IsKilling.chainLength_zero_right {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (α : LieModule.Weight K (↥H) L) [Nontrivial L] (hα : α.IsNonZero) : chainLength α 0 = 2

theorem LieAlgebra.IsKilling.rootSpace_two_smul {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (α : LieModule.Weight K (↥H) L) (hα : α.IsNonZero) : rootSpace H (2 • ⇑α) = ⊥

theorem LieAlgebra.IsKilling.rootSpace_one_div_two_smul {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (α : LieModule.Weight K (↥H) L) (hα : α.IsNonZero) : rootSpace H (2⁻¹ • ⇑α) = ⊥

theorem LieAlgebra.IsKilling.eq_neg_one_or_eq_zero_or_eq_one_of_eq_smul {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L) (hα : α.IsNonZero) (k : K) (h : ⇑β = k • ⇑α) : k = -1 ∨ k = 0 ∨ k = 1

theorem LieAlgebra.IsKilling.eq_neg_or_eq_of_eq_smul {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L) (hβ : β.IsNonZero) (k : K) (h : ⇑β = k • ⇑α) : β = -α ∨ β = α

±α are the only K-multiples of a root α that are also (non-zero) roots.

def LieAlgebra.IsKilling.reflectRoot {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L) : LieModule.Weight K (↥H) L

The reflection of a root along another.

theorem LieAlgebra.IsKilling.reflectRoot_isNonZero {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L) (hβ : β.IsNonZero) : (reflectRoot α β).IsNonZero

def LieAlgebra.IsKilling.rootSystem {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] : RootSystem { x : LieModule.Weight K (↥H) L // x ∈ LieSubalgebra.root } K (Module.Dual K ↥H) ↥H

The root system of a finite-dimensional Lie algebra with non-degenerate Killing form over a field of characteristic zero, relative to a splitting Cartan subalgebra.

@[simp]

theorem LieAlgebra.IsKilling.corootForm_rootSystem_eq_killing {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] : (rootSystem H).CorootForm = (killingForm K L).restrict H.toSubmodule

@[simp]

theorem LieAlgebra.IsKilling.rootSystem_toPerfectPairing_apply {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (f : Module.Dual K ↥H) (x : ↥H) : ((rootSystem H).toPerfectPairing f) x = f x

@[simp]

theorem LieAlgebra.IsKilling.rootSystem_pairing_apply {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (α β : { x : LieModule.Weight K (↥H) L // x ∈ LieSubalgebra.root }) : (rootSystem H).pairing β α = ↑β (coroot ↑α)

@[simp]

theorem LieAlgebra.IsKilling.rootSystem_root_apply {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (α : { x : LieModule.Weight K (↥H) L // x ∈ LieSubalgebra.root }) : (rootSystem H).root α = LieModule.Weight.toLinear K (↥H) L ↑α

@[simp]

theorem LieAlgebra.IsKilling.rootSystem_coroot_apply {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (α : { x : LieModule.Weight K (↥H) L // x ∈ LieSubalgebra.root }) : (rootSystem H).coroot α = coroot ↑α

instance LieAlgebra.IsKilling.instIsCrystallographicSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] : (rootSystem H).IsCrystallographic

instance LieAlgebra.IsKilling.instIsReducedSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] : (rootSystem H).IsReduced

theorem LieAlgebra.IsKilling.eq_top_of_invtSubmodule_ne_bot {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] [IsSimple K L] (q : Submodule K (Module.Dual K ↥H)) (h₀ : ∀ (i : { x : LieModule.Weight K (↥H) L // x ∈ LieSubalgebra.root }), q ∈ Module.End.invtSubmodule ↑((rootSystem H).reflection i)) (h₁ : q ≠ ⊥) : q = ⊤

instance LieAlgebra.IsKilling.instIsIrreducibleSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] [IsSimple K L] : (rootSystem H).IsIrreducible