The root system base associated to a Lie algebra basis

noncomputable def LieAlgebra.Basis.baseSupp' {ι : Type u_1} {K : Type u_2} {L : Type u_3} [Fintype ι] [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} (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' {ι : Type u_1} {K : Type u_2} {L : Type u_3} [Fintype ι] [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} (b : Basis ι H) (i : ι) : LieModule.Weight.toLinear K (↥H) L ↑(b.baseSupp' i) = b.baseSupp i

theorem LieAlgebra.Basis.linearIndepOn_root_baseSupp {ι : Type u_1} {K : Type u_2} {L : Type u_3} [Fintype ι] [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} (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 {ι : Type u_1} {K : Type u_2} {L : Type u_3} [Fintype ι] [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} (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 {ι : Type u_1} {K : Type u_2} {L : Type u_3} [Fintype ι] [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} (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 {ι : Type u_1} {K : Type u_2} {L : Type u_3} [Fintype ι] [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} (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 {ι : Type u_1} {K : Type u_2} {L : Type u_3} [Fintype ι] [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} (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' {ι : Type u_1} {K : Type u_2} {L : Type u_3} [Fintype ι] [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} (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 {ι : Type u_1} {K : Type u_2} {L : Type u_3} [Fintype ι] [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} (b : Basis ι H) [LieModule.IsTriangularizable K (↥H) L] [IsKilling K L] : b.base.cartanMatrix = (Matrix.reindex b.baseSupportEquiv b.baseSupportEquiv) b.A