An irreducible highest homogeneous component forces irreducibility of the full polynomial. Coefficient reduction preserves this implication and the full degree whenever the reduced highest component remains irreducible.
theorem
CCDN.map_homogeneousComponent
{R : Type u_1}
{S : Type u_2}
{σ : Type u_3}
[CommRing R]
[CommRing S]
(φ : R →+* S)
(d : ℕ)
(f : MvPolynomial σ R)
:
(MvPolynomial.map φ) ((MvPolynomial.homogeneousComponent d) f) = (MvPolynomial.homogeneousComponent d) ((MvPolynomial.map φ) f)
Applying a ring homomorphism to the coefficients commutes with taking the homogeneous
component of degree d.
theorem
CCDN.map_degree_and_irreducible_of_top_irreducible
{R : Type u_1}
{K : Type u_2}
{σ : Type u_3}
[CommRing R]
[Field K]
(φ : R →+* K)
(f : MvPolynomial σ R)
(hir : Irreducible ((MvPolynomial.map φ) ((MvPolynomial.homogeneousComponent f.totalDegree) f)))
:
If the coefficient image of the original top component is irreducible, the full coefficient image has unchanged total degree and is irreducible.