English
If f is monic and f.map φ is irreducible in the target ring, then f is irreducible in the source ring.
Русский
Если f моноцен и f.map φ делим на неприводимые в целевом кольце, тогда f неприводим в исходном кольце.
LaTeX
$$Monic f → Irreducible (map φ f) → Irreducible f$$
Lean4
/-- A polynomial over an integral domain `R` is irreducible if it is monic and
irreducible after mapping into an integral domain `S`.
A special case of this lemma is that a polynomial over `ℤ` is irreducible if
it is monic and irreducible over `ℤ/pℤ` for some prime `p`.
-/
theorem irreducible_of_irreducible_map (f : R[X]) (h_mon : Monic f) (h_irr : Irreducible (f.map φ)) : Irreducible f :=
by
refine ⟨h_irr.not_isUnit ∘ IsUnit.map (mapRingHom φ), fun a b h => ?_⟩
dsimp [Monic] at h_mon
have q := (leadingCoeff_mul a b).symm
rw [← h, h_mon] at q
refine (h_irr.isUnit_or_isUnit <| (congr_arg (Polynomial.map φ) h).trans (Polynomial.map_mul φ)).imp ?_ ?_ <;>
apply isUnit_of_isUnit_leadingCoeff_of_isUnit_map <;>
apply isUnit_of_mul_eq_one
· exact q
· rw [mul_comm]
exact q
