Right-coefficient PBW data for one derivation-Ore stage

The checked Ore interface gives the opposite-ring right action and the triangular coefficient identities. We prove directly that the candidate monomials form a genuine right basis; the proof uses finite-support maximal degree induction, so no freeness or flatness assumption is introduced.

noncomputable def AlgebraicAnalysis.OreRightPBW.rightPBWMonomial {B : Type u} [Ring B] (D : OreDivisionDerivation B) (n : ℕ) : ↥(OreAssociativity.NormalOre D)

The candidate right-coefficient PBW monomial of order n.

Equations

• AlgebraicAnalysis.OreRightPBW.rightPBWMonomial D n = AlgebraicAnalysis.OreAssociativity.normalForm D (Polynomial.X ^ n)

noncomputable def AlgebraicAnalysis.OreRightPBW.rightPBWCombination {B : Type u} [Ring B] (D : OreDivisionDerivation B) : (ℕ →₀ Bᵐᵒᵖ) →ₗ[Bᵐᵒᵖ] ↥(OreAssociativity.NormalOre D)

The finitely supported right-coefficient combination of PBW monomials.

Equations

• AlgebraicAnalysis.OreRightPBW.rightPBWCombination D = Finsupp.linearCombination Bᵐᵒᵖ (AlgebraicAnalysis.OreRightPBW.rightPBWMonomial D)

theorem AlgebraicAnalysis.OreRightPBW.rightPBWCombination_single {B : Type u} [Ring B] (D : OreDivisionDerivation B) (n : ℕ) (b : Bᵐᵒᵖ) : (rightPBWCombination D) (Finsupp.single n b) = b • rightPBWMonomial D n

theorem AlgebraicAnalysis.OreRightPBW.rightPBWCombination_term_as_normalForm {B : Type u} [Ring B] (D : OreDivisionDerivation B) (n : ℕ) (b : Bᵐᵒᵖ) : b • rightPBWMonomial D n = OreAssociativity.normalForm D (OreDivision.rightMul D (Polynomial.X ^ n) (Polynomial.C (MulOpposite.unop b)))

theorem AlgebraicAnalysis.OreRightPBW.rightPBWCombination_finsupp_as_normalForm {B : Type u} [Ring B] (D : OreDivisionDerivation B) (c : ℕ →₀ Bᵐᵒᵖ) : (rightPBWCombination D) c = OreAssociativity.normalForm D (c.sum fun (n : ℕ) (b : Bᵐᵒᵖ) => OreDivision.rightMul D (Polynomial.X ^ n) (Polynomial.C (MulOpposite.unop b)))

theorem AlgebraicAnalysis.OreRightPBW.rightPBWCombination_eq_zero {B : Type u} [Ring B] [Nontrivial B] (D : OreDivisionDerivation B) (c : ℕ →₀ Bᵐᵒᵖ) (hc : (rightPBWCombination D) c = 0) : c = 0

theorem AlgebraicAnalysis.OreRightPBW.rightPBWCombination_injective {B : Type u} [Ring B] [Nontrivial B] (D : OreDivisionDerivation B) : Function.Injective ⇑(rightPBWCombination D)

theorem AlgebraicAnalysis.OreRightPBW.rightPBWMonomial_mem_span {B : Type u} [Ring B] (D : OreDivisionDerivation B) (b : B) (n : ℕ) : OreAssociativity.normalForm D ((Polynomial.monomial n) b) ∈ Submodule.span Bᵐᵒᵖ (Set.range (rightPBWMonomial D))

theorem AlgebraicAnalysis.OreRightPBW.rightPBW_span_eq_top {B : Type u} [Ring B] (D : OreDivisionDerivation B) : Submodule.span Bᵐᵒᵖ (Set.range (rightPBWMonomial D)) = ⊤

theorem AlgebraicAnalysis.OreRightPBW.rightOrePBW_linearIndependent {B : Type u} [Ring B] [Nontrivial B] (D : OreDivisionDerivation B) : LinearIndependent Bᵐᵒᵖ (rightPBWMonomial D)

noncomputable def AlgebraicAnalysis.OreRightPBW.rightOrePBWBasis {B : Type u} [Ring B] [Nontrivial B] (D : OreDivisionDerivation B) : Module.Basis ℕ Bᵐᵒᵖ ↥(OreAssociativity.NormalOre D)

The right PBW basis of a one-stage derivation-Ore extension.

Equations

• AlgebraicAnalysis.OreRightPBW.rightOrePBWBasis D = Module.Basis.mk ⋯ ⋯

@[simp]

theorem AlgebraicAnalysis.OreRightPBW.rightOrePBWBasis_apply {B : Type u} [Ring B] [Nontrivial B] (D : OreDivisionDerivation B) (n : ℕ) : (rightOrePBWBasis D) n = rightPBWMonomial D n

theorem AlgebraicAnalysis.OreRightPBW.rightOrePBWBasis_repr_symm_single {B : Type u} [Ring B] [Nontrivial B] (D : OreDivisionDerivation B) (n : ℕ) (b : Bᵐᵒᵖ) : (rightOrePBWBasis D).repr.symm (Finsupp.single n b) = b • rightPBWMonomial D n

theorem AlgebraicAnalysis.OreRightPBW.rightPBWMonomial_zero {B : Type u} [Ring B] (D : OreDivisionDerivation B) : rightPBWMonomial D 0 = 1

@[simp]

