Degrees and leading coefficients of Ore polynomials

The degree filtration of an Ore extension is preserved by multiplication. At the top degree, the skew derivation contributes nothing: the coefficient of degree m + n in a product with degree bounds m and n is coeff p m * σ^[m] (coeff q n). Consequently an Ore extension over a semiring without zero divisors has no zero divisors when its coefficient endomorphism is injective. This is the leading-term calculation used in iterated Ore presentations.

The convention natDegree 0 = 0 agrees with ordinary polynomials.

References

• P. M. Cohn, Free Rings and Their Relations, second edition, Chapter 2.

def TauCeti.OreExtension.natDegree {k : Type u_1} {R : Type u_2} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (p : OreExtension σ δ) : ℕ

The largest index of a nonzero coefficient, with value zero for the zero polynomial.

def TauCeti.OreExtension.leadingCoeff {k : Type u_1} {R : Type u_2} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (p : OreExtension σ δ) : R

The coefficient at the natural degree.

theorem TauCeti.OreExtension.natDegree_def {k : Type u_1} {R : Type u_2} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (p : OreExtension σ δ) : p.natDegree = p.toFinsupp.support.sup id

The natural degree is the supremum of the coefficient support.

theorem TauCeti.OreExtension.leadingCoeff_def {k : Type u_1} {R : Type u_2} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (p : OreExtension σ δ) : p.leadingCoeff = p.coeff p.natDegree

The leading coefficient is the coefficient at the natural degree.

@[simp]

theorem TauCeti.OreExtension.natDegree_zero {k : Type u_1} {R : Type u_2} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} : natDegree 0 = 0

theorem TauCeti.OreExtension.natDegree_le_iff {k : Type u_1} {R : Type u_2} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} {p : OreExtension σ δ} {n : ℕ} : p.natDegree ≤ n ↔ ∀ (i : ℕ), n < i → p.coeff i = 0

A degree bound is equivalent to vanishing of all higher coefficients.

theorem TauCeti.OreExtension.coeff_eq_zero_of_natDegree_lt {k : Type u_1} {R : Type u_2} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} {p : OreExtension σ δ} {n : ℕ} (h : p.natDegree < n) : p.coeff n = 0

Coefficients above the natural degree vanish.

theorem TauCeti.OreExtension.le_natDegree_of_ne_zero {k : Type u_1} {R : Type u_2} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} {p : OreExtension σ δ} {n : ℕ} (h : p.coeff n ≠ 0) : n ≤ p.natDegree

A nonzero coefficient gives a lower bound on the natural degree.

theorem TauCeti.OreExtension.natDegree_monomial_le {k : Type u_1} {R : Type u_2} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (n : ℕ) (a : R) : ((monomial n) a).natDegree ≤ n

A monomial has degree at most its exponent.

@[simp]

theorem TauCeti.OreExtension.natDegree_monomial {k : Type u_1} {R : Type u_2} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (n : ℕ) {a : R} (ha : a ≠ 0) : ((monomial n) a).natDegree = n

A monomial with nonzero coefficient has its indicated degree.

@[simp]

theorem TauCeti.OreExtension.natDegree_C {k : Type u_1} {R : Type u_2} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (a : R) : (C a).natDegree = 0

@[simp]

theorem TauCeti.OreExtension.natDegree_one {k : Type u_1} {R : Type u_2} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} : natDegree 1 = 0

@[simp]

theorem TauCeti.OreExtension.natDegree_X_pow {k : Type u_1} {R : Type u_2} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} [Nontrivial R] (n : ℕ) : (X ^ n).natDegree = n

@[simp]

theorem TauCeti.OreExtension.natDegree_X {k : Type u_1} {R : Type u_2} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} [Nontrivial R] : X.natDegree = 1

@[simp]

theorem TauCeti.OreExtension.leadingCoeff_eq_zero {k : Type u_1} {R : Type u_2} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} {p : OreExtension σ δ} : p.leadingCoeff = 0 ↔ p = 0

@[simp]

theorem TauCeti.OreExtension.leadingCoeff_zero {k : Type u_1} {R : Type u_2} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} : leadingCoeff 0 = 0

@[simp]

theorem TauCeti.OreExtension.leadingCoeff_monomial {k : Type u_1} {R : Type u_2} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (n : ℕ) (a : R) : ((monomial n) a).leadingCoeff = a

The leading coefficient of a monomial is its coefficient, including the zero monomial.

@[simp]

theorem TauCeti.OreExtension.leadingCoeff_C {k : Type u_1} {R : Type u_2} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (a : R) : (C a).leadingCoeff = a

@[simp]

theorem TauCeti.OreExtension.leadingCoeff_one {k : Type u_1} {R : Type u_2} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} : leadingCoeff 1 = 1

@[simp]

