Restriction to x₀=1 is injective on forms of a fixed homogeneous degree. Explicit homogenization supplies its inverse on bounded-degree polynomials.

noncomputable def CCDN.affineChart {K : Type u_1} [CommRing K] (n : ℕ) : MvPolynomial (Fin (n + 1)) K →+* MvPolynomial (Fin n) K

The dehomogenization at the first coordinate: the ring homomorphism sending X 0 to 1 and X i.succ to X i, which restricts a polynomial in n + 1 variables to the affine chart x₀ = 1.

Equations

• CCDN.affineChart n = MvPolynomial.eval₂Hom MvPolynomial.C (Fin.cons 1 MvPolynomial.X)

noncomputable def CCDN.chartExponent {n : ℕ} (m : Fin (n + 1) →₀ ℕ) : Fin n →₀ ℕ

The exponent in n variables obtained from an exponent m in n + 1 variables by forgetting the exponent of the first variable.

Equations

• CCDN.chartExponent m = Finsupp.equivFunOnFinite.symm fun (i : Fin n) => m i.succ

@[simp]

theorem CCDN.chartExponent_apply {n : ℕ} (m : Fin (n + 1) →₀ ℕ) (i : Fin n) : (chartExponent m) i = m i.succ

The entry of chartExponent m at i is the entry of m at i.succ.

theorem CCDN.exponent_degree_split {n : ℕ} (m : Fin (n + 1) →₀ ℕ) : (m.sum fun (x : Fin (n + 1)) (e : ℕ) => e) = m 0 + (chartExponent m).sum fun (x : Fin n) (e : ℕ) => e

The degree of an exponent m in n + 1 variables is the exponent of the first variable plus the degree of chartExponent m.

theorem CCDN.affineChart_monomial {K : Type u_1} [CommRing K] {n : ℕ} (m : Fin (n + 1) →₀ ℕ) (c : K) : (affineChart n) ((MvPolynomial.monomial m) c) = (MvPolynomial.monomial (chartExponent m)) c

The affine chart of the monomial monomial m c is the monomial monomial (chartExponent m) c.

theorem CCDN.affineChart_homogeneous_coefficient {K : Type u_1} [CommRing K] {n M : ℕ} (f : MvPolynomial (Fin (n + 1)) K) (hf : f.IsHomogeneous M) (j : Fin ((n + M).choose M)) : ((affineChart n) f).coeff (chartExponent (homogeneousMonomials n M j)) = f.coeff (homogeneousMonomials n M j)

For f homogeneous of degree M, the coefficient of affineChart n f at the chart exponent of a degree-M exponent m is the coefficient of f at m.

theorem CCDN.affineChart_injective_on_homogeneous {K : Type u_1} [CommRing K] {n M : ℕ} {f g : MvPolynomial (Fin (n + 1)) K} (hf : f.IsHomogeneous M) (hg : g.IsHomogeneous M) (he : (affineChart n) f = (affineChart n) g) : f = g

Two homogeneous polynomials of the same degree with equal affine charts are equal.

theorem CCDN.affineChart_totalDegree_le {K : Type u_1} [CommRing K] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) K) : ((affineChart n) f).totalDegree ≤ f.totalDegree

Restriction to the affine chart x₀ = 1 does not increase the total degree.

noncomputable def CCDN.homogenizedExponent {n : ℕ} (M : ℕ) (m : Fin n →₀ ℕ) : Fin (n + 1) →₀ ℕ

The exponent in n + 1 variables obtained from m by prepending M - |m| as the exponent of the first variable, where |m| is the degree of m; it has degree M when |m| ≤ M.

Equations

• CCDN.homogenizedExponent M m = Finsupp.equivFunOnFinite.symm (Fin.cons (M - m.sum fun (x : Fin n) (e : ℕ) => e) ⇑m)

@[simp]

theorem CCDN.chartExponent_homogenizedExponent {n : ℕ} (M : ℕ) (m : Fin n →₀ ℕ) : chartExponent (homogenizedExponent M m) = m

Forgetting the first entry of homogenizedExponent M m recovers m.

noncomputable def CCDN.scaledHomogenize {R : Type u_1} [CommRing R] {n : ℕ} (d : ℕ) (h : R) (f : MvPolynomial (Fin n) R) : MvPolynomial (Fin (n + 1)) R

