Formal coordinates on the annihilator of a Lie subalgebra

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

proven

Loading review…

Natural Language Statement

Theorem

Proposition 1. Let $L_0$ be a Lie subalgebra of the Lie polynomials and let $P_1,\ldots,P_d$ represent a basis modulo $L_0$ . Set $J=\mathbb R\langle X\rangle L_0$ . If the zero-constant series $S_i$ vanish on $J$ and satisfy $(S_i,P_j)=\delta_{ij}$ , substitution of the $S_i$ into commutative formal series is a bijection onto $J^\perp$ .

Substitution is defined coefficient by coefficient using a finite truncation: at a word of length $n$ , only monomials of degree at most $n$ contribute. There exist such coordinates dual to the degree-one PBW monomials. For these coordinates the coefficient of $S^I$ in $T\in J^\perp$ is $(T,P^I)/I!$ . The annihilator is closed under the shuffle and all right residuals.

Concept map

8 concepts

100%

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

Evidence

This concept declares 5 statements. Each proof establishes one of them relative to its assumptions.

In the paper

page 7 of this submission's paper

Lean source view on GitHub

Show types on hover

1	import Lax825748.PBW
2	import Lax825748.ShuffleIdentities
3	import Lax825748.FormalSeries
4	import Mathlib.RingTheory.Ideal.Span
5
6	/-!
7	---
8	title: Formal coordinates on the annihilator of a Lie subalgebra
9	type: theorem
10	---
11	Proposition 1. Let $L_0$ be a Lie subalgebra of the Lie polynomials and let
12	$P_1,\ldots,P_d$ represent a basis modulo $L_0$ . Set
13	$J=\mathbb R\langle X\rangle L_0$ . If the zero-constant series $S_i$ vanish
14	on $J$ and satisfy $(S_i,P_j)=\delta_{ij}$ , substitution of the $S_i$ into
15	commutative formal series is a bijection onto $J^\perp$ .
16
17	Substitution is defined coefficient by coefficient using a finite truncation:
18	at a word of length $n$ , only monomials of degree at most $n$ contribute.
19	There exist such coordinates dual to the degree-one PBW monomials. For these
20	coordinates the coefficient of $S^I$ in $T\in J^\perp$ is $(T,P^I)/I!$ .
21	The annihilator is closed under the shuffle and all right residuals.
22	-/
23
24	noncomputable section
25
26	namespace Lax825748.Annihilator
27
28	open Series LieRank Monomials Shuffle ShuffleIdentities FormalSeries
29
30	abbrev LieSubalgebraOfPolynomials (X : Type) := LieSubalgebra ℝ (LiePolynomial X)
31
32	noncomputable def generatedIdeal {X : Type} (K : LieSubalgebraOfPolynomials X) :
33	Ideal (NCPolynomial X) :=
34	Ideal.span {P \| ∃ k : K, P = k.val.val}
35
36	def InAnnihilator {X : Type} (K : LieSubalgebraOfPolynomials X) (S : NCSeries X) : Prop :=
37	∀ P ∈ generatedIdeal K, pairing S P = 0
38
39	def IsComplement {X : Type} {d : ℕ} (K : LieSubalgebraOfPolynomials X)
40	(P : Fin d → LiePolynomial X) : Prop :=
41	LinearIndependent ℝ (fun i => K.toSubmodule.mkQ (P i)) ∧
42	Submodule.span ℝ (Set.range fun i => K.toSubmodule.mkQ (P i)) = ⊤
43
44	def IsCoordinateFamily {X : Type} {d : ℕ} (K : LieSubalgebraOfPolynomials X)
45	(P : Fin d → LiePolynomial X) (S : Fin d → NCSeries X) : Prop :=
46	(∀ i, S i 1 = 0) ∧ (∀ i, InAnnihilator K (S i)) ∧
47	∀ i j, pairing (S i) (P j).val = if i = j then 1 else 0
48
49	noncomputable def substituteShuffle {X : Type} {d : ℕ}
50	(S : Fin d → NCSeries X) (f : StateSeries d) : NCSeries X :=
51	fun w => (AddMonoidAlgebra.coeff
52	(MvPowerSeries.truncTotal (w.toList.length + 1) f)).sum
53	fun I a => a * shuffleMonomial S I w
54
55	def IsPBWCoordinateFamily {X : Type} {d : ℕ}
56	(P : Fin d → LiePolynomial X) (S : Fin d → NCSeries X) : Prop :=
57	∀ i (I : Fin d →₀ ℕ),
58	pairing (S i) (orderedPowers (fun j => (P j).val) I) =
59	if I = Finsupp.single i 1 then 1 else 0
60
61	axiom coordinates_exist {X : Type} {d : ℕ} (K : LieSubalgebraOfPolynomials X)
62	(P : Fin d → LiePolynomial X) (hP : IsComplement K P) :
63	∃ S : Fin d → NCSeries X, IsCoordinateFamily K P S ∧ IsPBWCoordinateFamily P S
64
65	axiom formal_coordinates {X : Type} {d : ℕ} (K : LieSubalgebraOfPolynomials X)
66	(P : Fin d → LiePolynomial X) (hP : IsComplement K P)
67	(S : Fin d → NCSeries X) (hS : IsCoordinateFamily K P S) :
68	∀ T : NCSeries X, InAnnihilator K T ↔ ∃! f : StateSeries d, substituteShuffle S f = T
69
70	axiom pbw_expansion {X : Type} {d : ℕ} (K : LieSubalgebraOfPolynomials X)
71	(P : Fin d → LiePolynomial X) (hP : IsComplement K P)
72	(S : Fin d → NCSeries X) (hS : IsCoordinateFamily K P S)
73	(hPBW : IsPBWCoordinateFamily P S) (T : NCSeries X) (hT : InAnnihilator K T) :
74	∃ f : StateSeries d, substituteShuffle S f = T ∧
75	∀ I : Fin d →₀ ℕ, MvPowerSeries.coeff I f =
76	pairing T (orderedPowers (fun j => (P j).val) I) / (multiFactorial I : ℝ)
77
78	axiom closed_shuffle {X : Type} (K : LieSubalgebraOfPolynomials X)
79	(S T : NCSeries X) (hS : InAnnihilator K S) (hT : InAnnihilator K T) :
80	InAnnihilator K (shuffle S T)
81
82	axiom closed_residual {X : Type} (K : LieSubalgebraOfPolynomials X)
83	(S : NCSeries X) (hS : InAnnihilator K S) (P : NCPolynomial X) :
84	InAnnihilator K (rightResidual S P)
85
86	end Lax825748.Annihilator
87

Show ProofShow ProofShow ProofShow ProofShow Proof

Builds on

Used by

From Mathlib

Mathlib.RingTheory.Ideal.Span

Discussion

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

Loading discussion…

Lax Lean Archive

Formal coordinates on the annihilator of a Lie subalgebra

Flags

Flag this concept

Natural Language Statement

Theorem

1 `closed_residual` proven

2 `closed_shuffle` proven

3 `coordinates_exist` proven

4 `formal_coordinates` proven

5 `pbw_expansion` proven

In the paper

Lean source view on GitHub

Discussion

Settings