Poincaré–Birkhoff–Witt for Lie polynomials

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

proven

Loading review…

Natural Language Statement

Theorem

Given any totally ordered basis of the Lie polynomials, the nondecreasing products of its basis elements, including the empty product, form a basis of the concatenation algebra $\mathbb R\langle X\rangle$ . Linear independence and spanning are stated separately in the conjunction.

Concept map

3 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

Evidence

Each proof establishes this claim relative to its assumptions.

- thm✓Lax825748.ShuffleIdentities
→
thm✓Lax825748.PBW
⊢Lax825748Proofs.PBW.basis

In the paper

page 5 of this submission's paper

Lean source view on GitHub

Show types on hover

1	import Lax825748.LieRank
2	import Mathlib.LinearAlgebra.Basis.Defs
3
4	/-!
5	---
6	title: Poincaré–Birkhoff–Witt for Lie polynomials
7	type: theorem
8	---
9	Given any totally ordered basis of the Lie polynomials, the nondecreasing
10	products of its basis elements, including the empty product, form a basis
11	of the concatenation algebra $\mathbb R\langle X\rangle$ .
12	Linear independence and spanning are stated separately in the conjunction.
13	-/
14
15	noncomputable section
16
17	namespace Lax825748.PBW
18
19	open Series LieRank
20
21	abbrev OrderedWord (ι : Type) [LinearOrder ι] :=
22	{l : List ι // l.Pairwise (· ≤ ·)}
23
24	noncomputable def monomial {X ι : Type} [LinearOrder ι]
25	(b : Module.Basis ι ℝ (LiePolynomial X)) (l : OrderedWord ι) : NCPolynomial X :=
26	(l.val.map fun i => (b i).val).prod
27
28	axiom basis {X ι : Type} [LinearOrder ι] (b : Module.Basis ι ℝ (LiePolynomial X)) :
29	LinearIndependent ℝ (monomial b) ∧
30	Submodule.span ℝ (Set.range (monomial b)) = ⊤
31
32	end Lax825748.PBW
33