Lax Lean Archive

The series homomorphism of a differential representation

Lax825748.RepresentationMap · concepts/Lax825748/RepresentationMap.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

    Lemma 6. The map η(k)w=(kμw)(0)\eta(k)_w=(k\mu w)(0) is a formally continuous real algebra homomorphism from the state series to the shuffle series, and η(kμw)=η(k)∘w\eta(k\mu w)=\eta(k)\circ w. Algebra preservation is expressed by its scalar, additive, and multiplicative identities, with shuffle multiplication written explicitly.

    Concept map
    6 concepts; 4 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

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

    1 algebra_homomorphism proven

    2 continuous proven

    3 intertwining proven

    In the paper

    • page 9 of this submission's paper

    Lean source view on GitHub

    1import Lax825748.DifferentialRepresentation
    2import Lax825748.Shuffle
    3
    4/-!
    5---
    6title: The series homomorphism of a differential representation
    7type: theorem
    8---
    9Lemma 6. The map η(k)w=(kμw)(0)\eta(k)_w=(k\mu w)(0) is a formally continuous real
    10algebra homomorphism from the state series to the shuffle series, and
    11η(kμw)=η(k)∘w\eta(k\mu w)=\eta(k)\circ w.
    12Algebra preservation is expressed by its scalar, additive, and multiplicative
    13identities, with shuffle multiplication written explicitly.
    14-/
    15
    16noncomputable section
    17
    18namespace Lax825748.RepresentationMap
    19
    20open Series FormalSeries DifferentialRepresentation Shuffle
    21
    22noncomputable def eta {X : Type} {d : ℕ} (R : Representation X d)
    23 (k : StateSeries d) : NCSeries X :=
    24 fun w => MvPowerSeries.constantCoeff (act R k w)
    25
    26axiom algebra_homomorphism {X : Type} {d : ℕ} (R : Representation X d) :
    27 (∀ a : ℝ, eta R (MvPowerSeries.C a) = constantSeries a) ∧
    28 (∀ f k, eta R (f + k) = eta R f + eta R k) ∧
    29 (∀ f k, eta R (f * k) = shuffle (eta R f) (eta R k))
    30
    31axiom continuous {X : Type} {d : ℕ} (R : Representation X d) :
    32 ∀ N, ∃ M, ∀ f k, FormalSeries.AgreeBelow M f k →
    33 Series.AgreeBelow N (eta R f) (eta R k)
    34
    35axiom intertwining {X : Type} {d : ℕ} (R : Representation X d)
    36 (k : StateSeries d) (w : Word X) :
    37 eta R (act R k w) = rightResidual (eta R k) (wordPolynomial w)
    38
    39end Lax825748.RepresentationMap
    40
    Show ProofShow ProofShow Proof
    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…