The root system base associated to a Lie algebra basis

noncomputable def LieAlgebra.Basis.baseSupp' {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} {ι : Type u_3} [Fintype ι] (b : Basis ι H) (i : ι) : ↥LieSubalgebra.root

The elements LieAlgebra.Basis.baseSupp as roots in the sense of LieSubalgebra.root.

Equations

• b.baseSupp' i = ⟨{ toFun := ⇑(b.baseSupp i), genWeightSpace_ne_bot' := ⋯ }, ⋯⟩

@[simp]

theorem LieAlgebra.Basis.coe_linearMap_baseSupp' {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} {ι : Type u_3} [Fintype ι] (b : Basis ι H) (i : ι) : LieModule.Weight.toLinear K (↥H) L ↑(b.baseSupp' i) = b.baseSupp i

theorem LieAlgebra.Basis.linearIndepOn_root_baseSupp {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} {ι : Type u_3} [Fintype ι] (b : Basis ι H) [LieModule.IsTriangularizable K (↥H) L] [IsKilling K L] : LinearIndepOn K (⇑(IsKilling.rootSystem H).root) (Set.range b.baseSupp')

theorem LieAlgebra.Basis.root_mem_or_mem_neg {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} {ι : Type u_3} [Fintype ι] (b : Basis ι H) [LieModule.IsTriangularizable K (↥H) L] [IsKilling K L] (χ : ↥LieSubalgebra.root) : (IsKilling.rootSystem H).root χ ∈ AddSubmonoid.closure (⇑(IsKilling.rootSystem H).root '' Set.range b.baseSupp') ∨ -(IsKilling.rootSystem H).root χ ∈ AddSubmonoid.closure (⇑(IsKilling.rootSystem H).root '' Set.range b.baseSupp')

noncomputable def LieAlgebra.Basis.base {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} {ι : Type u_3} [Fintype ι] (b : Basis ι H) [LieModule.IsTriangularizable K (↥H) L] [IsKilling K L] : (IsKilling.rootSystem H).Base

The distinguished root system base associated to a basis.

Equations

• b.base = RootPairing.Base.mk' (LieAlgebra.IsKilling.rootSystem H) (Set.range b.baseSupp') ⋯ ⋯

noncomputable def LieAlgebra.Basis.baseSupportEquiv {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} {ι : Type u_3} [Fintype ι] (b : Basis ι H) [LieModule.IsTriangularizable K (↥H) L] [IsKilling K L] : ι ≃ ↥b.base.support

The support of LieAlgebra.Basis.base is in one-to-one correspondence with the indexing set of the basis.

Equations

• b.baseSupportEquiv = (Equiv.ofInjective b.baseSupp' ⋯).trans ⋯.subtypeEquivToFinset

@[simp]

theorem LieAlgebra.Basis.coe_baseSupportEquiv_apply {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} {ι : Type u_3} [Fintype ι] (b : Basis ι H) [LieModule.IsTriangularizable K (↥H) L] [IsKilling K L] (i : ι) : LieModule.Weight.toLinear K (↥H) L ↑↑(b.baseSupportEquiv i) = b.baseSupp i

@[simp]

theorem LieAlgebra.Basis.coroot_eq_h' {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} {ι : Type u_3} [Fintype ι] (b : Basis ι H) [LieModule.IsTriangularizable K (↥H) L] [IsKilling K L] (i : ι) : IsKilling.coroot ↑↑(b.baseSupportEquiv i) = b.h' i

theorem LieAlgebra.Basis.cartanMatrix_base_eq {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} {ι : Type u_3} [Fintype ι] (b : Basis ι H) [LieModule.IsTriangularizable K (↥H) L] [IsKilling K L] : b.base.cartanMatrix = (Matrix.reindex b.baseSupportEquiv b.baseSupportEquiv) b.A

theorem LieAlgebra.lieSpan_range_union_eq_top_of_mem_rootSpace {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] [IsKilling K L] (b : (IsKilling.rootSystem H).Base) (e f : ↥b.support → L) (ef_sl2 : ∀ (α : ↥b.support), IsSl2Triple (↑((IsKilling.rootSystem H).coroot ↑α)) (e α) (f α)) (e_mem : ∀ (α : ↥b.support), e α ∈ rootSpace H ⇑(LieModule.Weight.toLinear K (↥H) L ↑↑α)) (f_mem : ∀ (α : ↥b.support), f α ∈ rootSpace H (-⇑(LieModule.Weight.toLinear K (↥H) L ↑↑α))) : LieSubalgebra.lieSpan K L (Set.range e ∪ Set.range f) = ⊤

theorem LieAlgebra.exists_basis_of_base {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] [IsKilling K L] (b : (IsKilling.rootSystem H).Base) : ∃ (B : Basis (↥b.support) H), B.A = b.cartanMatrix ∧ ∀ (i : ↥b.support), B.h i = ↑((IsKilling.rootSystem H).coroot ↑i)

noncomputable def LieAlgebra.equivOfRootSystemEquiv {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {L₂ : Type u_3} [LieRing L₂] [LieAlgebra K L₂] [FiniteDimensional K L₂] {H₂ : LieSubalgebra K L₂} [H₂.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H₂) L₂] [IsSimple K L] [IsSimple K L₂] (e : (IsKilling.rootSystem H).Equiv (IsKilling.rootSystem H₂)) : L ≃ₗ⁅K⁆ L₂

Lie algebras with equivalent root systems are equivalent.

Equations

• LieAlgebra.equivOfRootSystemEquiv e = LieAlgebra.Basis.equivOfReindex (⋯.some.supportMapEquiv e) ⋯.choose ⋯.choose ⋯