Division by monomials

This file extends Mathlib's MvPolynomial.divMonomial API with homogeneous degree bookkeeping and identities for moving monomial factors through a division. The statements depend only on finitely supported exponent vectors and multivariate polynomials. They include exact division by a power of one variable and cross-variable cancellation; projective localization and Čech constructions import these facts as consumers.

theorem Finsupp.degree_eq_weight_one_apply {ι : Type u} (e : ι →₀ ℕ) : degree e = (weight 1) e

Finsupp.degree is Finsupp.weight 1, pointwise.

theorem MvPolynomial.isHomogeneous_divMonomial {ι R : Type u} [CommRing R] {p : MvPolynomial ι R} {s : ι →₀ ℕ} {k : ℕ} (hp : p.IsHomogeneous (Finsupp.degree s + k)) : (p.divMonomial s).IsHomogeneous k

Dividing by a monomial drops homogeneous degree by the degree of that monomial.

theorem MvPolynomial.divMonomial_monomial_mul_add {ι R : Type u} [CommRing R] (a b : ι →₀ ℕ) (x : MvPolynomial ι R) : ((monomial a) 1 * x).divMonomial (a + b) = x.divMonomial b

Dividing off a factor already present leaves the rest of the division to do.

theorem MvPolynomial.divMonomial_monomial_mul_comm {ι R : Type u} [CommRing R] {a s : ι →₀ ℕ} (hd : ∀ (j : ι), a j = 0 ∨ s j = 0) (p : MvPolynomial ι R) : ((monomial a) 1 * p).divMonomial s = (monomial a) 1 * p.divMonomial s

A monomial factor passes through a division when the factor and divisor have disjoint support.

theorem MvPolynomial.divMonomial_pow_mul {ι R : Type u} [CommRing R] {γ γ' : ι →₀ ℕ} {i₀ : ι} {c : ℕ} (hγ : γ = Finsupp.single i₀ c + γ') (hγ' : γ' i₀ = 0) (m t : ℕ) (p : MvPolynomial ι R) : ((monomial γ) 1 ^ t * p).divMonomial (Finsupp.single i₀ ((m + t) * c)) = (monomial γ') 1 ^ t * p.divMonomial (Finsupp.single i₀ (m * c))

Raising a numerator by a power of one monomial and then dividing off one of its factors agrees with first dividing and then multiplying by the disjoint remaining factor.

Exact division by a power of one variable

theorem MvPolynomial.divMonomial_single_mem_homogeneousSubmodule (ι k : Type u) [Field k] (i : ι) (n d : ℕ) (p : MvPolynomial ι k) (hp : p ∈ homogeneousSubmodule ι k (n + d)) : p.divMonomial (Finsupp.single i n) ∈ homogeneousSubmodule ι k d

Dividing a homogeneous polynomial of degree n + d by Xᵢⁿ, when the division is exact, produces a homogeneous polynomial of degree d.

theorem MvPolynomial.X_pow_mul_divMonomial_single (ι k : Type u) [Field k] (i : ι) (n : ℕ) (p : MvPolynomial ι k) (hdiv : X i ^ n ∣ p) : X i ^ n * p.divMonomial (Finsupp.single i n) = p

Exact division by Xᵢⁿ reconstructs the original polynomial.

theorem MvPolynomial.X_pow_dvd_of_cross_mul (ι k : Type u) [Field k] {i j : ι} (hij : i ≠ j) (n m : ℕ) (p q : MvPolynomial ι k) (hcross : X j ^ m * p = X i ^ n * q) : X i ^ n ∣ p

If a fraction with denominator a power of Xᵢ also admits a denominator involving only a different variable, then its numerator is divisible by the entire power of Xᵢ.

theorem MvPolynomial.eq_zero_of_X_pow_dvd_of_isHomogeneous_of_lt (ι k : Type u) [Field k] (i : ι) (a m : ℕ) (p : MvPolynomial ι k) (hp : p ∈ homogeneousSubmodule ι k m) (hdvd : X i ^ a ∣ p) (hlt : m < a) : p = 0

A homogeneous polynomial divisible by X i ^ a but of degree below a is zero.

Every monomial of a multiple of X i ^ a carries X i to at least the power a, so its total degree is at least a. A homogeneous polynomial of degree m < a therefore has no monomials at all.

theorem MvPolynomial.num_eq_zero_of_cross_of_neg (ι k : Type u) [Field k] {i j : ι} (hij : i ≠ j) (d : ℤ) (hd : d < 0) (a b m : ℕ) (p q : MvPolynomial ι k) (hm : ↑m = ↑a + d) (hp : p ∈ homogeneousSubmodule ι k m) (hcross : X j ^ b * p = X i ^ a * q) : p = 0

A homogeneous numerator in a negative shifted degree vanishes when a cross-variable equation forces divisibility by its own denominator power.

The cross equation makes X i ^ a divide p, while m = a + d and d < 0 put the homogeneous degree of p strictly below a.