Dehomogenization preserves degree and irreducibility when the homogenizing coordinate does not divide the homogeneous equation.

theorem CCDN.irreducible_of_affineChart_irreducible {K : Type u_1} [Field K] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) K) (hdeg : ((affineChart n) f).totalDegree = f.totalDegree) (hir : Irreducible ((affineChart n) f)) : Irreducible f

A full-degree affine chart detects irreducibility of the original equation; a factor lost on the chart would force a degree drop.

theorem CCDN.variable_not_dvd_irreducible_homogeneous {K : Type u_1} [Field K] {n d : ℕ} (f : MvPolynomial (Fin (n + 1)) K) (hf : f.IsHomogeneous d) (hir : Irreducible f) (hd : 2 ≤ d) (j : Fin (n + 1)) : ¬MvPolynomial.X j ∣ f

No variable X j divides an irreducible homogeneous polynomial of degree at least 2.

theorem CCDN.irreducible_homogeneous_not_dvd_variable {K : Type u_1} [Field K] {n d : ℕ} (f : MvPolynomial (Fin (n + 1)) K) (hf : f.IsHomogeneous d) (hir : Irreducible f) (hd : 2 ≤ d) (j : Fin (n + 1)) : ¬f ∣ MvPolynomial.X j

An irreducible homogeneous polynomial of degree at least 2 divides no variable X j.

theorem CCDN.affineChart_degree_of_not_variable_dvd {K : Type u_1} [Field K] {n d : ℕ} (f : MvPolynomial (Fin (n + 1)) K) (hf : f.IsHomogeneous d) (hX : ¬MvPolynomial.X 0 ∣ f) : ((affineChart n) f).totalDegree = d

If X 0 does not divide the homogeneous polynomial f of degree d, then the affine chart x₀ = 1 of f has total degree exactly d.

theorem CCDN.affineChart_irreducible_of_not_variable_dvd {K : Type u_1} [Field K] {n d : ℕ} (f : MvPolynomial (Fin (n + 1)) K) (hf : f.IsHomogeneous d) (hir : Irreducible f) (hX : ¬MvPolynomial.X 0 ∣ f) : Irreducible ((affineChart n) f)

If X 0 does not divide the irreducible homogeneous polynomial f, then the affine chart x₀ = 1 of f is irreducible.

theorem CCDN.affineChart_rename_swap_irreducible_degree {K : Type u_1} {R : Type u_2} [CommRing K] [Field R] {n d : ℕ} (φ : K →+* R) (f : MvPolynomial (Fin (n + 1)) K) (hf : f.IsHomogeneous d) (hd : 2 ≤ d) (hir : Irreducible ((MvPolynomial.map φ) f)) (k : Fin (n + 1)) : Irreducible ((MvPolynomial.map φ) ((affineChart n) ((MvPolynomial.rename ⇑(Equiv.swap 0 k)) f))) ∧ ((MvPolynomial.map φ) ((affineChart n) ((MvPolynomial.rename ⇑(Equiv.swap 0 k)) f))).totalDegree = d

After mapping coefficients into a field, every pivot chart of an irreducible homogeneous polynomial of degree at least two remains irreducible and has the original degree.