theorem TauCeti.OreExtension.leadingCoeff_X_pow {k : Type u_1} {R : Type u_2} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (n : ℕ) : (X ^ n).leadingCoeff = 1

@[simp]

theorem TauCeti.OreExtension.leadingCoeff_X {k : Type u_1} {R : Type u_2} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} : X.leadingCoeff = 1

theorem TauCeti.OreExtension.natDegree_add_le {k : Type u_1} {R : Type u_2} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (p q : OreExtension σ δ) : (p + q).natDegree ≤ max p.natDegree q.natDegree

Adding Ore polynomials cannot increase the largest of their degree bounds.

theorem TauCeti.OreExtension.natDegree_X_mul_le {k : Type u_1} {R : Type u_2} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (p : OreExtension σ δ) : (X * p).natDegree ≤ p.natDegree + 1

Left multiplication by the variable raises a degree bound by at most one.

theorem TauCeti.OreExtension.natDegree_X_pow_mul_le {k : Type u_1} {R : Type u_2} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (p : OreExtension σ δ) (m : ℕ) : (X ^ m * p).natDegree ≤ m + p.natDegree

Left multiplication by Xᵐ raises a degree bound by at most m.

theorem TauCeti.OreExtension.coeff_X_pow_mul_add {k : Type u_1} {R : Type u_2} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (p : OreExtension σ δ) (m n : ℕ) (hp : p.natDegree ≤ n) : (X ^ m * p).coeff (m + n) = (⇑σ)^[m] (p.coeff n)

At the shifted top degree only the iterated coefficient endomorphism contributes.

@[simp]

theorem TauCeti.OreExtension.coeff_X_pow_mul_C_self {k : Type u_1} {R : Type u_2} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (n : ℕ) (b : R) : (X ^ n * C b).coeff n = (⇑σ)^[n] b

The top coefficient of Xⁿ * C b is σⁿ b.

theorem TauCeti.OreExtension.natDegree_X_pow_mul_C_le {k : Type u_1} {R : Type u_2} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (n : ℕ) (b : R) : (X ^ n * C b).natDegree ≤ n

The monomial Xⁿ * C b with its coefficient on the right has degree at most n.

theorem TauCeti.OreExtension.natDegree_mul_le {k : Type u_1} {R : Type u_2} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (p q : OreExtension σ δ) : (p * q).natDegree ≤ p.natDegree + q.natDegree

Multiplication preserves the sum of the degree bounds, without injectivity assumptions.

theorem TauCeti.OreExtension.coeff_mul_add_eq_of_natDegree_le {k : Type u_1} {R : Type u_2} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} {p q : OreExtension σ δ} {m n : ℕ} (hp : p.natDegree ≤ m) (hq : q.natDegree ≤ n) : (p * q).coeff (m + n) = p.coeff m * (⇑σ)^[m] (q.coeff n)

The coefficient at the sum of two degree bounds in an Ore product.

theorem TauCeti.OreExtension.coeff_mul_degree_add_degree {k : Type u_1} {R : Type u_2} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (p q : OreExtension σ δ) : (p * q).coeff (p.natDegree + q.natDegree) = p.leadingCoeff * (⇑σ)^[p.natDegree] q.leadingCoeff

The coefficient at the sum of the natural degrees is the twisted leading product.

theorem TauCeti.OreExtension.natDegree_mul {k : Type u_1} {R : Type u_2} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} [NoZeroDivisors R] (hσ : Function.Injective ⇑σ) {p q : OreExtension σ δ} (hp : p ≠ 0) (hq : q ≠ 0) : (p * q).natDegree = p.natDegree + q.natDegree

An Ore product has additive natural degree if both factors are nonzero and the coefficient endomorphism is injective.

theorem TauCeti.OreExtension.leadingCoeff_mul {k : Type u_1} {R : Type u_2} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} [NoZeroDivisors R] (hσ : Function.Injective ⇑σ) (p q : OreExtension σ δ) : (p * q).leadingCoeff = p.leadingCoeff * (⇑σ)^[p.natDegree] q.leadingCoeff

The leading coefficient of a product over a semiring without zero divisors.

theorem TauCeti.OreExtension.noZeroDivisors {k : Type u_1} {R : Type u_2} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} [NoZeroDivisors R] (hσ : Function.Injective ⇑σ) : NoZeroDivisors (OreExtension σ δ)

An injective coefficient endomorphism preserves absence of zero divisors in an Ore extension. The skew derivation is arbitrary.

theorem TauCeti.OreExtension.isDomain {k : Type u_1} [CommSemiring k] {S : Type u_3} [Ring S] [Algebra k S] {τ : S →ₐ[k] S} {ε : SigmaDerivation τ} [IsDomain S] (hτ : Function.Injective ⇑τ) : IsDomain (OreExtension τ ε)

An Ore extension of a domain by an injective endomorphism is a domain.