Scaled homogenization in degree d: the monomial x^m becomes h ^ |m| * x₀ ^ (d - |m|) * x^m. With h = 1 this is the usual homogenization, which is a section of affineChart (see affineChart_scaledHomogenize_one).

Equations

• CCDN.scaledHomogenize d h f = ∑ m ∈ f.support, (MvPolynomial.monomial (CCDN.homogenizedExponent d m)) ((h ^ m.sum fun (x : Fin n) (e : ℕ) => e) * f.coeff m)

theorem CCDN.scaledHomogenize_coefficient {R : Type u_1} [CommRing R] {n : ℕ} (d : ℕ) (h : R) (f : MvPolynomial (Fin n) R) (m : Fin n →₀ ℕ) : (scaledHomogenize d h f).coeff (homogenizedExponent d m) = (h ^ m.sum fun (x : Fin n) (e : ℕ) => e) * f.coeff m

The coefficient of scaledHomogenize d h f at homogenizedExponent d m is h ^ |m| * f.coeff m, where |m| is the degree of m.

theorem CCDN.scaledHomogenize_homogeneous {R : Type u_1} [CommRing R] {n d : ℕ} (h : R) (f : MvPolynomial (Fin n) R) (hf : f.totalDegree ≤ d) : (scaledHomogenize d h f).IsHomogeneous d

If f has total degree at most d, then its scaled homogenization in degree d is homogeneous of degree d.

theorem CCDN.affineChart_scaledHomogenize_one {R : Type u_1} [CommRing R] {n : ℕ} (d : ℕ) (f : MvPolynomial (Fin n) R) : (affineChart n) (scaledHomogenize d 1 f) = f

Homogenization in degree d, that is scaled homogenization with h = 1, is a right inverse of the affine chart x₀ = 1.

theorem CCDN.affineChart_map {K : Type u_1} {L : Type u_2} [CommRing K] [CommRing L] {n : ℕ} (φ : K →+* L) (f : MvPolynomial (Fin (n + 1)) K) : (affineChart n) ((MvPolynomial.map φ) f) = (MvPolynomial.map φ) ((affineChart n) f)

The affine chart x₀ = 1 commutes with mapping the coefficients along a ring homomorphism φ.

theorem CCDN.affineChart_eval {K : Type u_1} [CommRing K] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) K) (x : Fin n → K) : (MvPolynomial.eval x) ((affineChart n) f) = (MvPolynomial.eval (Fin.cons 1 x)) f

Evaluating the affine chart of f at x is evaluating f at the point Fin.cons 1 x.

theorem CCDN.eval₂_affineChart {K : Type u_1} {R : Type u_2} [CommRing K] [CommRing R] {n : ℕ} (φ : K →+* R) (a : Fin n → R) (f : MvPolynomial (Fin (n + 1)) K) : MvPolynomial.eval₂ φ a ((affineChart n) f) = MvPolynomial.eval₂ φ (Fin.cons 1 a) f

Evaluating the affine chart of f at a through φ is evaluating f at Fin.cons 1 a through φ.

theorem CCDN.homogeneous_dvd_of_affineChart_dvd {K : Type u_1} [CommRing K] [IsDomain K] {n d M : ℕ} {f g : MvPolynomial (Fin (n + 1)) K} (hf : f.IsHomogeneous d) (hf0 : f ≠ 0) (hg : g.IsHomogeneous M) (hdchart : ((affineChart n) f).totalDegree = d) (hdiv : (affineChart n) f ∣ (affineChart n) g) : f ∣ g

Divisibility of affine charts lifts to homogeneous divisibility when the first equation retains its degree on the chart.

theorem CCDN.rational_affineChart_not_dvd {n d M : ℕ} {f g : MvPolynomial (Fin (n + 1)) ℤ} (hf : f.IsHomogeneous d) (hf0 : f ≠ 0) (hg : g.IsHomogeneous M) (hprim : PrimitiveIntegerPolynomial f) (hdchart : ((affineChart n) f).totalDegree = d) (hnd : ¬f ∣ g) : ¬(MvPolynomial.map (Int.castRingHom ℚ)) ((affineChart n) f) ∣ (MvPolynomial.map (Int.castRingHom ℚ)) ((affineChart n) g)

Let f be a primitive integer homogeneous polynomial of degree d whose affine chart x₀ = 1 still has degree d. If f does not divide the homogeneous polynomial g, then over ℚ the affine chart of f does not divide the affine chart of g.