English
Gauss's Lemma for GCD domains: a primitive polynomial p ∈ R[X] is irreducible if and only if p.map(algebraMap R K) is irreducible in K[X].
Русский
Лемма Гаусса для GCD-домена: примитивный полином p ∈ R[X] неприводим тогда, когда p.map(algebraMap R K) неприводим в K[X].
LaTeX
$$p.IsPrimitive → (Irreducible p ↔ Irreducible (p.map (algebraMap R K)))$$
Lean4
/-- **Gauss's Lemma** for GCD domains states that a primitive polynomial is irreducible iff it is
irreducible in the fraction field. -/
theorem irreducible_iff_irreducible_map_fraction_map {p : R[X]} (hp : p.IsPrimitive) :
Irreducible p ↔ Irreducible (p.map (algebraMap R K)) :=
by
refine
⟨fun hi => ⟨fun h => hi.not_isUnit (hp.isUnit_iff_isUnit_map.2 h), fun a b hab => ?_⟩,
hp.irreducible_of_irreducible_map_of_injective (IsFractionRing.injective _ _)⟩
obtain ⟨⟨c, c0⟩, hc⟩ := integerNormalization_map_to_map R⁰ a
obtain ⟨⟨d, d0⟩, hd⟩ := integerNormalization_map_to_map R⁰ b
rw [Algebra.smul_def, algebraMap_apply, Subtype.coe_mk] at hc hd
rw [mem_nonZeroDivisors_iff_ne_zero] at c0 d0
have hcd0 : c * d ≠ 0 := mul_ne_zero c0 d0
rw [Ne, ← C_eq_zero] at hcd0
have h1 : C c * C d * p = integerNormalization R⁰ a * integerNormalization R⁰ b :=
by
apply map_injective (algebraMap R K) (IsFractionRing.injective _ _) _
rw [Polynomial.map_mul, Polynomial.map_mul, Polynomial.map_mul, hc, hd, map_C, map_C, hab]
ring
obtain ⟨u, hu⟩ : Associated (c * d) (content (integerNormalization R⁰ a) * content (integerNormalization R⁰ b)) := by
rw [← dvd_dvd_iff_associated, ← normalize_eq_normalize_iff, normalize.map_mul, normalize.map_mul, normalize_content,
normalize_content, ← mul_one (normalize c * normalize d), ← hp.content_eq_one, ← content_C, ← content_C, ←
content_mul, ← content_mul, ← content_mul, h1]
rw [← RingHom.map_mul, eq_comm, (integerNormalization R⁰ a).eq_C_content_mul_primPart,
(integerNormalization R⁰ b).eq_C_content_mul_primPart, mul_assoc, mul_comm _ (C _ * _), ← mul_assoc, ← mul_assoc, ←
RingHom.map_mul, ← hu, RingHom.map_mul, mul_assoc, mul_assoc, ← mul_assoc (C (u : R))] at h1
have h0 : a ≠ 0 ∧ b ≠ 0 := by
classical
rw [Ne, Ne, ← not_or, ← mul_eq_zero, ← hab]
intro con
apply hp.ne_zero (map_injective (algebraMap R K) (IsFractionRing.injective _ _) _)
simp [con]
rcases hi.isUnit_or_isUnit (mul_left_cancel₀ hcd0 h1).symm with (h | h)
· right
apply isUnit_or_eq_zero_of_isUnit_integerNormalization_primPart h0.2 (isUnit_of_mul_isUnit_right h)
· left
apply isUnit_or_eq_zero_of_isUnit_integerNormalization_primPart h0.1 h
