Principal right ideals in a derivation Ore normal form

This module isolates the generic minimal-degree and right-principal-ideal arguments for a derivation Ore extension over a division ring. The coefficient ring may be noncommutative. The right-sided orientation is explicit: division has the divisor on the left and the quotient on the right.

No simplicity, localization, or left-PID statement is asserted here.

theorem AlgebraicAnalysis.OrePrincipalRightIdeal.rightMul_C_left {B : Type u_1} [DivisionRing B] (D : OreDivisionDerivation B) (c : B) (p : Polynomial B) : OreDivision.rightMul D (Polynomial.C c) p = Polynomial.C c * p

theorem AlgebraicAnalysis.OrePrincipalRightIdeal.rightMul_coeff_C_top {B : Type u_1} [DivisionRing B] (D : OreDivisionDerivation B) (p : Polynomial B) (b : B) (hp : p ≠ 0) : (OreDivision.rightMul D p (Polynomial.C b)).coeff p.natDegree = p.leadingCoeff * b

theorem AlgebraicAnalysis.OrePrincipalRightIdeal.degree_lt_of_degree_le_of_coeff_zero {B : Type u_1} [DivisionRing B] (p : Polynomial B) (n : ℕ) (hdeg : p.degree ≤ ↑n) (hcoef : p.coeff n = 0) : p.degree < ↑n

theorem AlgebraicAnalysis.OrePrincipalRightIdeal.minimal_monic_member_commutes_coefficients {B : Type u_1} [DivisionRing B] (D : OreDivisionDerivation B) (I : TwoSidedIdeal ↥(OreAssociativity.NormalOre D)) (p : Polynomial B) (hp : p.Monic) (hpI : OreAssociativity.normalForm D p ∈ I) (hmin : ∀ (q : Polynomial B), q ≠ 0 → OreAssociativity.normalForm D q ∈ I → p.natDegree ≤ q.natDegree) (b : B) : OreDivision.rightMul D p (Polynomial.C b) = OreDivision.rightMul D (Polynomial.C b) p

A monic minimum-degree member of a two-sided ideal commutes with every coefficient. This is a minimal-degree reduction, not a simplicity theorem.

theorem AlgebraicAnalysis.OrePrincipalRightIdeal.exists_monic_minimal_member {B : Type u_1} [DivisionRing B] (D : OreDivisionDerivation B) (I : TwoSidedIdeal ↥(OreAssociativity.NormalOre D)) (hI : ∃ z ∈ I, z ≠ 0) : ∃ (p : Polynomial B), p.Monic ∧ OreAssociativity.normalForm D p ∈ I ∧ ∀ (q : Polynomial B), q ≠ 0 → OreAssociativity.normalForm D q ∈ I → p.natDegree ≤ q.natDegree

Every nonzero two-sided ideal has a monic member of minimum normal-form degree. The leading coefficient is normalized within the ideal.

The remaining declarations are the right-sided Euclidean/PID stage for a normal-form differential Ore extension. They use the same leading-term argument and make no claim about left ideals.

noncomputable def AlgebraicAnalysis.OrePrincipalRightIdeal.normalOrePrincipalRightIdeal {B : Type u_1} [DivisionRing B] (D : OreDivisionDerivation B) (p : Polynomial B) : Submodule (↥(OreAssociativity.NormalOre D))ᵐᵒᵖ ↥(OreAssociativity.NormalOre D)

The right ideal generated by a normal-form polynomial.

Equations

• AlgebraicAnalysis.OrePrincipalRightIdeal.normalOrePrincipalRightIdeal D p = (↥(AlgebraicAnalysis.OreAssociativity.NormalOre D))ᵐᵒᵖ ∙ AlgebraicAnalysis.OreAssociativity.normalForm D p

noncomputable def AlgebraicAnalysis.OrePrincipalRightIdeal.normalOrePrincipalRightIdealElement {B : Type u_1} [DivisionRing B] (D : OreDivisionDerivation B) (a : ↥(OreAssociativity.NormalOre D)) : Submodule (↥(OreAssociativity.NormalOre D))ᵐᵒᵖ ↥(OreAssociativity.NormalOre D)

The right ideal generated by an arbitrary element of NormalOre D.

Equations

• AlgebraicAnalysis.OrePrincipalRightIdeal.normalOrePrincipalRightIdealElement D a = (↥(AlgebraicAnalysis.OreAssociativity.NormalOre D))ᵐᵒᵖ ∙ a

theorem AlgebraicAnalysis.OrePrincipalRightIdeal.normalOre_right_division {B : Type u_1} [DivisionRing B] (D : OreDivisionDerivation B) (d : Polynomial B) (hd : d.Monic) (a : ↥(OreAssociativity.NormalOre D)) : ∃ (q : Polynomial B) (r : Polynomial B), a = OreAssociativity.normalForm D (OreDivision.rightMul D d q) + OreAssociativity.normalForm D r ∧ (r = 0 ∨ r.natDegree < d.natDegree)

Right Euclidean division transported from polynomial normal form.

theorem AlgebraicAnalysis.OrePrincipalRightIdeal.rightMul_C_degree_eq {B : Type u_1} [DivisionRing B] (D : OreDivisionDerivation B) (p : Polynomial B) (c : B) (hp : p ≠ 0) (hc : c ≠ 0) : (OreDivision.rightMul D p (Polynomial.C c)).degree = p.degree

theorem AlgebraicAnalysis.OrePrincipalRightIdeal.exists_monic_minimal_right_member {B : Type u_1} [DivisionRing B] (D : OreDivisionDerivation B) (I : Submodule (↥(OreAssociativity.NormalOre D))ᵐᵒᵖ ↥(OreAssociativity.NormalOre D)) (hI : ∃ z ∈ I, z ≠ 0) : ∃ (p : Polynomial B), p.Monic ∧ OreAssociativity.normalForm D p ∈ I ∧ ∀ (q : Polynomial B), q ≠ 0 → OreAssociativity.normalForm D q ∈ I → p.natDegree ≤ q.natDegree

A nonzero right submodule has a monic member of minimum normal-form degree. Normalization uses right multiplication by the inverse coefficient.

theorem AlgebraicAnalysis.OrePrincipalRightIdeal.rightIdeal_eq_principal_of_nonzero {B : Type u_1} [DivisionRing B] (D : OreDivisionDerivation B) (I : Submodule (↥(OreAssociativity.NormalOre D))ᵐᵒᵖ ↥(OreAssociativity.NormalOre D)) (hI : ∃ z ∈ I, z ≠ 0) : ∃ (p : Polynomial B), p.Monic ∧ I = normalOrePrincipalRightIdeal D p

Every nonzero right ideal is generated by one monic normal-form element. The ideal equality is on the right: I = p (NormalOre D).

theorem AlgebraicAnalysis.OrePrincipalRightIdeal.rightIdeal_isPrincipal {B : Type u_1} [DivisionRing B] (D : OreDivisionDerivation B) (I : Submodule (↥(OreAssociativity.NormalOre D))ᵐᵒᵖ ↥(OreAssociativity.NormalOre D)) : ∃ (a : ↥(OreAssociativity.NormalOre D)), I = normalOrePrincipalRightIdealElement D a

Every right ideal of NormalOre D is principal, including the zero ideal. This is a one-sided PID statement; no left-PID claim is made.