English
If f is a primitive polynomial with certain coefficient conditions and leading coefficient not in P^2 in a quotient, then f is irreducible.
Русский
Если f — примитивный полином с заданными условиями коэффициентов и ведущий коэффициент не в P^2 в фактор-моде, то f ирредуцируем.
LaTeX
$$$\\text{irreducible_of_eisenstein_criterion}$$$
Lean4
/-- If `f` is a nonconstant polynomial with coefficients in `R`, and `P` is a prime ideal in `R`,
then if every coefficient in `R` except the leading coefficient is in `P`, and
the trailing coefficient is not in `P^2` and no nonunits in `R` divide `f`, then `f` is
irreducible. -/
theorem irreducible_of_eisenstein_criterion {f : R[X]} {P : Ideal R} (hP : P.IsPrime) (hfl : f.leadingCoeff ∉ P)
(hfP : ∀ n : ℕ, ↑n < degree f → f.coeff n ∈ P) (hfd0 : 0 < degree f) (h0 : f.coeff 0 ∉ P ^ 2) (hu : f.IsPrimitive) :
Irreducible f :=
by
apply
generalizedEisenstein (K := FractionRing (R ⧸ P)) (q := X) (p := f.natDegree) (by simp [map_X, irreducible_X])
monic_X hu (natDegree_pos_iff_degree_pos.mpr hfd0)
· simp only [IsScalarTower.algebraMap_eq R (R ⧸ P) (FractionRing (R ⧸ P)), Quotient.algebraMap_eq, coe_comp,
Function.comp_apply, ne_eq, FaithfulSMul.algebraMap_eq_zero_iff]
rw [Ideal.Quotient.eq_zero_iff_mem]
exact hfl
· rw [← map_C, ← Polynomial.map_pow, ← Polynomial.map_mul]
simp only [IsScalarTower.algebraMap_eq R (R ⧸ P) (FractionRing (R ⧸ P)), Quotient.algebraMap_eq, ← map_map]
congr 1
ext n
simp only [coeff_map, Ideal.Quotient.mk_eq_mk_iff_sub_mem]
simp only [coeff_C_mul, coeff_X_pow, mul_ite, mul_one, mul_zero, sub_ite, sub_zero]
split_ifs with hn
· rw [hn, leadingCoeff, sub_self]
exact zero_mem _
· by_cases hn' : n < f.natDegree
· exact hfP _ (coe_lt_degree.mpr hn')
· rw [f.coeff_eq_zero_of_natDegree_lt]
· exact P.zero_mem
· simp [Nat.lt_iff_le_and_ne, ← Nat.not_lt, hn', Ne.symm hn]
· rw [modByMonic_X, map_C, ne_eq, C_eq_zero, Ideal.Quotient.eq_zero_iff_mem, ← coeff_zero_eq_eval_zero]
convert h0
· rw [IsScalarTower.algebraMap_eq R (R ⧸ P) (FractionRing (R ⧸ P))]
rw [ker_comp_of_injective]
· ext a; simp
· exact FaithfulSMul.algebraMap_injective (R ⧸ P) (FractionRing (R ⧸ P))
