Lax Lean Archive

Lie polynomials and Lie rank

Lax825748.LieRank · concepts/Lax825748/LieRank.lean · lax-825748

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    The Lie polynomials form the Lie subalgebra of R⟨X⟩\mathbb R\langle X\rangle generated by the letters, with bracket [P,Q]=PQ−QP[P,Q]=PQ-QP. The Lie residual space of gg is the linear span of the series P∘gP\circ g for Lie polynomials PP. The assertion that gg has Lie rank dd includes finite dimensionality; in particular an infinite-dimensional space never has rank zero by convention.

    Concept map
    2 concepts
    100%
    DefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

    In the paper

    • page 4 of this submission's paper

    Lean source view on GitHub

    1import Lax825748.Series
    2import Mathlib.Algebra.Lie.OfAssociative
    3import Mathlib.Algebra.Lie.Subalgebra
    4import Mathlib.LinearAlgebra.Dimension.Finite
    5
    6/-!
    7---
    8title: Lie polynomials and Lie rank
    9type: definition
    10---
    11The Lie polynomials form the Lie subalgebra of R⟨X⟩\mathbb R\langle X\rangle
    12generated by the letters, with bracket [P,Q]=PQ−QP[P,Q]=PQ-QP.
    13The Lie residual space of gg is the linear span of the series P∘gP\circ g
    14for Lie polynomials PP. The assertion that gg has Lie rank dd includes
    15finite dimensionality; in particular an infinite-dimensional space never
    16has rank zero by convention.
    17-/
    18
    19noncomputable section
    20
    21namespace Lax825748.LieRank
    22
    23open Series
    24
    25instance polynomialLieRing {X : Type} : LieRing (NCPolynomial X) :=
    26 LieRing.ofAssociativeRing
    27
    28def liePolynomials (X : Type) : LieSubalgebra ℝ (NCPolynomial X) :=
    29 LieSubalgebra.lieSpan ℝ (NCPolynomial X) (Set.range letter)
    30
    31abbrev LiePolynomial (X : Type) := liePolynomials X
    32
    33noncomputable def residualSpace {X : Type} (g : NCSeries X) :
    34 Submodule ℝ (NCSeries X) :=
    35 Submodule.span ℝ {S | ∃ P : LiePolynomial X, S = leftResidual P.val g}
    36
    37def HasLieRank {X : Type} (g : NCSeries X) (d : ℕ) : Prop :=
    38 Module.Finite ℝ (residualSpace g) ∧ Module.finrank ℝ (residualSpace g) = d
    39
    40def FiniteLieRank {X : Type} (g : NCSeries X) : Prop := ∃ d, HasLieRank g d
    41
    42end Lax825748.LieRank
    43
    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…