Documentation

Mathlib.FieldTheory.Separable

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 #

A polynomial is separable iff it is coprime with its derivative.

Equations
  • f.Separable = IsCoprime f (Polynomial.derivative f)
Instances For
    theorem Polynomial.separable_def {R : Type u} [CommSemiring R] (f : Polynomial R) :
    f.Separable IsCoprime f (Polynomial.derivative f)
    theorem Polynomial.separable_def' {R : Type u} [CommSemiring R] (f : Polynomial R) :
    f.Separable ∃ (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 : f.Separable) :
    f 0
    theorem Polynomial.separable_X_add_C {R : Type u} [CommSemiring R] (a : R) :
    (Polynomial.X + Polynomial.C a).Separable
    theorem Polynomial.separable_X {R : Type u} [CommSemiring R] :
    Polynomial.X.Separable
    theorem Polynomial.separable_C {R : Type u} [CommSemiring R] (r : R) :
    (Polynomial.C r).Separable IsUnit r
    theorem Polynomial.Separable.of_mul_left {R : Type u} [CommSemiring R] {f : Polynomial R} {g : Polynomial R} (h : (f * g).Separable) :
    f.Separable
    theorem Polynomial.Separable.of_mul_right {R : Type u} [CommSemiring R] {f : Polynomial R} {g : Polynomial R} (h : (f * g).Separable) :
    g.Separable
    theorem Polynomial.Separable.of_dvd {R : Type u} [CommSemiring R] {f : Polynomial R} {g : Polynomial R} (hf : f.Separable) (hfg : g f) :
    g.Separable
    theorem Polynomial.separable_gcd_left {F : Type u_1} [Field F] [DecidableEq (Polynomial F)] {f : Polynomial F} (hf : f.Separable) (g : Polynomial F) :
    (EuclideanDomain.gcd f g).Separable
    theorem Polynomial.separable_gcd_right {F : Type u_1} [Field F] [DecidableEq (Polynomial F)] {g : Polynomial F} (f : Polynomial F) (hg : g.Separable) :
    (EuclideanDomain.gcd f g).Separable
    theorem Polynomial.Separable.isCoprime {R : Type u} [CommSemiring R] {f : Polynomial R} {g : Polynomial R} (h : (f * g).Separable) :
    theorem Polynomial.Separable.of_pow' {R : Type u} [CommSemiring R] {f : Polynomial R} {n : } (_h : (f ^ n).Separable) :
    IsUnit f f.Separable n = 1 n = 0
    theorem Polynomial.Separable.of_pow {R : Type u} [CommSemiring R] {f : Polynomial R} (hf : ¬IsUnit f) {n : } (hn : n 0) (hfs : (f ^ n).Separable) :
    f.Separable n = 1
    theorem Polynomial.Separable.map {R : Type u} [CommSemiring R] {S : Type v} [CommSemiring S] {p : Polynomial R} (h : p.Separable) {f : R →+* S} :
    (Polynomial.map f p).Separable
    theorem Associated.separable {R : Type u} [CommSemiring R] {f : Polynomial R} {g : Polynomial R} (ha : Associated f g) (h : f.Separable) :
    g.Separable
    theorem Associated.separable_iff {R : Type u} [CommSemiring R] {f : Polynomial R} {g : Polynomial R} (ha : Associated f g) :
    f.Separable g.Separable
    theorem Polynomial.Separable.mul_unit {R : Type u} [CommSemiring R] {f : Polynomial R} {g : Polynomial R} (hf : f.Separable) (hg : IsUnit g) :
    (f * g).Separable
    theorem Polynomial.Separable.unit_mul {R : Type u} [CommSemiring R] {f : Polynomial R} {g : Polynomial R} (hf : IsUnit f) (hg : g.Separable) :
    (f * g).Separable
    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 : p.Separable) {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 : p.Separable) {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 : p.Separable) (hq : q * q p) :
    theorem Polynomial.multiplicity_le_one_of_separable {R : Type u} [CommSemiring R] [DecidableRel fun (x x_1 : Polynomial R) => x x_1] {p : Polynomial R} {q : Polynomial R} (hq : ¬IsUnit q) (hsep : p.Separable) :
    theorem Polynomial.Separable.squarefree {R : Type u} [CommSemiring R] {p : Polynomial R} (hsep : p.Separable) :

    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.X - Polynomial.C x).Separable
    theorem Polynomial.Separable.mul {R : Type u} [CommRing R] {f : Polynomial R} {g : Polynomial R} (hf : f.Separable) (hg : g.Separable) (h : IsCoprime f g) :
    (f * g).Separable
    theorem Polynomial.separable_prod' {R : Type u} [CommRing R] {ι : Type u_1} {f : ιPolynomial R} {s : Finset ι} :
    (∀ xs, ys, x yIsCoprime (f x) (f y))(∀ xs, (f x).Separable)(∏ xs, f x).Separable
    theorem Polynomial.separable_prod {R : Type u} [CommRing R] {ι : Type u_1} [Fintype ι] {f : ιPolynomial R} (h1 : Pairwise (IsCoprime on f)) (h2 : ∀ (x : ι), (f x).Separable) :
    (∏ x : ι, f x).Separable
    theorem Polynomial.Separable.inj_of_prod_X_sub_C {R : Type u} [CommRing R] [Nontrivial R] {ι : Type u_1} {f : ιR} {s : Finset ι} (hfs : (∏ is, (Polynomial.X - Polynomial.C (f i))).Separable) {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 : (∏ i : ι, (Polynomial.X - Polynomial.C (f i))).Separable) :
    theorem Polynomial.nodup_of_separable_prod {R : Type u} [CommRing R] [Nontrivial R] {s : Multiset R} (hs : (Multiset.map (fun (a : R) => Polynomial.X - Polynomial.C a) s).prod.Separable) :
    s.Nodup
    theorem Polynomial.separable_X_pow_sub_C_unit {R : Type u} [CommRing R] {n : } (u : Rˣ) (hn : IsUnit n) :
    (Polynomial.X ^ n - Polynomial.C u).Separable

    If IsUnit n in a CommRing R, then X ^ n - u is separable for any unit u.

    theorem Polynomial.count_roots_le_one {R : Type u} [CommRing R] [IsDomain R] [DecidableEq R] {p : Polynomial R} (hsep : p.Separable) (x : R) :
    Multiset.count x p.roots 1
    theorem Polynomial.nodup_roots {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hsep : p.Separable) :
    p.roots.Nodup
    theorem Polynomial.separable_iff_derivative_ne_zero {F : Type u} [Field F] {f : Polynomial F} (hf : Irreducible f) :
    f.Separable 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} :
    (Polynomial.map f p).Separable p.Separable
    theorem Polynomial.separable_prod_X_sub_C_iff' {F : Type u} [Field F] {ι : Type u_1} {f : ιF} {s : Finset ι} :
    (∏ is, (Polynomial.X - Polynomial.C (f i))).Separable xs, ys, f x = f yx = y
    theorem Polynomial.separable_prod_X_sub_C_iff {F : Type u} [Field F] {ι : Type u_1} [Fintype ι] {f : ιF} :
    (∏ i : ι, (Polynomial.X - Polynomial.C (f i))).Separable Function.Injective f
    theorem Polynomial.separable_or {F : Type u} [Field F] (p : ) [HF : CharP F p] {f : Polynomial F} (hf : Irreducible f) :
    f.Separable ¬f.Separable ∃ (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), g.Separable (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.expand F (p ^ n)) f).Separable) :
    IsUnit f n = 0
    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₁ : g₁.Separable) (hgf₁ : (Polynomial.expand F (p ^ n₁)) g₁ = f) (n₂ : ) (g₂ : Polynomial F) (hg₂ : g₂.Separable) (hgf₂ : (Polynomial.expand F (p ^ n₂)) g₂ = f) :
    n₁ = n₂ g₁ = g₂
    theorem Polynomial.separable_X_pow_sub_C {F : Type u} [Field F] {n : } (a : F) (hn : n 0) (ha : a 0) :
    (Polynomial.X ^ n - Polynomial.C a).Separable

    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.X ^ n - 1).Separable 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 : p.Separable) (hsplit : Polynomial.Splits (algebraMap F K) p) :
    Fintype.card (p.rootSet K) = p.natDegree
    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) :
    f.roots.Nodup f.Separable

    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) :
    (f.aroots K).Nodup f.Separable

    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) :
    Fintype.card (f.rootSet K) = f.natDegree f.Separable
    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 : h.Separable) (h_root : Polynomial.eval x h = 0) (h_splits : Polynomial.Splits i h) (h_roots : y(Polynomial.map i h).roots, y = i x) :
    h = Polynomial.C h.leadingCoeff * (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 : f.Separable) (sp : Polynomial.Splits i f) :
    ∃ (s : Finset K), Polynomial.map i f = Polynomial.C (i f.leadingCoeff) * as, (Polynomial.X - Polynomial.C a)
    theorem Irreducible.separable {F : Type u} [Field F] [CharZero F] {f : Polynomial F} (hf : Irreducible f) :
    f.Separable
    def IsSeparable (F : Type u_1) {K : Type u_3} [CommRing F] [Ring K] [Algebra F K] (x : K) :

    An element x of an algebra K over a commutative ring F is said to be separable, if its minimal polynomial over K is separable. Note that the minimal polynomial of any element not integral over F is defined to be 0, which is not a separable polynomial.

    Equations
    Instances For
      theorem Algebra.isSeparable_def (F : Type u_1) (K : Type u_3) [CommRing F] [Ring K] [Algebra F K] :
      Algebra.IsSeparable F K ∀ (x : K), IsSeparable F x
      class Algebra.IsSeparable (F : Type u_1) (K : Type u_3) [CommRing F] [Ring K] [Algebra F K] :

      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.

      Instances
        theorem Algebra.IsSeparable.isSeparable' {F : Type u_1} {K : Type u_3} :
        ∀ {inst : CommRing F} {inst_1 : Ring K} {inst_2 : Algebra F K} [self : Algebra.IsSeparable F K] (x : K), IsSeparable F x
        theorem Algebra.IsSeparable.isSeparable (F : Type u_1) {K : Type u_3} [CommRing F] [Ring K] [Algebra F K] [Algebra.IsSeparable F K] (x : K) :
        theorem IsSeparable.isIntegral {F : Type u_1} {K : Type u_3} [CommRing F] [Ring K] [Algebra F K] {x : K} (h : IsSeparable 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 Algebra.IsSeparable.isIntegral (F : Type u_1) {K : Type u_3} [CommRing F] [Ring K] [Algebra F K] [Algebra.IsSeparable F K] (x : K) :
        Equations
        • =
        theorem Algebra.isSeparable_iff {F : Type u_1} {K : Type u_3} [CommRing F] [Ring K] [Algebra F K] :
        theorem AlgEquiv.isSeparable_iff {F : Type u_1} {K : Type u_3} [CommRing F] [Ring K] [Algebra F K] {E : Type u_4} [Ring E] [Algebra F E] (e : K ≃ₐ[F] E) {x : K} :

        Transfer IsSeparable across an AlgEquiv.

        theorem AlgEquiv.Algebra.isSeparable {F : Type u_1} {K : Type u_3} [CommRing F] [Ring K] [Algebra F K] {E : Type u_4} [Ring E] [Algebra F E] (e : K ≃ₐ[F] E) [Algebra.IsSeparable F K] :

        Transfer Algebra.IsSeparable across an AlgEquiv.

        @[deprecated AlgEquiv.Algebra.isSeparable]
        theorem AlgEquiv.isSeparable {F : Type u_1} {K : Type u_3} [CommRing F] [Ring K] [Algebra F K] {E : Type u_4} [Ring E] [Algebra F E] (e : K ≃ₐ[F] E) [Algebra.IsSeparable F K] :

        Alias of AlgEquiv.Algebra.isSeparable.


        Transfer Algebra.IsSeparable across an AlgEquiv.

        theorem AlgEquiv.Algebra.isSeparable_iff {F : Type u_1} {K : Type u_3} [CommRing F] [Ring K] [Algebra F K] {E : Type u_4} [Ring E] [Algebra F E] (e : K ≃ₐ[F] E) :
        theorem IsSeparable.tower_top {F : Type u_1} (L : Type u_2) [CommRing F] {E : Type u_4} [Field L] [CommRing E] [Algebra F L] [Algebra F E] [Algebra L E] [IsScalarTower F L E] {x : E} (h : IsSeparable F x) :

        If E / L / F is a scalar tower and x : E is separable over F, then it's also separable over L.

        @[deprecated Algebra.isSeparable_tower_top_of_isSeparable]
        theorem IsSeparable.of_isScalarTower (F : Type u_1) (L : Type u_2) [CommRing F] (E : Type u_4) [Field L] [CommRing E] [Algebra F L] [Algebra F E] [Algebra L E] [IsScalarTower F L E] [Algebra.IsSeparable F E] :

        Alias of Algebra.isSeparable_tower_top_of_isSeparable.

        theorem isSeparable_algebraMap {F : Type u_1} [Field F] {K : Type u_2} [Ring K] [Algebra F K] (x : F) :
        Equations
        • =
        theorem IsSeparable.of_integral (F : Type u_1) [Field F] {K : Type u_2} [Ring K] [Algebra F K] [IsDomain K] [Algebra.IsIntegral F K] [CharZero F] (x : K) :
        @[instance 100]

        A integral field extension in characteristic 0 is separable.

        Equations
        • =
        theorem IsSeparable.tower_bot {F : Type u_1} [Field F] {K : Type u_2} {E : Type u_3} [Field K] [Ring E] [Algebra F K] [Algebra F E] [Algebra K E] [Nontrivial E] [IsScalarTower F K E] {x : K} (h : IsSeparable F ((algebraMap K E) x)) :

        If E / K / F is a scalar tower and algebraMap K E x is separable over F, then x is `` also separable over F.

        theorem Algebra.isSeparable_tower_bot_of_isSeparable (F : Type u_1) [Field F] (K : Type u_2) (E : Type u_3) [Field K] [Ring E] [Algebra F K] [Algebra F E] [Algebra K E] [Nontrivial E] [IsScalarTower F K E] [h : Algebra.IsSeparable F E] :
        theorem IsSeparable.of_algHom {F : Type u_1} [Field F] {E : Type u_3} {E' : Type u_4} [Field E] [Field E'] [Algebra F E] [Algebra F E'] (f : E →ₐ[F] E') {x : E} (h : IsSeparable F (f x)) :
        theorem Algebra.IsSeparable.of_algHom (F : Type u_1) [Field F] {E : Type u_3} (E' : Type u_4) [Field E] [Field E'] [Algebra F E] [Algebra F E'] (f : E →ₐ[F] E') [Algebra.IsSeparable F E'] :
        theorem IsSeparable.of_equiv_equiv {A₁ : Type u_1} {B₁ : Type u_2} {A₂ : Type u_3} {B₂ : Type u_4} [Field A₁] [Field B₁] [Field A₂] [Field B₂] [Algebra A₁ B₁] [Algebra A₂ B₂] (e₁ : A₁ ≃+* A₂) (e₂ : B₁ ≃+* B₂) (he : (algebraMap A₂ B₂).comp e₁ = (↑e₂).comp (algebraMap A₁ B₁)) {x : B₁} (h : IsSeparable A₁ x) :
        IsSeparable A₂ (e₂ x)
        theorem Algebra.IsSeparable.of_equiv_equiv {A₁ : Type u_1} {B₁ : Type u_2} {A₂ : Type u_3} {B₂ : Type u_4} [Field A₁] [Field B₁] [Field A₂] [Field B₂] [Algebra A₁ B₁] [Algebra A₂ B₂] (e₁ : A₁ ≃+* A₂) (e₂ : B₁ ≃+* B₂) (he : (algebraMap A₂ B₂).comp e₁ = (↑e₂).comp (algebraMap A₁ B₁)) [Algebra.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 : IsSeparable K pb.gen) (h_splits : Polynomial.Splits (algebraMap K L) (minpoly K pb.gen)) :
        Fintype.card (S →ₐ[K] L) = pb.dim