Shuffle-finite series

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

definition

Loading review…

Natural Language Statement

Definition

A series is shuffle finite if it belongs to a finitely generated unital shuffle subalgebra stable under prefix derivatives. Finite generation is expressed by spanning all shuffle monomials in a finite family of series. Only finite linear combinations enter this algebra; its formal completion is a separate construction.

Concept map

6 concepts; 2 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

Show types on hover

1	import Lax825748.ShuffleIdentities
2	import Mathlib.LinearAlgebra.Span.Defs
3
4	/-!
5	---
6	title: Shuffle-finite series
7	type: definition
8	---
9	A series is shuffle finite if it belongs to a finitely generated unital
10	shuffle subalgebra stable under prefix derivatives. Finite generation is
11	expressed by spanning all shuffle monomials in a finite family of series.
12	Only finite linear combinations enter this algebra; its formal completion
13	is a separate construction.
14	-/
15
16	noncomputable section
17
18	namespace Lax825748.ShuffleFinite
19
20	open Series Shuffle ShuffleIdentities
21
22	structure ShuffleSubalgebra (X : Type) where
23	toSubmodule : Submodule ℝ (NCSeries X)
24	one_mem : constantSeries 1 ∈ toSubmodule
25	shuffle_mem : ∀ S T, S ∈ toSubmodule → T ∈ toSubmodule → shuffle S T ∈ toSubmodule
26
27	def FinitelyGenerated {X : Type} (A : ShuffleSubalgebra X) : Prop :=
28	∃ (n : ℕ) (S : Fin n → NCSeries X),
29	A.toSubmodule = Submodule.span ℝ (Set.range fun I : Fin n → ℕ => shuffleMonomial S I)
30
31	def DerivativeStable {X : Type} (A : ShuffleSubalgebra X) : Prop :=
32	∀ (x : X) (T : NCSeries X), T ∈ A.toSubmodule →
33	rightResidual T (letter x) ∈ A.toSubmodule
34
35	def IsShuffleFinite {X : Type} (f : NCSeries X) : Prop :=
36	∃ A : ShuffleSubalgebra X, FinitelyGenerated A ∧ DerivativeStable A ∧ f ∈ A.toSubmodule
37
38	end Lax825748.ShuffleFinite
39