Left PBW basis for a derivation Ore extension

The normal-form Ore ring is a left module over its coefficient field even when the derivation is nonzero (and hence the coefficient field is not central). Transporting the ordinary polynomial monomial basis across the checked normal-form equivalence gives the expected basis 1, ∂, ∂², ....

The iterated tower still needs the commuting derivations to be extended over earlier stages. Nothing in this file postulates such extensions.

@[instance_reducible]

noncomputable instance AlgebraicAnalysis.OreLeftPBW.normalOreLeftModule {K : Type u_1} [Field K] (D : OreDivisionDerivation K) : Module K ↥(OreAssociativity.NormalOre D)

The coefficient field acts on an Ore extension by multiplication on the left through the canonical coefficient embedding. Centrality is neither assumed nor needed.

Equations

• AlgebraicAnalysis.OreLeftPBW.normalOreLeftModule D = Module.compHom (↥(AlgebraicAnalysis.OreAssociativity.NormalOre D)) (AlgebraicAnalysis.OreAssociativity.normalCoefficient D)

theorem AlgebraicAnalysis.OreLeftPBW.normalForm_smul_left {K : Type u_1} [Field K] (D : OreDivisionDerivation K) (c : K) (p : Polynomial K) : OreAssociativity.normalForm D (c • p) = c • OreAssociativity.normalForm D p

noncomputable def AlgebraicAnalysis.OreLeftPBW.leftNormalFormLinearEquiv {K : Type u_1} [Field K] (D : OreDivisionDerivation K) : Polynomial K ≃ₗ[K] ↥(OreAssociativity.NormalOre D)

Coefficient-left Ore normal form as a linear equivalence over the coefficient field.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicAnalysis.OreLeftPBW.leftNormalFormLinearEquiv_apply {K : Type u_1} [Field K] (D : OreDivisionDerivation K) (p : Polynomial K) : (leftNormalFormLinearEquiv D) p = OreAssociativity.normalForm D p

noncomputable def AlgebraicAnalysis.OreLeftPBW.orePBWBasis {K : Type u_1} [Field K] (D : OreDivisionDerivation K) : Module.Basis ℕ K ↥(OreAssociativity.NormalOre D)

The powers of the Ore variable form a left basis over the coefficient field.

Equations

• AlgebraicAnalysis.OreLeftPBW.orePBWBasis D = (Polynomial.basisMonomials K).map (AlgebraicAnalysis.OreLeftPBW.leftNormalFormLinearEquiv D)

@[simp]

theorem AlgebraicAnalysis.OreLeftPBW.orePBWBasis_apply {K : Type u_1} [Field K] (D : OreDivisionDerivation K) (n : ℕ) : (orePBWBasis D) n = OreAssociativity.normalVariable D ^ n

theorem AlgebraicAnalysis.OreLeftPBW.orePBW_repr_symm_single {K : Type u_1} [Field K] (D : OreDivisionDerivation K) (n : ℕ) (c : K) : (orePBWBasis D).repr.symm (Finsupp.single n c) = (OreAssociativity.normalCoefficient D) c * OreAssociativity.normalVariable D ^ n

Every element has a unique finite coefficient-left expansion in powers of the Ore variable.