English
If L/K is an integral extension with K a domain and L a field, then any irreducible polynomial over L divides a monic irreducible polynomial over K after mapping the coefficients via the algebra map K→L.
Русский
Если L/K является интегральным расширением, K — область, L — поле, тогда любой ирредуцируемый полином над L делит монический ирредуцируемый полином над K после отображения коэффициентов через алгебраическое отображение K→L.
LaTeX
$$$$ \exists g \in K[X]\; (g \text{ монопольный и ирредукцируемый}) \text{ such that } f \mid g^{\sigma} \; (\sigma: K \to L) $$$$
Lean4
/-- If `L / K` is an integral extension, `K` is a domain, `L` is a field, then any irreducible
polynomial over `L` divides some monic irreducible polynomial over `K`. -/
theorem exists_dvd_monic_irreducible_of_isIntegral {K L : Type*} [CommRing K] [IsDomain K] [Field L] [Algebra K L]
[Algebra.IsIntegral K L] {f : L[X]} (hf : Irreducible f) :
∃ g : K[X], g.Monic ∧ Irreducible g ∧ f ∣ g.map (algebraMap K L) :=
by
haveI := Fact.mk hf
have h := hf.ne_zero
have h2 := isIntegral_trans (R := K) _ (AdjoinRoot.isIntegral_root h)
have h3 := (AdjoinRoot.minpoly_root h) ▸ minpoly.dvd_map_of_isScalarTower K L (AdjoinRoot.root f)
exact ⟨_, minpoly.monic h2, minpoly.irreducible h2, dvd_of_mul_right_dvd h3⟩
