Documentation

Mathlib.Algebra.Lie.Basis.Base

The root system base associated to a Lie algebra basis #

source
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
Instances For
    source
    @[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
    source
    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')
    source
    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')
    source
    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
    Instances For
      source
      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
      Instances For
        source
        @[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
        source
        @[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
        source
        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
        source
        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) = ⊤
        source
        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)
        source
        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
        Instances For