Restriction to a nonzero constant homogenizing coordinate. Proper affine sections follow from homogeneous nonmultiples also on x₀=h, not just x₀=1.

noncomputable def CCDN.firstCoordinateScaleHom (R : Type u_1) [CommRing R] {n : ℕ} (h : R) : MvPolynomial (Fin (n + 1)) R →ₐ[R] MvPolynomial (Fin (n + 1)) R

The R-algebra endomorphism of MvPolynomial (Fin (n + 1)) R that substitutes C h * X 0 for the first variable and fixes the other variables.

Equations

• CCDN.firstCoordinateScaleHom R h = MvPolynomial.aeval (Fin.cons (MvPolynomial.C h * MvPolynomial.X 0) fun (j : Fin n) => MvPolynomial.X j.succ)

theorem CCDN.firstCoordinateScaleHom_comp {R : Type u_1} [CommRing R] {n : ℕ} (h k : R) : (firstCoordinateScaleHom R h).comp (firstCoordinateScaleHom R k) = firstCoordinateScaleHom R (k * h)

Composing the scalings of the first variable by h and by k gives the scaling by k * h.

@[simp]

theorem CCDN.firstCoordinateScaleHom_one (R : Type u_1) [CommRing R] (n : ℕ) : firstCoordinateScaleHom R 1 = AlgHom.id R (MvPolynomial (Fin (n + 1)) R)

Scaling the first variable by 1 is the identity.

noncomputable def CCDN.firstCoordinateScale (K : Type u_1) [Field K] {n : ℕ} (h : K) (hh : h ≠ 0) : MvPolynomial (Fin (n + 1)) K ≃ₐ[K] MvPolynomial (Fin (n + 1)) K

For nonzero h in a field K, the K-algebra automorphism of MvPolynomial (Fin (n + 1)) K substituting C h * X 0 for the first variable; its inverse scales by h⁻¹.

Equations

• CCDN.firstCoordinateScale K h hh = AlgEquiv.ofAlgHom (CCDN.firstCoordinateScaleHom K h) (CCDN.firstCoordinateScaleHom K h⁻¹) ⋯ ⋯

theorem CCDN.firstCoordinateScaleHom_homogeneous {R : Type u_1} [CommRing R] {n d : ℕ} (h : R) {f : MvPolynomial (Fin (n + 1)) R} (hf : f.IsHomogeneous d) : ((firstCoordinateScaleHom R h) f).IsHomogeneous d

Scaling the first variable preserves homogeneity of degree d.

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

Restriction of a polynomial in n + 1 variables to the slice x₀ = h: the ring homomorphism sending X 0 to C h and X i.succ to X i.

Equations

• CCDN.homogeneousSlice n h = MvPolynomial.eval₂Hom MvPolynomial.C (Fin.cons (MvPolynomial.C h) MvPolynomial.X)

theorem CCDN.homogeneousSlice_eq_chart_scale {R : Type u_1} [CommRing R] {n : ℕ} (h : R) (f : MvPolynomial (Fin (n + 1)) R) : (homogeneousSlice n h) f = (affineChart n) ((firstCoordinateScaleHom R h) f)

The restriction of f to the slice x₀ = h is the affine chart x₀ = 1 of f with its first variable scaled by h.

theorem CCDN.homogeneousSlice_eval {R : Type u_1} [CommRing R] {n : ℕ} (h : R) (f : MvPolynomial (Fin (n + 1)) R) (x : Fin n → R) : (MvPolynomial.eval x) ((homogeneousSlice n h) f) = (MvPolynomial.eval (Fin.cons h x)) f

Evaluating the restriction of f to the slice x₀ = h at x is evaluating f at the point Fin.cons h x.

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

The restriction of a homogeneous polynomial of degree d to the slice x₀ = h has total degree at most d.

theorem CCDN.homogeneousSlice_monomial {R : Type u_1} [CommRing R] {n : ℕ} (h : R) (m : Fin (n + 1) →₀ ℕ) (c : R) : (homogeneousSlice n h) ((MvPolynomial.monomial m) c) = (MvPolynomial.monomial (chartExponent m)) (c * h ^ m 0)

The restriction of the monomial monomial m c to the slice x₀ = h is the monomial with exponent chartExponent m and coefficient c * h ^ m 0.

theorem CCDN.homogeneousSlice_scaledHomogenize {R : Type u_1} [CommRing R] {n d : ℕ} (h : R) (f : MvPolynomial (Fin n) R) (hf : f.totalDegree ≤ d) : (homogeneousSlice n h) (scaledHomogenize d h f) = MvPolynomial.C (h ^ d) * f

If f has total degree at most d, then restricting the scaled homogenization scaledHomogenize d h f to the slice x₀ = h gives C (h ^ d) * f.

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

Integer nonmultiples of a primitive homogeneous equation stay proper on a nonzero rational slice preserving the degree.