Finite right quotients over noncommutative Ore coefficients

Monic right division leaves coefficient-left remainders. A signed reverse normal-ordering identity rewrites them in a finite right-coefficient window. The natural scalar ring is therefore Bᵐᵒᵖ, not B; this removes the commutativity restriction from the older finite-quotient consumer.

The final section instantiates the construction on the outer momentum layer of the iterated Weyl tower and uses the literal generators d and x^N d.

instance AlgebraicAnalysis.OreRightQuotient.normalOreNontrivial {B : Type u_1} [Ring B] [Nontrivial B] (D : OreDivisionDerivation B) : Nontrivial ↥(OreAssociativity.NormalOre D)

theorem AlgebraicAnalysis.OreRightQuotient.normalCoefficient_injective {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) : Function.Injective ⇑(OreAssociativity.normalCoefficient D)

@[instance_reducible]

noncomputable instance AlgebraicAnalysis.OreRightQuotient.normalOreOpSMul {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) : SMul Bᵐᵒᵖ ↥(OreAssociativity.NormalOre D)

Equations

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

@[instance_reducible]

noncomputable instance AlgebraicAnalysis.OreRightQuotient.normalOreOpModule {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) : Module Bᵐᵒᵖ ↥(OreAssociativity.NormalOre D)

Equations

• AlgebraicAnalysis.OreRightQuotient.normalOreOpModule D = Module.ofMinimalAxioms ⋯ ⋯ ⋯ ⋯

@[simp]

theorem AlgebraicAnalysis.OreRightQuotient.normalOre_op_smul_def {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (b : Bᵐᵒᵖ) (a : ↥(OreAssociativity.NormalOre D)) : b • a = a * (OreAssociativity.normalCoefficient D) (MulOpposite.unop b)

@[simp]

theorem AlgebraicAnalysis.OreRightQuotient.normalForm_X_pow_coe {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (n : ℕ) : ↑(OreAssociativity.normalForm D (Polynomial.X ^ n)) = OreAssociativity.leftOreShift D ^ n

theorem AlgebraicAnalysis.OreRightQuotient.normalForm_monomial_reverse {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (b : B) (n : ℕ) : OreAssociativity.normalForm D ((Polynomial.monomial n) b) = ∑ ij ∈ Finset.antidiagonal n, n.choose ij.1 • ((-1) ^ ij.1 * MulOpposite.op (D.toFun^[ij.1] b) • OreAssociativity.normalForm D (Polynomial.X ^ ij.2))

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

The finite right-coefficient window of order less than n.

Equations

• AlgebraicAnalysis.OreRightQuotient.rightCoefficientWindow D n = Submodule.span Bᵐᵒᵖ (Set.range fun (j : Fin n) => AlgebraicAnalysis.OreAssociativity.normalForm D (Polynomial.X ^ ↑j))

theorem AlgebraicAnalysis.OreRightQuotient.normalForm_monomial_mem_rightCoefficientWindow {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (b : B) {j n : ℕ} (hj : j < n) : OreAssociativity.normalForm D ((Polynomial.monomial j) b) ∈ rightCoefficientWindow D n

theorem AlgebraicAnalysis.OreRightQuotient.normalForm_mem_rightCoefficientWindow_of_degree_lt {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (p : Polynomial B) (n : ℕ) (hp : p = 0 ∨ p.natDegree < n) : OreAssociativity.normalForm D p ∈ rightCoefficientWindow D n

def AlgebraicAnalysis.OreRightQuotient.rightIdealAsCoeffSubmodule {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (I : Submodule (↥(OreAssociativity.NormalOre D))ᵐᵒᵖ ↥(OreAssociativity.NormalOre D)) : Submodule Bᵐᵒᵖ ↥(OreAssociativity.NormalOre D)

A right ideal viewed as a coefficient-opposite submodule.

Equations

• AlgebraicAnalysis.OreRightQuotient.rightIdealAsCoeffSubmodule D I = { carrier := ↑I, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

noncomputable def AlgebraicAnalysis.OreRightQuotient.twoGeneratorRightIdeal {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (H J : Polynomial B) : Submodule (↥(OreAssociativity.NormalOre D))ᵐᵒᵖ ↥(OreAssociativity.NormalOre D)

The right ideal generated by two normal forms.

Equations

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

noncomputable def AlgebraicAnalysis.OreRightQuotient.twoGeneratorCoeffSubmodule {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (H J : Polynomial B) : Submodule Bᵐᵒᵖ ↥(OreAssociativity.NormalOre D)

The coefficient-opposite submodule underlying a two-generator ideal.

Equations

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

@[reducible, inline]

abbrev AlgebraicAnalysis.OreRightQuotient.TwoGeneratorQuotient {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (H J : Polynomial B) : Type u_1

The corresponding quotient as a coefficient-opposite module.

Equations

• AlgebraicAnalysis.OreRightQuotient.TwoGeneratorQuotient D H J = (↥(AlgebraicAnalysis.OreAssociativity.NormalOre D) ⧸ AlgebraicAnalysis.OreRightQuotient.twoGeneratorCoeffSubmodule D H J)

theorem AlgebraicAnalysis.OreRightQuotient.normalForm_H_mem_twoGeneratorRightIdeal {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (H J : Polynomial B) : OreAssociativity.normalForm D H ∈ twoGeneratorRightIdeal D H J

theorem AlgebraicAnalysis.OreRightQuotient.normalForm_rightMul_H_mem_twoGeneratorCoeffSubmodule {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (H J q : Polynomial B) : OreAssociativity.normalForm D (OreDivision.rightMul D H q) ∈ twoGeneratorCoeffSubmodule D H J

theorem AlgebraicAnalysis.OreRightQuotient.rightCoefficientWindow_quotient_surjective {B : Type u_1} [Ring B] [Nontrivial B] (D : OreDivisionDerivation B) (H J : Polynomial B) (hH : H.Monic) : Function.Surjective ⇑((twoGeneratorCoeffSubmodule D H J).mkQ ∘ₗ (rightCoefficientWindow D H.natDegree).subtype)

theorem AlgebraicAnalysis.OreRightQuotient.twoGeneratorQuotient_finite {B : Type u_1} [Ring B] [Nontrivial B] (D : OreDivisionDerivation B) (H J : Polynomial B) (hH : H.Monic) : Module.Finite Bᵐᵒᵖ (TwoGeneratorQuotient D H J)