Separable polynomials #
We define a polynomial to be separable if it is coprime with its derivative. We prove basic properties about separable polynomials here.
Main definitions #
Polynomial.Separable f: a polynomialfis separable iff it is coprime with its derivative.
A polynomial is separable iff it is coprime with its derivative.
Equations
- Polynomial.Separable f = IsCoprime f (Polynomial.derivative f)
Instances For
theorem
Polynomial.separable_def
{R : Type u}
[CommSemiring R]
(f : Polynomial R)
:
Polynomial.Separable f ↔ IsCoprime f (Polynomial.derivative f)
theorem
Polynomial.separable_def'
{R : Type u}
[CommSemiring R]
(f : Polynomial R)
:
Polynomial.Separable f ↔ ∃ (a : Polynomial R) (b : Polynomial R), a * f + b * Polynomial.derivative f = 1
theorem
Polynomial.Separable.ne_zero
{R : Type u}
[CommSemiring R]
[Nontrivial R]
{f : Polynomial R}
(h : Polynomial.Separable f)
:
f ≠ 0
@[simp]
theorem
Polynomial.separable_of_subsingleton
{R : Type u}
[CommSemiring R]
[Subsingleton R]
(f : Polynomial R)
:
theorem
Polynomial.separable_X_add_C
{R : Type u}
[CommSemiring R]
(a : R)
:
Polynomial.Separable (Polynomial.X + Polynomial.C a)
theorem
Polynomial.separable_C
{R : Type u}
[CommSemiring R]
(r : R)
:
Polynomial.Separable (Polynomial.C r) ↔ IsUnit r
theorem
Polynomial.Separable.of_mul_left
{R : Type u}
[CommSemiring R]
{f : Polynomial R}
{g : Polynomial R}
(h : Polynomial.Separable (f * g))
:
theorem
Polynomial.Separable.of_mul_right
{R : Type u}
[CommSemiring R]
{f : Polynomial R}
{g : Polynomial R}
(h : Polynomial.Separable (f * g))
:
theorem
Polynomial.Separable.of_dvd
{R : Type u}
[CommSemiring R]
{f : Polynomial R}
{g : Polynomial R}
(hf : Polynomial.Separable f)
(hfg : g ∣ f)
:
theorem
Polynomial.separable_gcd_left
{F : Type u_1}
[Field F]
{f : Polynomial F}
(hf : Polynomial.Separable f)
(g : Polynomial F)
:
theorem
Polynomial.separable_gcd_right
{F : Type u_1}
[Field F]
{g : Polynomial F}
(f : Polynomial F)
(hg : Polynomial.Separable g)
:
theorem
Polynomial.Separable.isCoprime
{R : Type u}
[CommSemiring R]
{f : Polynomial R}
{g : Polynomial R}
(h : Polynomial.Separable (f * g))
:
IsCoprime f g
theorem
Polynomial.Separable.of_pow'
{R : Type u}
[CommSemiring R]
{f : Polynomial R}
{n : ℕ}
(_h : Polynomial.Separable (f ^ n))
:
theorem
Polynomial.Separable.of_pow
{R : Type u}
[CommSemiring R]
{f : Polynomial R}
(hf : ¬IsUnit f)
{n : ℕ}
(hn : n ≠ 0)
(hfs : Polynomial.Separable (f ^ n))
:
Polynomial.Separable f ∧ n = 1
theorem
Polynomial.Separable.map
{R : Type u}
[CommSemiring R]
{S : Type v}
[CommSemiring S]
{p : Polynomial R}
(h : Polynomial.Separable p)
{f : R →+* S}
:
theorem
Polynomial.Separable.eval₂_derivative_ne_zero
{R : Type u}
[CommSemiring R]
{S : Type v}
[CommSemiring S]
[Nontrivial S]
(f : R →+* S)
{p : Polynomial R}
(h : Polynomial.Separable p)
{x : S}
(hx : Polynomial.eval₂ f x p = 0)
:
Polynomial.eval₂ f x (Polynomial.derivative p) ≠ 0
theorem
Polynomial.Separable.aeval_derivative_ne_zero
{R : Type u}
[CommSemiring R]
{S : Type v}
[CommSemiring S]
[Nontrivial S]
[Algebra R S]
{p : Polynomial R}
(h : Polynomial.Separable p)
{x : S}
(hx : (Polynomial.aeval x) p = 0)
:
(Polynomial.aeval x) (Polynomial.derivative p) ≠ 0
theorem
Polynomial.isUnit_of_self_mul_dvd_separable
{R : Type u}
[CommSemiring R]
{p : Polynomial R}
{q : Polynomial R}
(hp : Polynomial.Separable p)
(hq : q * q ∣ p)
:
IsUnit q
theorem
Polynomial.multiplicity_le_one_of_separable
{R : Type u}
[CommSemiring R]
{p : Polynomial R}
{q : Polynomial R}
(hq : ¬IsUnit q)
(hsep : Polynomial.Separable p)
:
multiplicity q p ≤ 1
theorem
Polynomial.Separable.squarefree
{R : Type u}
[CommSemiring R]
{p : Polynomial R}
(hsep : Polynomial.Separable p)
:
A separable polynomial is square-free.
See PerfectField.separable_iff_squarefree for the converse when the coefficients are a perfect
field.
theorem
Polynomial.separable_X_sub_C
{R : Type u}
[CommRing R]
{x : R}
:
Polynomial.Separable (Polynomial.X - Polynomial.C x)
theorem
Polynomial.Separable.mul
{R : Type u}
[CommRing R]
{f : Polynomial R}
{g : Polynomial R}
(hf : Polynomial.Separable f)
(hg : Polynomial.Separable g)
(h : IsCoprime f g)
:
Polynomial.Separable (f * g)
theorem
Polynomial.separable_prod'
{R : Type u}
[CommRing R]
{ι : Type u_1}
{f : ι → Polynomial R}
{s : Finset ι}
:
(∀ x ∈ s, ∀ y ∈ s, x ≠ y → IsCoprime (f x) (f y)) →
(∀ x ∈ s, Polynomial.Separable (f x)) → Polynomial.Separable (Finset.prod s fun (x : ι) => f x)
theorem
Polynomial.separable_prod
{R : Type u}
[CommRing R]
{ι : Type u_1}
[Fintype ι]
{f : ι → Polynomial R}
(h1 : Pairwise (IsCoprime on f))
(h2 : ∀ (x : ι), Polynomial.Separable (f x))
:
Polynomial.Separable (Finset.prod Finset.univ fun (x : ι) => f x)
theorem
Polynomial.Separable.inj_of_prod_X_sub_C
{R : Type u}
[CommRing R]
[Nontrivial R]
{ι : Type u_1}
{f : ι → R}
{s : Finset ι}
(hfs : Polynomial.Separable (Finset.prod s fun (i : ι) => Polynomial.X - Polynomial.C (f i)))
{x : ι}
{y : ι}
(hx : x ∈ s)
(hy : y ∈ s)
(hfxy : f x = f y)
:
x = y
theorem
Polynomial.Separable.injective_of_prod_X_sub_C
{R : Type u}
[CommRing R]
[Nontrivial R]
{ι : Type u_1}
[Fintype ι]
{f : ι → R}
(hfs : Polynomial.Separable (Finset.prod Finset.univ fun (i : ι) => Polynomial.X - Polynomial.C (f i)))
:
theorem
Polynomial.nodup_of_separable_prod
{R : Type u}
[CommRing R]
[Nontrivial R]
{s : Multiset R}
(hs : Polynomial.Separable (Multiset.prod (Multiset.map (fun (a : R) => Polynomial.X - Polynomial.C a) s)))
:
theorem
Polynomial.rootMultiplicity_le_one_of_separable
{R : Type u}
[CommRing R]
[Nontrivial R]
{p : Polynomial R}
(hsep : Polynomial.Separable p)
(x : R)
:
Polynomial.rootMultiplicity x p ≤ 1
theorem
Polynomial.count_roots_le_one
{R : Type u}
[CommRing R]
[IsDomain R]
{p : Polynomial R}
(hsep : Polynomial.Separable p)
(x : R)
:
Multiset.count x (Polynomial.roots p) ≤ 1
theorem
Polynomial.nodup_roots
{R : Type u}
[CommRing R]
[IsDomain R]
{p : Polynomial R}
(hsep : Polynomial.Separable p)
:
theorem
Polynomial.separable_iff_derivative_ne_zero
{F : Type u}
[Field F]
{f : Polynomial F}
(hf : Irreducible f)
:
Polynomial.Separable f ↔ Polynomial.derivative f ≠ 0
theorem
Polynomial.separable_map
{F : Type u}
[Field F]
{S : Type u_1}
[CommRing S]
[Nontrivial S]
(f : F →+* S)
{p : Polynomial F}
:
theorem
Polynomial.separable_prod_X_sub_C_iff'
{F : Type u}
[Field F]
{ι : Type u_1}
{f : ι → F}
{s : Finset ι}
:
Polynomial.Separable (Finset.prod s fun (i : ι) => Polynomial.X - Polynomial.C (f i)) ↔ ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y
theorem
Polynomial.separable_prod_X_sub_C_iff
{F : Type u}
[Field F]
{ι : Type u_1}
[Fintype ι]
{f : ι → F}
:
Polynomial.Separable (Finset.prod Finset.univ fun (i : ι) => Polynomial.X - Polynomial.C (f i)) ↔ Function.Injective f
theorem
Polynomial.separable_or
{F : Type u}
[Field F]
(p : ℕ)
[HF : CharP F p]
{f : Polynomial F}
(hf : Irreducible f)
:
Polynomial.Separable f ∨ ¬Polynomial.Separable f ∧ ∃ (g : Polynomial F), Irreducible g ∧ (Polynomial.expand F p) g = f
theorem
Polynomial.exists_separable_of_irreducible
{F : Type u}
[Field F]
(p : ℕ)
[HF : CharP F p]
{f : Polynomial F}
(hf : Irreducible f)
(hp : p ≠ 0)
:
∃ (n : ℕ) (g : Polynomial F), Polynomial.Separable g ∧ (Polynomial.expand F (p ^ n)) g = f
theorem
Polynomial.isUnit_or_eq_zero_of_separable_expand
{F : Type u}
[Field F]
(p : ℕ)
[HF : CharP F p]
{f : Polynomial F}
(n : ℕ)
(hp : 0 < p)
(hf : Polynomial.Separable ((Polynomial.expand F (p ^ n)) f))
:
theorem
Polynomial.unique_separable_of_irreducible
{F : Type u}
[Field F]
(p : ℕ)
[HF : CharP F p]
{f : Polynomial F}
(hf : Irreducible f)
(hp : 0 < p)
(n₁ : ℕ)
(g₁ : Polynomial F)
(hg₁ : Polynomial.Separable g₁)
(hgf₁ : (Polynomial.expand F (p ^ n₁)) g₁ = f)
(n₂ : ℕ)
(g₂ : Polynomial F)
(hg₂ : Polynomial.Separable g₂)
(hgf₂ : (Polynomial.expand F (p ^ n₂)) g₂ = f)
:
theorem
Polynomial.separable_X_pow_sub_C
{F : Type u}
[Field F]
{n : ℕ}
(a : F)
(hn : ↑n ≠ 0)
(ha : a ≠ 0)
:
Polynomial.Separable (Polynomial.X ^ n - Polynomial.C a)
If n ≠ 0 in F, then X ^ n - a is separable for any a ≠ 0.
theorem
Polynomial.X_pow_sub_one_separable_iff
{F : Type u}
[Field F]
{n : ℕ}
:
Polynomial.Separable (Polynomial.X ^ n - 1) ↔ ↑n ≠ 0
In a field F, X ^ n - 1 is separable iff ↑n ≠ 0.
theorem
Polynomial.card_rootSet_eq_natDegree
{F : Type u}
[Field F]
{K : Type v}
[Field K]
[Algebra F K]
{p : Polynomial F}
(hsep : Polynomial.Separable p)
(hsplit : Polynomial.Splits (algebraMap F K) p)
:
theorem
Polynomial.nodup_roots_iff_of_splits
{F : Type u}
[Field F]
{f : Polynomial F}
(hf : f ≠ 0)
(h : Polynomial.Splits (RingHom.id F) f)
:
If a non-zero polynomial splits, then it has no repeated roots on that field if and only if it is separable.
theorem
Polynomial.nodup_aroots_iff_of_splits
{F : Type u}
[Field F]
{K : Type v}
[Field K]
[Algebra F K]
{f : Polynomial F}
(hf : f ≠ 0)
(h : Polynomial.Splits (algebraMap F K) f)
:
If a non-zero polynomial over F splits in K, then it has no repeated roots on K
if and only if it is separable.
theorem
Polynomial.card_rootSet_eq_natDegree_iff_of_splits
{F : Type u}
[Field F]
{K : Type v}
[Field K]
[Algebra F K]
{f : Polynomial F}
(hf : f ≠ 0)
(h : Polynomial.Splits (algebraMap F K) f)
:
theorem
Polynomial.eq_X_sub_C_of_separable_of_root_eq
{F : Type u}
[Field F]
{K : Type v}
[Field K]
{i : F →+* K}
{x : F}
{h : Polynomial F}
(h_sep : Polynomial.Separable h)
(h_root : Polynomial.eval x h = 0)
(h_splits : Polynomial.Splits i h)
(h_roots : ∀ y ∈ Polynomial.roots (Polynomial.map i h), y = i x)
:
h = Polynomial.C (Polynomial.leadingCoeff h) * (Polynomial.X - Polynomial.C x)
theorem
Polynomial.exists_finset_of_splits
{F : Type u}
[Field F]
{K : Type v}
[Field K]
(i : F →+* K)
{f : Polynomial F}
(sep : Polynomial.Separable f)
(sp : Polynomial.Splits i f)
:
∃ (s : Finset K),
Polynomial.map i f = Polynomial.C (i (Polynomial.leadingCoeff f)) * Finset.prod s fun (a : K) => Polynomial.X - Polynomial.C a
theorem
Irreducible.separable
{F : Type u}
[Field F]
[CharZero F]
{f : Polynomial F}
(hf : Irreducible f)
:
theorem
isSeparable_def
(F : Type u_1)
(K : Type u_2)
[CommRing F]
[Ring K]
[Algebra F K]
:
IsSeparable F K ↔ ∀ (x : K), Polynomial.Separable (minpoly F x)
Typeclass for separable field extension: K is a separable field extension of F iff
the minimal polynomial of every x : K is separable. This implies that K/F is an algebraic
extension, because the minimal polynomial of a non-integral element is 0, which is not
separable.
We define this for general (commutative) rings and only assume F and K are fields if this
is needed for a proof.
- separable' : ∀ (x : K), Polynomial.Separable (minpoly F x)
Instances
theorem
IsSeparable.separable
(F : Type u_1)
{K : Type u_2}
[CommRing F]
[Ring K]
[Algebra F K]
[IsSeparable F K]
(x : K)
:
Polynomial.Separable (minpoly F x)
theorem
Polynomial.Separable.isIntegral
{F : Type u_1}
{K : Type u_2}
[CommRing F]
[Ring K]
[Algebra F K]
{x : K}
(h : Polynomial.Separable (minpoly F x))
:
IsIntegral F x
If the minimal polynomial of x : K over F is separable, then x is integral over F,
because the minimal polynomial of a non-integral element is 0, which is not separable.
theorem
IsSeparable.isIntegral
(F : Type u_1)
{K : Type u_2}
[CommRing F]
[Ring K]
[Algebra F K]
[IsSeparable F K]
(x : K)
:
IsIntegral F x
theorem
isSeparable_iff
{F : Type u_1}
{K : Type u_2}
[CommRing F]
[Ring K]
[Algebra F K]
:
IsSeparable F K ↔ ∀ (x : K), IsIntegral F x ∧ Polynomial.Separable (minpoly F x)
theorem
AlgEquiv.isSeparable
{F : Type u_1}
{K : Type u_2}
[CommRing F]
[Ring K]
[Algebra F K]
{E : Type u_3}
[Ring E]
[Algebra F E]
(e : K ≃ₐ[F] E)
[IsSeparable F K]
:
IsSeparable F E
Transfer IsSeparable across an AlgEquiv.
theorem
AlgEquiv.isSeparable_iff
{F : Type u_1}
{K : Type u_2}
[CommRing F]
[Ring K]
[Algebra F K]
{E : Type u_3}
[Ring E]
[Algebra F E]
(e : K ≃ₐ[F] E)
:
IsSeparable F K ↔ IsSeparable F E
theorem
IsSeparable.isAlgebraic
(F : Type u_1)
(K : Type u_2)
[CommRing F]
[Ring K]
[Algebra F K]
[Nontrivial F]
[IsSeparable F K]
:
Equations
- (_ : IsSeparable F F) = (_ : IsSeparable F F)
instance
IsSeparable.of_finite
(F : Type u_1)
(K : Type u_2)
[Field F]
[Field K]
[Algebra F K]
[FiniteDimensional F K]
[CharZero F]
:
IsSeparable F K
A finite field extension in characteristic 0 is separable.
Equations
- (_ : IsSeparable F K) = (_ : IsSeparable F K)
theorem
Polynomial.Separable.map_minpoly
{A : Type u_1}
[CommRing A]
(K : Type u_2)
[Field K]
[Algebra A K]
{R : Type u_3}
[CommRing R]
[Algebra A R]
[Algebra K R]
[IsScalarTower A K R]
{x : R}
(h : Polynomial.Separable (minpoly A x))
:
Polynomial.Separable (minpoly K x)
If R / K / A is an extension tower, x : R is separable over A, then it's also separable
over K.
theorem
isSeparable_tower_top_of_isSeparable
(F : Type u_1)
(K : Type u_2)
(E : Type u_3)
[Field F]
[Field K]
[Field E]
[Algebra F K]
[Algebra F E]
[Algebra K E]
[IsScalarTower F K E]
[IsSeparable F E]
:
IsSeparable K E
theorem
isSeparable_tower_bot_of_isSeparable
(F : Type u_1)
(K : Type u_2)
(E : Type u_3)
[Field F]
[Field K]
[Field E]
[Algebra F K]
[Algebra F E]
[Algebra K E]
[IsScalarTower F K E]
[h : IsSeparable F E]
:
IsSeparable F K
theorem
IsSeparable.of_algHom
(F : Type u_1)
{E : Type u_3}
[Field F]
[Field E]
[Algebra F E]
(E' : Type u_4)
[Field E']
[Algebra F E']
(f : E →ₐ[F] E')
[IsSeparable F E']
:
IsSeparable F E
theorem
IsSeparable.of_equiv_equiv
{A₁ : Type u_4}
{B₁ : Type u_5}
{A₂ : Type u_6}
{B₂ : Type u_7}
[Field A₁]
[Field B₁]
[Field A₂]
[Field B₂]
[Algebra A₁ B₁]
[Algebra A₂ B₂]
(e₁ : A₁ ≃+* A₂)
(e₂ : B₁ ≃+* B₂)
(he : RingHom.comp (algebraMap A₂ B₂) ↑e₁ = RingHom.comp (↑e₂) (algebraMap A₁ B₁))
[IsSeparable A₁ B₁]
:
IsSeparable A₂ B₂
theorem
AlgHom.card_of_powerBasis
{S : Type u_2}
[CommRing S]
{K : Type u_4}
{L : Type u_5}
[Field K]
[Field L]
[Algebra K S]
[Algebra K L]
(pb : PowerBasis K S)
(h_sep : Polynomial.Separable (minpoly K pb.gen))
(h_splits : Polynomial.Splits (algebraMap K L) (minpoly K pb.gen))
:
Fintype.card (S →ₐ[K] L) = pb.dim