Lax Lean Archive

Prevarieties and effective prevarieties of series

Lax619925.Prevariety · concepts/Lax619925/Prevariety.lean · lax-619925

definition

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

    Definition

    A prevariety of series over an alphabet αα is a Qℚ-subspace of the series closed under the left and right derivatives (paper §2.3, conditions (V.1) and (V.2)). An effective prevariety is a prevariety whose elements admit finite presentations (a type RepRep with a semantics map) such that the closure operations are carried out algorithmically on presentations and the equality problem is decidable (paper §2.3, conditions (1)–(3)). These are definitions only; the decidability results built on them live in the CommutativityCommutativity module.

    Concept map
    2 concepts; 8 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    In the paper

    • page 9 of this submission's paper

    Lean source view on GitHub

    1import Lax619925.Series
    2import Mathlib.Data.Real.Basic
    3import Mathlib.Algebra.Module.Basic
    4import Mathlib.Algebra.Module.Pi
    5import Mathlib.Algebra.Module.Submodule.Basic
    6
    7universe u
    8
    9/-!
    10---
    11title: Prevarieties and effective prevarieties of series
    12type: definition
    13---
    14A *prevariety* of series over an alphabet `α` is a `ℚ`-subspace of the series
    15closed under the left and right derivatives (paper §2.3, conditions (V.1) and
    16(V.2)). An *effective prevariety* is a prevariety whose elements admit finite
    17presentations (a type `Rep` with a semantics map) such that the closure
    18operations are carried out algorithmically on presentations and the equality
    19problem is decidable (paper §2.3, conditions (1)–(3)). These are definitions
    20only; the decidability results built on them live in the `Commutativity` module.
    21-/
    22
    23namespace Lax619925.Prevariety
    24
    25open Lax619925.Series
    26
    27-- the type and the module carrying it have the same name on purpose
    28set_option linter.dupNamespace false in
    29/-- A prevariety of series over `α`: a `ℚ`-subspace of `Series α` (the field
    30 `carrier`) that is closed under the left and right derivatives. -/
    31structure Prevariety (α : Type*) where
    32 carrier : Submodule ℚ (Series α)
    33 closedLeftDeriv : ∀ {f : Series α} (_hf : f ∈ carrier), ∀ a, leftDeriv α a f ∈ carrier
    34 closedRightDeriv : ∀ {f : Series α} (_hf : f ∈ carrier), ∀ a, rightDeriv α a f ∈ carrier
    35
    36/-- Coercion from a prevariety to its underlying `ℚ`-submodule. -/
    37instance (α : Type*) : Coe (Prevariety α) (Submodule ℚ (Series α)) where
    38 coe P := P.carrier
    39
    40/-- Membership in a prevariety: `f ∈ P` means that `f` belongs to the underlying
    41 `ℚ`-subspace of `P`. -/
    42instance (α : Type*) : Membership (Series α) (Prevariety α) where
    43 mem P f := f ∈ P.carrier
    44
    45/-- An effective prevariety of series over `α`: a prevariety given by a type `Rep`
    46 of finite presentations with a semantics map `sem`, in which the vector-space
    47 operations and the left and right derivatives are computed by operations on
    48 presentations (the `sem_*` fields record their correctness), and on which the
    49 equality problem is decidable. The fields `prevariety` and `mem` record that
    50 the image of the semantics is a prevariety. -/
    51structure EffectivePrevariety (α : Type u) where
    52 Rep : Type u
    53 sem : Rep → Series α
    54 prevariety : Prevariety α
    55 mem : ∀ r, sem r ∈ prevariety
    56 zero : Rep
    57 add : Rep → Rep → Rep
    58 smul : ℚ → Rep → Rep
    59 derivL : α → Rep → Rep
    60 derivR : α → Rep → Rep
    61 sem_zero : sem zero = 0
    62 sem_add : ∀ r s, sem (add r s) = sem r + sem s
    63 sem_smul : ∀ c r, sem (smul c r) = c • sem r
    64 sem_derivL : ∀ a r, sem (derivL a r) = leftDeriv α a (sem r)
    65 sem_derivR : ∀ a r, sem (derivR a r) = rightDeriv α a (sem r)
    66 decEq : ∀ r s, Decidable (sem r = sem s)
    67
    68end Lax619925.Prevariety
    69
    Builds on
    Used by
    From Mathlib

    Discussion

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

    Loading discussion…