Irreducibility and coefficient maps of scaled homogeneous models in arbitrary dimension, including reduction modulo primes.

theorem CCDN.scaledHomogenize_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {n : ℕ} (φ : R →+* S) (d : ℕ) (h : R) (f : MvPolynomial (Fin n) R) : (MvPolynomial.map φ) (scaledHomogenize d h f) = scaledHomogenize d (φ h) ((MvPolynomial.map φ) f)

Scaled homogenization commutes with mapping the coefficients along a ring homomorphism φ, the scaling factor h being replaced by φ h.

theorem CCDN.scaledHomogenize_irreducible {K : Type u_1} [Field K] {n : ℕ} (f : MvPolynomial (Fin n) K) (hir : Irreducible f) {h : K} (hh : h ≠ 0) : Irreducible (scaledHomogenize f.totalDegree h f)

Over a field, every nonzero scaling of an irreducible affine equation has an irreducible homogeneous model.

theorem CCDN.scaledHomogenize_integer_irreducible {n : ℕ} (f : MvPolynomial (Fin n) ℤ) (hprim : PrimitiveIntegerPolynomial f) (hir : Irreducible f) (hd : 0 < f.totalDegree) {p : ℕ} (hp : Nat.Prime p) (hp0 : ¬↑p ∣ f.coeff 0) : Irreducible (scaledHomogenize f.totalDegree (↑p) f)

Prime scaling preserves integer irreducibility whenever it preserves primitivity; avoiding the constant coefficient discharges that condition.