Documentation

LeanPool.Stafford38.AlgebraicAnalysis.Ore.IteratedPBW

Left-field PBW bases for the finite Ore tower #

This is the noncentral left-module layer. Scalars act through the canonical coefficient embedding at every stage; no centrality of the coefficient field inside the Ore ring is used.

source
@[reducible, inline]
abbrev AlgebraicAnalysis.OreIteratedPBW.KDerivation (K : Type u_2) [Ring K] :
Type u_2

A derivation of the field coefficient ring for an Ore stage.

Equations
Instances For
    source
    def AlgebraicAnalysis.OreIteratedPBW.towerCoefficient {K : Type u_1} [Field K] (Ds : List (KDerivation K)) (hDs : OreIteratedTower.PairwiseCommutes Ds) :
    K →+* OreIteratedTower.OreTower Ds hDs

    The coefficient embedding into a finite iterated Ore tower.

    Equations
    Instances For
      source
      @[instance_reducible]
      noncomputable instance AlgebraicAnalysis.OreIteratedPBW.towerKModule {K : Type u_1} [Field K] (Ds : List (KDerivation K)) (hDs : OreIteratedTower.PairwiseCommutes Ds) :
      Module K (OreIteratedTower.OreTower Ds hDs)
      Equations
      source
      def AlgebraicAnalysis.OreIteratedPBW.exponentIndex {K : Type u_1} [Field K] :
      List (KDerivation K) → Type

      The nested natural-number index type for tower monomials.

      Equations
      Instances For
        source
        @[instance_reducible]
        noncomputable instance AlgebraicAnalysis.OreIteratedPBW.polynomialKSMul {K : Type u_1} [Field K] (R : Type u_2) [Semiring R] [Module K R] :
        SMul K (Polynomial R)
        Equations
        source
        @[instance_reducible]
        noncomputable instance AlgebraicAnalysis.OreIteratedPBW.polynomialKModule {K : Type u_1} [Field K] (R : Type u_2) [Semiring R] [Module K R] :
        Module K (Polynomial R)
        Equations
        source
        theorem AlgebraicAnalysis.OreIteratedPBW.polynomial_smul_eq_C_mul {K : Type u_1} [Field K] {R : Type u_2} [Ring R] [Module K R] (φ : K →+* R) (hφ : ∀ (c : K) (r : R), c • r = φ c * r) (c : K) (p : Polynomial R) :
        c • p = Polynomial.C (φ c) * p
        source
        noncomputable def AlgebraicAnalysis.OreIteratedPBW.polynomialToFinsuppLinearEquiv {K : Type u_1} [Field K] {R : Type u_2} [Ring R] [Module K R] :
        Polynomial R ≃ₗ[K] ℕ →₀ R

        The coefficient-wise additive coordinates of a polynomial.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def AlgebraicAnalysis.OreIteratedPBW.polynomialBasis {K : Type u_1} [Field K] {ι : Type u_3} (R : Type u_2) [Ring R] [Module K R] (b : Module.Basis ι K R) :
          Module.Basis (ℕ × ι) K (Polynomial R)

          Lift a coefficient basis to the standard polynomial basis.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def AlgebraicAnalysis.OreIteratedPBW.normalFormLinearEquivK {K : Type u_1} [Field K] {R : Type u_2} [Ring R] (D : OreDivisionDerivation R) (φ : K →+* R) (ψ : K →+* ↥(OreAssociativity.NormalOre D)) (hψ : ψ = (OreAssociativity.normalCoefficient D).comp φ) [Module K R] [Module K ↥(OreAssociativity.NormalOre D)] (hφ : ∀ (c : K) (r : R), c • r = φ c * r) (hsmul : ∀ (c : K) (z : ↥(OreAssociativity.NormalOre D)), c • z = ψ c * z) :
            Polynomial R ≃ₗ[K] ↥(OreAssociativity.NormalOre D)

            The tower normal form as a linear equivalence over the coefficient field.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def AlgebraicAnalysis.OreIteratedPBW.towerPBWBasis {K : Type u_1} [Field K] (Ds : List (KDerivation K)) (hDs : OreIteratedTower.PairwiseCommutes Ds) :
              Module.Basis (exponentIndex Ds) K (OreIteratedTower.OreTower Ds hDs)

              The PBW basis indexed by nested exponent tuples.

              Equations
              Instances For