Lax Lean Archive

Formal equivalence of minimal realizations

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

    Two formal differential representations of a series of Lie rank dd, both of dimension dd, are equivalent under a formal change of coordinates fixing the origin. The change sends the first output series to the second and intertwines the right action of every word on every state series. The change of coordinates and its inverse are continuous for the formal topology.

    Concept map
    15 concepts; 1 descendant hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax825748.FormalMinimality
    2import Lax825748.CoordinateChange
    3import Lax825748.Projection
    4import Lax825748.RepresentationMap
    5
    6/-!
    7---
    8title: Formal equivalence of minimal realizations
    9type: theorem
    10---
    11Two formal differential representations of a series of Lie rank dd, both of
    12dimension dd, are equivalent under a formal change of coordinates
    13fixing the origin. The change sends the first output series to the second
    14and intertwines the right action of every word on every state series.
    15The change of coordinates and its inverse are continuous for the formal topology.
    16-/
    17
    18noncomputable section
    19
    20namespace Lax825748.FormalUniqueness
    21
    22open Series LieRank DifferentialRepresentation CoordinateChange
    23
    24axiom minimal_realizations_equivalent {X : Type} [Finite X] {d : ℕ}
    25 (g : NCSeries X) (hr : HasLieRank g d)
    26 (R R' : Representation X d) (hR : Represents R g) (hR' : Represents R' g) :
    27 ∃ φ : FormalChange d,
    28 φ.toAlgEquiv R.output = R'.output ∧
    29 ∀ (k : FormalSeries.StateSeries d) (w : Word X),
    30 φ.toAlgEquiv (act R k w) = act R' (φ.toAlgEquiv k) w
    31
    32end Lax825748.FormalUniqueness
    33
    Show 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…