Lax Lean Archive

FormalExistence of formal realizations

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

    For a finite alphabet, a series admits a finite-dimensional formal differential representation if and only if its Lie rank is finite. If it has Lie rank dd, a formal differential representation of dimension exactly dd exists.

    Concept map
    10 concepts; 5 descendants hidden
    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 characterization proven

    2 existence proven

    Lean source view on GitHub

    1import Lax825748.DifferentialRepresentation
    2import Lax825748.Annihilator
    3
    4/-!
    5---
    6title: FormalExistence of formal realizations
    7type: theorem
    8---
    9For a finite alphabet, a series admits a finite-dimensional formal differential
    10representation if and only if its Lie rank is finite. If it has Lie rank dd,
    11a formal differential representation of dimension exactly dd exists.
    12-/
    13
    14noncomputable section
    15
    16namespace Lax825748.FormalRealization
    17
    18open Series LieRank DifferentialRepresentation
    19
    20axiom existence {X : Type} [Finite X] (g : NCSeries X) (d : ℕ)
    21 (hr : HasLieRank g d) :
    22 ∃ R : Representation X d, Represents R g
    23
    24axiom characterization {X : Type} [Finite X] (g : NCSeries X) :
    25 DifferentiallyProduced g ↔ FiniteLieRank g
    26
    27end Lax825748.FormalRealization
    28
    Show 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…