English
For a polynomial f over a field F, irreducibility implies that f is separable or there exists a separable g with a specific expansion relation; this is used to study separable polynomials in characteristic p.
Русский
Пусть f ∈ F[x] иррефлексible; тогда либо f разделим, либо существует сепарабельный g, удовлетворяющий соотношениям expansion.
LaTeX
$$$\\text{Irreducible}(f) \\Rightarrow (f \\text{ separable}) \\lor (\\exists g: F[x], Irreducible(g) \\land \\text{expand}(f) = g)$$$
Lean4
theorem separable_or {f : F[X]} (hf : Irreducible f) :
f.Separable ∨ ¬f.Separable ∧ ∃ g : F[X], Irreducible g ∧ expand F p g = f := by
classical
exact
if H : derivative f = 0 then by
rcases p.eq_zero_or_pos with (rfl | hp)
· haveI := CharP.charP_to_charZero F
have := natDegree_eq_zero_of_derivative_eq_zero H
have := (natDegree_pos_iff_degree_pos.mpr <| degree_pos_of_irreducible hf).ne'
contradiction
haveI := isLocalHom_expand F hp
exact
Or.inr
⟨by rw [separable_iff_derivative_ne_zero hf, Classical.not_not, H], contract p f,
Irreducible.of_map (by rwa [← expand_contract p H hp.ne'] at hf), expand_contract p H hp.ne'⟩
else Or.inl <| (separable_iff_derivative_ne_zero hf).2 H
