Units of multivariate polynomials under a change of coefficients

Over a commutative ring, a polynomial is a unit exactly when its constant coefficient is a unit and its other coefficients are nilpotent. Mapping the coefficients along an injective local homomorphism f : R →+* S of commutative rings therefore reflects units: if map f p is a unit of S[X_σ], then, since f is injective and reflects units, the same coefficient conditions hold for p. In other words map f is a local homomorphism, so irreducibility of map f p implies irreducibility of p (Irreducible.of_map). Every ring homomorphism from a field k into a nontrivial commutative ring is injective and local, so this holds for it with no hypothesis. This is how absolute irreducibility, over an algebraic closure, gives irreducibility over every intermediate field.

Main results

• MvPolynomial.isLocalHom_map_of_injective: map f reflects units for an injective local homomorphism f of commutative rings.
• MvPolynomial.isLocalHom_map: its specialization to a ring homomorphism f out of a field into a nontrivial commutative ring. It is an instance, so Irreducible.of_map applies to map f directly.
• MvPolynomial.isUnit_iff_totalDegree_eq_zero: a nonzero polynomial over a field is a unit exactly when its total degree is zero.

theorem MvPolynomial.isUnit_iff_totalDegree_eq_zero {σ : Type u_1} {k : Type u_2} [Field k] {p : MvPolynomial σ k} (hp : p ≠ 0) : IsUnit p ↔ p.totalDegree = 0

Over a field, a nonzero polynomial is a unit exactly when its total degree is zero, that is, when it is a nonzero constant.

theorem MvPolynomial.isLocalHom_map_of_injective {σ : Type u_1} {R : Type u_4} {S : Type u_5} [CommRing R] [CommRing S] (f : R →+* S) [IsLocalHom f] (hf : Function.Injective ⇑f) : IsLocalHom (map f)

Changing the coefficients along an injective local homomorphism reflects units: if f : R →+* S is an injective local homomorphism of commutative rings and map f p is a unit, so is p.

instance MvPolynomial.isLocalHom_map {σ : Type u_1} {k : Type u_2} {L : Type u_3} [Field k] [CommRing L] [Nontrivial L] (f : k →+* L) : IsLocalHom (map f)

Changing the coefficients along a ring homomorphism from a field into a nontrivial commutative ring reflects units: if map f p is a unit, so is p. Hence Irreducible.of_map applies to map f.