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] [LieAlgebra.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 length of the α-chain through β. See chainBotCoeff_add_chainTopCoeff.

Equations

• LieAlgebra.IsKilling.chainLength α β = if hα : α.IsZero then 0 else ⋯.choose

theorem LieAlgebra.IsKilling.chainLength_of_isZero {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.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) (hα : α.IsZero) : LieAlgebra.IsKilling.chainLength α β = 0

theorem LieAlgebra.IsKilling.chainLength_nsmul {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.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) {x : L} (hx : x ∈ LieAlgebra.rootSpace H ⇑(LieModule.chainTop (⇑α) β)) : LieAlgebra.IsKilling.chainLength α β • x = ⁅LieAlgebra.IsKilling.coroot α, x⁆

theorem LieAlgebra.IsKilling.chainLength_smul {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.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) {x : L} (hx : x ∈ LieAlgebra.rootSpace H ⇑(LieModule.chainTop (⇑α) β)) : ↑(LieAlgebra.IsKilling.chainLength α β) • x = ⁅LieAlgebra.IsKilling.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] [LieAlgebra.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) : β (LieAlgebra.IsKilling.coroot α) = ↑(↑(LieAlgebra.IsKilling.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] [LieAlgebra.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) {n : ℕ} (hn : n ≤ LieAlgebra.IsKilling.chainLength α β) : LieAlgebra.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] [LieAlgebra.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) (hα : α.IsNonZero) {n : ℕ} (hn : LieAlgebra.IsKilling.chainLength α β < n) : LieAlgebra.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] [LieAlgebra.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) : LieModule.chainTopCoeff (⇑α) β ≤ LieAlgebra.IsKilling.chainLength α β

theorem LieAlgebra.IsKilling.chainBotCoeff_add_chainTopCoeff {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.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) : LieModule.chainBotCoeff (⇑α) β + LieModule.chainTopCoeff (⇑α) β = LieAlgebra.IsKilling.chainLength α β

theorem LieAlgebra.IsKilling.chainTopCoeff_add_chainBotCoeff {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.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) : LieModule.chainTopCoeff (⇑α) β + LieModule.chainBotCoeff (⇑α) β = LieAlgebra.IsKilling.chainLength α β

theorem LieAlgebra.IsKilling.chainBotCoeff_le_chainLength {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.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) : LieModule.chainBotCoeff (⇑α) β ≤ LieAlgebra.IsKilling.chainLength α β

@[simp]

theorem LieAlgebra.IsKilling.chainLength_neg {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.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) : LieAlgebra.IsKilling.chainLength (-α) β = LieAlgebra.IsKilling.chainLength α β

@[simp]

theorem LieAlgebra.IsKilling.chainLength_zero {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (β : LieModule.Weight K (↥H) L) [Nontrivial L] : LieAlgebra.IsKilling.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] [LieAlgebra.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) : β (LieAlgebra.IsKilling.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] [LieAlgebra.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) (hα : α.IsNonZero) (n : ℤ) (hn : LieAlgebra.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] [LieAlgebra.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) (hα : α.IsNonZero) (n : ℤ) : LieAlgebra.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] [LieAlgebra.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) (hα : α.IsNonZero) (n : ℤ) : LieAlgebra.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] [LieAlgebra.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) (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] [LieAlgebra.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) (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] [LieAlgebra.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) (β' : LieModule.Weight K (↥H) L) (n : ℤ) (hβ' : ⇑β' = n • ⇑α + ⇑β) : LieAlgebra.IsKilling.chainLength α β' = LieAlgebra.IsKilling.chainLength α β

theorem LieAlgebra.IsKilling.chainTopCoeff_zero_right {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (α : LieModule.Weight K (↥H) L) (hα : α.IsNonZero) [Nontrivial L] : 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] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (α : LieModule.Weight K (↥H) L) (hα : α.IsNonZero) [Nontrivial L] : 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] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (α : LieModule.Weight K (↥H) L) (hα : α.IsNonZero) [Nontrivial L] : LieAlgebra.IsKilling.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] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (α : LieModule.Weight K (↥H) L) (hα : α.IsNonZero) : LieAlgebra.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] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (α : LieModule.Weight K (↥H) L) (hα : α.IsNonZero) : LieAlgebra.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] [LieAlgebra.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) (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] [LieAlgebra.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) (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] [LieAlgebra.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) : LieModule.Weight K (↥H) L

The reflection of a root along another.

Equations

• LieAlgebra.IsKilling.reflectRoot α β = { toFun := ⇑β - β (LieAlgebra.IsKilling.coroot α) • ⇑α, weightSpace_ne_bot' := ⋯ }

theorem LieAlgebra.IsKilling.reflectRoot_isNonZero {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.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) (hβ : β.IsNonZero) : (LieAlgebra.IsKilling.reflectRoot α β).IsNonZero

def LieAlgebra.IsKilling.rootSystem {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] : RootSystem { α : LieModule.Weight K (↥H) L // α.IsNonZero } 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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LieAlgebra.IsKilling.rootSystem_toLin_apply {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (f : Module.Dual K ↥H) (x : ↥H) : ((LieAlgebra.IsKilling.rootSystem H).toLin 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] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (α : { α : LieModule.Weight K (↥H) L // α.IsNonZero }) (β : { α : LieModule.Weight K (↥H) L // α.IsNonZero }) : (LieAlgebra.IsKilling.rootSystem H).pairing β α = ↑β (LieAlgebra.IsKilling.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] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (α : { α : LieModule.Weight K (↥H) L // α.IsNonZero }) : (LieAlgebra.IsKilling.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] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (α : { α : LieModule.Weight K (↥H) L // α.IsNonZero }) : (LieAlgebra.IsKilling.rootSystem H).coroot α = LieAlgebra.IsKilling.coroot ↑α

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

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