theorem AlgebraicAnalysis.OreRightPBW.rightPBWMonomial_op_smul {B : Type u} [Ring B] (D : OreDivisionDerivation B) (b : Bᵐᵒᵖ) (n : ℕ) : b • rightPBWMonomial D n = OreAssociativity.normalForm D (Polynomial.X ^ n) * (OreAssociativity.normalCoefficient D) (MulOpposite.unop b)

noncomputable def AlgebraicAnalysis.OreRightPBW.rightPBWWindow {B : Type u} [Ring B] (D : OreDivisionDerivation B) (n : ℕ) : Submodule Bᵐᵒᵖ ↥(OreAssociativity.NormalOre D)

The finite window generated by the candidate right PBW monomials.

Equations

• AlgebraicAnalysis.OreRightPBW.rightPBWWindow D n = Submodule.span Bᵐᵒᵖ (Set.range fun (j : Fin n) => AlgebraicAnalysis.OreRightPBW.rightPBWMonomial D ↑j)

theorem AlgebraicAnalysis.OreRightPBW.normalForm_mem_rightPBWWindow_of_degree_lt {B : Type u} [Ring B] (D : OreDivisionDerivation B) (p : Polynomial B) (n : ℕ) (hp : p = 0 ∨ p.natDegree < n) : OreAssociativity.normalForm D p ∈ rightPBWWindow D n

theorem AlgebraicAnalysis.OreRightPBW.rightPBWWindow_finite {B : Type u} [Ring B] (D : OreDivisionDerivation B) (n : ℕ) : Module.Finite Bᵐᵒᵖ ↥(rightPBWWindow D n)

@[simp]

theorem AlgebraicAnalysis.OreRightPBW.rightPBWMonomial_apply {B : Type u} [Ring B] (D : OreDivisionDerivation B) (n : ℕ) : rightPBWMonomial D n = OreAssociativity.normalForm D (Polynomial.X ^ n)

theorem AlgebraicAnalysis.OreRightPBW.rightMul_Xpow_top_coefficient {B : Type u} [Ring B] [Nontrivial B] (D : OreDivisionDerivation B) (p : Polynomial B) (n j : ℕ) (hp : p.degree ≤ ↑n) : (OreDivision.rightMul D p (Polynomial.X ^ j)).coeff (n + j) = p.coeff n

Right multiplication by a PBW monomial has the expected top coefficient. This is the triangular input for an eventual basis proof.

theorem AlgebraicAnalysis.OreRightPBW.rightMul_Xpow_degree_le {B : Type u} [Ring B] [Nontrivial B] (D : OreDivisionDerivation B) (p : Polynomial B) (j : ℕ) : (OreDivision.rightMul D p (Polynomial.X ^ j)).degree ≤ ↑p.natDegree + ↑j

Monic principal quotients

theorem AlgebraicAnalysis.OreRightPBW.exists_lowDegreePolynomial_eq_of_mem_rightPBWWindow {B : Type u} [Ring B] [Nontrivial B] (D : OreDivisionDerivation B) (N : ℕ) {z : ↥(OreAssociativity.NormalOre D)} (hz : z ∈ rightPBWWindow D N) : ∃ (r : Polynomial B), (r = 0 ∨ r.natDegree < N) ∧ OreAssociativity.normalForm D r = z

A vector in the first N right-PBW slots has a coefficient-left normal form of degree strictly less than N. This is the converse, at the level needed for division, of normalForm_mem_rightPBWWindow_of_degree_lt.

theorem AlgebraicAnalysis.OreRightPBW.monicPrincipalRightIdeal_isCompl_rightPBWWindow {B : Type u} [Ring B] [Nontrivial B] (D : OreDivisionDerivation B) (H : Polynomial B) (hH : H.Monic) : IsCompl (OreRightQuotient.twoGeneratorCoeffSubmodule D H 0) (rightPBWWindow D H.natDegree)

Monic right multiples and the finite right-PBW remainder window are exact complements. Equivalently, monic right division is both exhaustive and unique as a decomposition over the opposite coefficient ring.

noncomputable def AlgebraicAnalysis.OreRightPBW.rightPBWWindowBasis {B : Type u} [Ring B] [Nontrivial B] (D : OreDivisionDerivation B) (N : ℕ) : Module.Basis (Fin N) Bᵐᵒᵖ ↥(rightPBWWindow D N)

The basis of the finite right-PBW remainder window.

Equations

• AlgebraicAnalysis.OreRightPBW.rightPBWWindowBasis D N = Module.Basis.span ⋯

noncomputable def AlgebraicAnalysis.OreRightPBW.monicPrincipalRightQuotientBasis {B : Type u} [Ring B] [Nontrivial B] (D : OreDivisionDerivation B) (H : Polynomial B) (hH : H.Monic) : Module.Basis (Fin H.natDegree) Bᵐᵒᵖ (OreRightQuotient.TwoGeneratorQuotient D H 0)

A monic principal right quotient of a derivation-Ore extension is free of rank H.natDegree over the opposite coefficient ring, with basis represented by 1, X, …, X^(H.natDegree-1). The 0 second generator is only a literal encoding of the principal right ideal inside the existing quotient API.

Equations

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

@[simp]

theorem AlgebraicAnalysis.OreRightPBW.monicPrincipalRightQuotientBasis_apply {B : Type u} [Ring B] [Nontrivial B] (D : OreDivisionDerivation B) (H : Polynomial B) (hH : H.Monic) (j : Fin H.natDegree) : (monicPrincipalRightQuotientBasis D H hH) j = Submodule.Quotient.mk (OreAssociativity.normalForm D (Polynomial.X ^ ↑j))