Documentation

Mathlib.Algebra.Lie.Rank

Rank of a Lie algebra and regular elements #

Let L be a Lie algebra over a nontrivial commutative ring R, and assume that L is finite free as R-module. Then the coefficients of the characteristic polynomial of ad R L x are polynomial in x. The rank of L is the smallest n for which the n-th coefficient is not the zero polynomial.

Continuing to write n for the rank of L, an element x of L is regular if the n-th coefficient of the characteristic polynomial of ad R L x is non-zero.

Main declarations #

References #

noncomputable def LieModule.rank (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Finite R M] [Module.Free R M] :

Let M be a representation of a Lie algebra L over a nontrivial commutative ring R, and assume that L and M are finite free as R-module. Then the coefficients of the characteristic polynomial of ⁅x, ·⁆ are polynomial in x. The rank of M is the smallest n for which the n-th coefficient is not the zero polynomial.

Equations
Instances For
    theorem LieModule.polyCharpoly_coeff_rank_ne_zero (R : Type u_1) (L : Type u_3) (M : Type u_4) {ι : Type u_5} [CommRing R] [Nontrivial R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Finite R M] [Module.Free R M] [Fintype ι] [DecidableEq ι] (b : Basis ι R L) :
    (((LieModule.toEnd R L M)).polyCharpoly b).coeff (LieModule.rank R L M) 0
    theorem LieModule.rank_eq_natTrailingDegree (R : Type u_1) (L : Type u_3) (M : Type u_4) {ι : Type u_5} [CommRing R] [Nontrivial R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Finite R M] [Module.Free R M] [Fintype ι] [DecidableEq ι] (b : Basis ι R L) :
    LieModule.rank R L M = (((LieModule.toEnd R L M)).polyCharpoly b).natTrailingDegree
    theorem LieModule.rank_le_card (R : Type u_1) (L : Type u_3) (M : Type u_4) {ιₘ : Type u_6} [CommRing R] [Nontrivial R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Finite R M] [Module.Free R M] [Fintype ιₘ] (bₘ : Basis ιₘ R M) :
    theorem LieModule.rank_le_natTrailingDegree_charpoly_ad (R : Type u_1) {L : Type u_3} (M : Type u_4) [CommRing R] [Nontrivial R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Finite R M] [Module.Free R M] (x : L) :
    LieModule.rank R L M (LinearMap.charpoly ((LieModule.toEnd R L M) x)).natTrailingDegree
    def LieModule.IsRegular (R : Type u_1) {L : Type u_3} (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Finite R M] [Module.Free R M] (x : L) :

    Let x be an element of a Lie algebra L over R, and write n for rank R L. Then x is regular if the n-th coefficient of the characteristic polynomial of ad R L x is non-zero.

    Equations
    Instances For
      theorem LieModule.isRegular_def (R : Type u_1) {L : Type u_3} (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Finite R M] [Module.Free R M] (x : L) :
      theorem LieModule.isRegular_iff_coeff_polyCharpoly_rank_ne_zero (R : Type u_1) {L : Type u_3} (M : Type u_4) {ι : Type u_5} [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Finite R M] [Module.Free R M] [Fintype ι] [DecidableEq ι] (b : Basis ι R L) (x : L) :
      LieModule.IsRegular R M x (MvPolynomial.eval (b.repr x)) ((((LieModule.toEnd R L M)).polyCharpoly b).coeff (LieModule.rank R L M)) 0
      theorem LieModule.exists_isRegular (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [Nontrivial R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Finite R M] [Module.Free R M] [IsDomain R] [Infinite R] :
      ∃ (x : L), LieModule.IsRegular R M x
      @[reducible, inline]
      noncomputable abbrev LieAlgebra.rank (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] :

      Let L be a Lie algebra over a nontrivial commutative ring R, and assume that L is finite free as R-module. Then the coefficients of the characteristic polynomial of ad R L x are polynomial in x. The rank of L is the smallest n for which the n-th coefficient is not the zero polynomial.

      Equations
      Instances For
        theorem LieAlgebra.polyCharpoly_coeff_rank_ne_zero (R : Type u_1) (L : Type u_3) {ι : Type u_5} [CommRing R] [Nontrivial R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] [Fintype ι] [DecidableEq ι] (b : Basis ι R L) :
        (((LieAlgebra.ad R L)).polyCharpoly b).coeff (LieAlgebra.rank R L) 0
        theorem LieAlgebra.rank_eq_natTrailingDegree (R : Type u_1) (L : Type u_3) {ι : Type u_5} [CommRing R] [Nontrivial R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] [Fintype ι] [DecidableEq ι] (b : Basis ι R L) :
        LieAlgebra.rank R L = (((LieAlgebra.ad R L)).polyCharpoly b).natTrailingDegree
        theorem LieAlgebra.rank_le_card (R : Type u_1) (L : Type u_3) {ι : Type u_5} [CommRing R] [Nontrivial R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] [Fintype ι] (b : Basis ι R L) :
        @[reducible, inline]
        abbrev LieAlgebra.IsRegular (R : Type u_1) {L : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] (x : L) :

        Let x be an element of a Lie algebra L over R, and write n for rank R L. Then x is regular if the n-th coefficient of the characteristic polynomial of ad R L x is non-zero.

        Equations
        Instances For
          theorem LieAlgebra.isRegular_def (R : Type u_1) {L : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] (x : L) :
          theorem LieAlgebra.isRegular_iff_coeff_polyCharpoly_rank_ne_zero (R : Type u_1) {L : Type u_3} {ι : Type u_5} [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] [Fintype ι] [DecidableEq ι] (b : Basis ι R L) (x : L) :
          LieAlgebra.IsRegular R x (MvPolynomial.eval (b.repr x)) ((((LieAlgebra.ad R L)).polyCharpoly b).coeff (LieAlgebra.rank R L)) 0
          theorem LieAlgebra.exists_isRegular (R : Type u_1) (L : Type u_3) [CommRing R] [Nontrivial R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] [IsDomain R] [Infinite R] :
          ∃ (x : L), LieAlgebra.IsRegular R x
          theorem LieAlgebra.finrank_engel (K : Type u_7) {L : Type u_8} [Field K] [LieRing L] [LieAlgebra K L] [Module.Finite K L] (x : L) :