Lax Lean Archive

CDA coefficients in minimal formal realizations

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

proven

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

    Theorem

    In normalized shuffle-finite coordinates, all elements of the witnessing shuffle algebra that belong to the coordinate annihilator have expansions in one finitely generated algebra stable under ordinary partial derivatives. In particular, a minimal realization has CDA output and CDA vector-field coefficients, while its coordinate series remain shuffle finite.

    Concept map
    14 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

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

    1 coordinate_algebra proven

    2 minimal_realization proven

    Lean source view on GitHub

    1import Lax825748.CDA
    2import Lax825748.ShuffleFiniteCoordinates
    3
    4/-!
    5---
    6title: CDA coefficients in minimal formal realizations
    7type: theorem
    8---
    9In normalized shuffle-finite coordinates, all elements of the witnessing
    10shuffle algebra that belong to the coordinate annihilator have expansions
    11in one finitely generated algebra stable under ordinary partial derivatives.
    12In particular, a minimal realization has CDA output and CDA vector-field
    13coefficients, while its coordinate series remain shuffle finite.
    14-/
    15
    16noncomputable section
    17
    18namespace Lax825748.CDACoefficients
    19
    20open Series LieRank Annihilator FormalSeries ShuffleFinite
    21open DifferentialRepresentation RepresentationMap CDA
    22
    23axiom coordinate_algebra {X : Type} {k : ℕ}
    24 (A : ShuffleSubalgebra X) (hfg : FinitelyGenerated A)
    25 (hstable : ShuffleFinite.DerivativeStable A)
    26 (K : LieSubalgebraOfPolynomials X) (P : Fin k → LiePolynomial X)
    27 (hP : IsComplement K P) (G : Fin k → NCSeries X)
    28 (hG : IsCoordinateFamily K P G) (hmem : ∀ i, G i ∈ A.toSubmodule) :
    29 ∃ C : Subalgebra ℝ (StateSeries k), C.FG ∧ CDA.DerivativeStable C ∧
    30 ∀ u : StateSeries k, substituteShuffle G u ∈ A.toSubmodule → u ∈ C
    31
    32axiom minimal_realization {X : Type} [Finite X] (f : NCSeries X) (k : ℕ)
    33 (hr : HasLieRank f k) (A : ShuffleSubalgebra X)
    34 (hfg : FinitelyGenerated A) (hstable : ShuffleFinite.DerivativeStable A)
    35 (hf : f ∈ A.toSubmodule) :
    36 ∃ R : Representation X k, Represents R f ∧ IsCDA R.output ∧
    37 (∀ (x : X) (i : Fin k), IsCDA (R.fields x i)) ∧
    38 ∀ i : Fin k, eta R (MvPowerSeries.X i) ∈ A.toSubmodule ∧
    39 IsShuffleFinite (eta R (MvPowerSeries.X i))
    40
    41end Lax825748.CDACoefficients
    42
    Show ProofShow Proof
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

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

    Loading discussion…