The derivation-Ore right Hilbert-basis theorem

This file is a right-sided version of the leading-coefficient proof for a differential Ore extension. Coefficients are allowed to be noncommutative: right ideals of the coefficient ring are represented as submodules for the opposite scalar ring.

def AlgebraicAnalysis.OreDerivationRightHilbertBasis.DerivationOreRightHilbertBasis : Prop

The right Hilbert-basis assertion for one derivation-Ore stage.

Equations

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

@[simp]

theorem AlgebraicAnalysis.OreDerivationRightHilbertBasis.rightScalar_smul_def {B : Type u} [Ring B] (b : Bᵐᵒᵖ) (c : B) : b • c = c * MulOpposite.unop b

noncomputable def AlgebraicAnalysis.OreDerivationRightHilbertBasis.normalPolyEquiv {B : Type u} [Ring B] (D : OreDivisionDerivation B) : Polynomial B ≃+ ↥(OreAssociativity.NormalOre D)

Additive equivalence between coefficient-left polynomials and normal forms.

Equations

• AlgebraicAnalysis.OreDerivationRightHilbertBasis.normalPolyEquiv D = AlgebraicAnalysis.OreAssociativity.normalFormAddEquiv D

theorem AlgebraicAnalysis.OreDerivationRightHilbertBasis.rightMul_coeff_C_of_degree_le {B : Type u} [Ring B] (D : OreDivisionDerivation B) (p : Polynomial B) (b : B) (n : ℕ) (hp : p.degree ≤ ↑n) : (OreDivision.rightMul D p (Polynomial.C b)).coeff n = p.coeff n * b

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

The degree-at-most-n submodule of normal forms.

Equations

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

noncomputable def AlgebraicAnalysis.OreDerivationRightHilbertBasis.normalCoeffNth {B : Type u} [Ring B] (D : OreDivisionDerivation B) (n : ℕ) : ↥(normalDegreeLE D n) →ₗ[Bᵐᵒᵖ] B

The nth coefficient functional on the degree window.

Equations

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

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

The degree window cut out by a right ideal.

Equations

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

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

The leading-coefficient submodule at a fixed degree.

Equations

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

theorem AlgebraicAnalysis.OreDerivationRightHilbertBasis.mem_leadingCoeffNth {B : Type u} [Ring B] (D : OreDivisionDerivation B) (I : Submodule (↥(OreAssociativity.NormalOre D))ᵐᵒᵖ ↥(OreAssociativity.NormalOre D)) (n : ℕ) (c : B) : c ∈ leadingCoeffNth D I n ↔ ∃ (p : Polynomial B), OreAssociativity.normalForm D p ∈ I ∧ p.degree ≤ ↑n ∧ p.coeff n = c

theorem AlgebraicAnalysis.OreDerivationRightHilbertBasis.rightMul_Xpow_coeff_of_degree_le {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

theorem AlgebraicAnalysis.OreDerivationRightHilbertBasis.leadingCoeffNth_mono {B : Type u} [Ring B] [Nontrivial B] (D : OreDivisionDerivation B) (I : Submodule (↥(OreAssociativity.NormalOre D))ᵐᵒᵖ ↥(OreAssociativity.NormalOre D)) {m n : ℕ} (hmn : m ≤ n) : leadingCoeffNth D I m ≤ leadingCoeffNth D I n

noncomputable def AlgebraicAnalysis.OreDerivationRightHilbertBasis.leadingCoeffChain {B : Type u} [Ring B] [Nontrivial B] (D : OreDivisionDerivation B) (I : Submodule (↥(OreAssociativity.NormalOre D))ᵐᵒᵖ ↥(OreAssociativity.NormalOre D)) : ℕ →o Submodule Bᵐᵒᵖ B

The monotone chain of leading-coefficient submodules.

Equations

• AlgebraicAnalysis.OreDerivationRightHilbertBasis.leadingCoeffChain D I = { toFun := fun (n : ℕ) => AlgebraicAnalysis.OreDerivationRightHilbertBasis.leadingCoeffNth D I n, monotone' := ⋯ }

theorem AlgebraicAnalysis.OreDerivationRightHilbertBasis.exists_leadingCoeff_stable {B : Type u} [Ring B] [Nontrivial B] [IsNoetherianRing Bᵐᵒᵖ] (D : OreDivisionDerivation B) (I : Submodule (↥(OreAssociativity.NormalOre D))ᵐᵒᵖ ↥(OreAssociativity.NormalOre D)) : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → leadingCoeffNth D I n = leadingCoeffNth D I N

theorem AlgebraicAnalysis.OreDerivationRightHilbertBasis.normalDegreeLE_le_window {B : Type u} [Ring B] (D : OreDivisionDerivation B) (n : ℕ) : normalDegreeLE D n ≤ OreRightQuotient.rightCoefficientWindow D (n + 1)

def AlgebraicAnalysis.OreDerivationRightHilbertBasis.normalDegreeLEToWindow {B : Type u} [Ring B] (D : OreDivisionDerivation B) (n : ℕ) : ↥(normalDegreeLE D n) →ₗ[Bᵐᵒᵖ] ↥(OreRightQuotient.rightCoefficientWindow D (n + 1))

The degree window embedded in the finite coefficient window.

Equations

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

def AlgebraicAnalysis.OreDerivationRightHilbertBasis.normalDegreeIncl {B : Type u} [Ring B] (D : OreDivisionDerivation B) (n : ℕ) (J : Submodule Bᵐᵒᵖ ↥(OreAssociativity.NormalOre D)) (hJ : J ≤ normalDegreeLE D n) : ↥J →ₗ[Bᵐᵒᵖ] ↥(normalDegreeLE D n)

Inclusion of an ideal degree window into the full degree window.

Equations

• AlgebraicAnalysis.OreDerivationRightHilbertBasis.normalDegreeIncl D n J hJ = { toFun := fun (z : ↥J) => ⟨↑z, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

theorem AlgebraicAnalysis.OreDerivationRightHilbertBasis.rightIdealDegreeLE_fg {B : Type u} [Ring B] [IsNoetherianRing Bᵐᵒᵖ] (D : OreDivisionDerivation B) (I : Submodule (↥(OreAssociativity.NormalOre D))ᵐᵒᵖ ↥(OreAssociativity.NormalOre D)) (n : ℕ) : (rightIdealDegreeLE D I n).FG

theorem AlgebraicAnalysis.OreDerivationRightHilbertBasis.normalOre_rightIdeal_fg_of_op_noetherian {B : Type u} [Ring B] [Nontrivial B] [IsNoetherianRing Bᵐᵒᵖ] (D : OreDivisionDerivation B) (I : Submodule (↥(OreAssociativity.NormalOre D))ᵐᵒᵖ ↥(OreAssociativity.NormalOre D)) : I.FG

theorem AlgebraicAnalysis.OreDerivationRightHilbertBasis.normalOre_op_isNoetherian_of_nontrivial {B : Type u} [Ring B] [Nontrivial B] [IsNoetherianRing Bᵐᵒᵖ] (D : OreDivisionDerivation B) : IsNoetherianRing (↥(OreAssociativity.NormalOre D))ᵐᵒᵖ

theorem AlgebraicAnalysis.OreDerivationRightHilbertBasis.normalOre_op_isNoetherian_of_subsingleton {B : Type u} [Ring B] [Subsingleton B] (D : OreDivisionDerivation B) : IsNoetherianRing (↥(OreAssociativity.NormalOre D))ᵐᵒᵖ

theorem AlgebraicAnalysis.OreDerivationRightHilbertBasis.derivationOre_rightHilbertBasis : DerivationOreRightHilbertBasis