Documentation

Mathlib.FieldTheory.SeparableDegree

Separable degree #

This file contains basics about the separable degree of a field extension.

Main definitions #

Main results #

Tags #

separable degree, degree, polynomial

def Field.Emb (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] :

Field.Emb F E is the type of F-algebra homomorphisms from E to the algebraic closure of E.

Equations
Instances For
    def Field.finSepDegree (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] :

    If E / F is an algebraic extension, then the (finite) separable degree of E / F is the number of F-algebra homomorphisms from E to the algebraic closure of E, as a natural number. It is defined to be zero if there are infinitely many of them. Note that if E / F is not algebraic, then this definition makes no mathematical sense.

    Equations
    Instances For
      instance Field.instInhabitedEmb (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] :
      Equations
      Equations
      • =
      def Field.embEquivOfEquiv (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type w) [Field K] [Algebra F K] (i : E ≃ₐ[F] K) :

      A random bijection between Field.Emb F E and Field.Emb F K when E and K are isomorphic as F-algebras.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        theorem Field.finSepDegree_eq_of_equiv (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type w) [Field K] [Algebra F K] (i : E ≃ₐ[F] K) :

        If E and K are isomorphic as F-algebras, then they have the same Field.finSepDegree over F.

        @[simp]
        @[simp]
        theorem IntermediateField.finSepDegree_bot (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] :
        @[simp]
        theorem IntermediateField.finSepDegree_bot' {F : Type u} (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type w) [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] :
        @[simp]
        theorem IntermediateField.finSepDegree_top {F : Type u} (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type w) [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] :
        def Field.embEquivOfAdjoinSplits (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type w) [Field K] [Algebra F K] {S : Set E} (hS : IntermediateField.adjoin F S = ) (hK : sS, IsIntegral F s Polynomial.Splits (algebraMap F K) (minpoly F s)) :

        A random bijection between Field.Emb F E and E →ₐ[F] K if E = F(S) such that every element s of S is integral (= algebraic) over F and whose minimal polynomial splits in K. Combined with Field.instInhabitedEmb, it can be viewed as a stronger version of IntermediateField.nonempty_algHom_of_adjoin_splits.

        Equations
        Instances For
          theorem Field.finSepDegree_eq_of_adjoin_splits (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type w) [Field K] [Algebra F K] {S : Set E} (hS : IntermediateField.adjoin F S = ) (hK : sS, IsIntegral F s Polynomial.Splits (algebraMap F K) (minpoly F s)) :

          The Field.finSepDegree F E is equal to the cardinality of E →ₐ[F] K if E = F(S) such that every element s of S is integral (= algebraic) over F and whose minimal polynomial splits in K.

          def Field.embEquivOfIsAlgClosed (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type w) [Field K] [Algebra F K] [Algebra.IsAlgebraic F E] [IsAlgClosed K] :

          A random bijection between Field.Emb F E and E →ₐ[F] K when E / F is algebraic and K / F is algebraically closed.

          Equations
          Instances For

            The Field.finSepDegree F E is equal to the cardinality of E →ₐ[F] K as a natural number, when E / F is algebraic and K / F is algebraically closed.

            def Field.embProdEmbOfIsAlgebraic (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type w) [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] [Algebra.IsAlgebraic E K] :

            If K / E / F is a field extension tower, such that K / E is algebraic, then there is a non-canonical bijection Field.Emb F E × Field.Emb E K ≃ Field.Emb F K. A corollary of algHomEquivSigma.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              If K / E / F is a field extension tower, such that K / E is algebraic, then their separable degrees satisfy the tower law $[E:F]_s [K:E]_s = [K:F]_s$. See also FiniteDimensional.finrank_mul_finrank.

              The separable degree Polynomial.natSepDegree of a polynomial is a natural number, defined to be the number of distinct roots of it over its splitting field. This is similar to Polynomial.natDegree but not to Polynomial.degree, namely, the separable degree of 0 is 0, not negative infinity.

              Equations
              • f.natSepDegree = (f.aroots f.SplittingField).toFinset.card
              Instances For
                theorem Polynomial.natSepDegree_le_natDegree {F : Type u} [Field F] (f : Polynomial F) :
                f.natSepDegree f.natDegree

                The separable degree of a polynomial is smaller than its degree.

                @[simp]
                theorem Polynomial.natSepDegree_X_sub_C {F : Type u} [Field F] (x : F) :
                (Polynomial.X - Polynomial.C x).natSepDegree = 1
                @[simp]
                theorem Polynomial.natSepDegree_X {F : Type u} [Field F] :
                Polynomial.X.natSepDegree = 1
                theorem Polynomial.natSepDegree_eq_zero {F : Type u} [Field F] (f : Polynomial F) (h : f.natDegree = 0) :
                f.natSepDegree = 0

                A constant polynomial has zero separable degree.

                @[simp]
                theorem Polynomial.natSepDegree_C {F : Type u} [Field F] (x : F) :
                (Polynomial.C x).natSepDegree = 0
                theorem Polynomial.natSepDegree_ne_zero {F : Type u} [Field F] (f : Polynomial F) (h : f.natDegree 0) :
                f.natSepDegree 0

                A non-constant polynomial has non-zero separable degree.

                theorem Polynomial.natSepDegree_eq_zero_iff {F : Type u} [Field F] (f : Polynomial F) :
                f.natSepDegree = 0 f.natDegree = 0

                A polynomial has zero separable degree if and only if it is constant.

                theorem Polynomial.natSepDegree_ne_zero_iff {F : Type u} [Field F] (f : Polynomial F) :
                f.natSepDegree 0 f.natDegree 0

                A polynomial has non-zero separable degree if and only if it is non-constant.

                theorem Polynomial.natSepDegree_eq_natDegree_iff {F : Type u} [Field F] (f : Polynomial F) (hf : f 0) :
                f.natSepDegree = f.natDegree f.Separable

                The separable degree of a non-zero polynomial is equal to its degree if and only if it is separable.

                theorem Polynomial.natSepDegree_eq_natDegree_of_separable {F : Type u} [Field F] (f : Polynomial F) (h : f.Separable) :
                f.natSepDegree = f.natDegree

                If a polynomial is separable, then its separable degree is equal to its degree.

                theorem Polynomial.Separable.natSepDegree_eq_natDegree {F : Type u} [Field F] {f : Polynomial F} (h : f.Separable) :
                f.natSepDegree = f.natDegree

                Same as Polynomial.natSepDegree_eq_natDegree_of_separable, but enables the use of dot notation.

                theorem Polynomial.natSepDegree_eq_of_splits {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (f : Polynomial F) (h : Polynomial.Splits (algebraMap F E) f) :
                f.natSepDegree = (f.aroots E).toFinset.card

                If a polynomial splits over E, then its separable degree is equal to the number of distinct roots of it over E.

                theorem Polynomial.natSepDegree_eq_of_isAlgClosed {F : Type u} (E : Type v) [Field F] [Field E] [Algebra F E] (f : Polynomial F) [IsAlgClosed E] :
                f.natSepDegree = (f.aroots E).toFinset.card

                The separable degree of a polynomial is equal to the number of distinct roots of it over any algebraically closed field.

                theorem Polynomial.natSepDegree_map {F : Type u} (E : Type v) [Field F] [Field E] [Algebra F E] (f : Polynomial F) :
                (Polynomial.map (algebraMap F E) f).natSepDegree = f.natSepDegree
                @[simp]
                theorem Polynomial.natSepDegree_C_mul {F : Type u} [Field F] (f : Polynomial F) {x : F} (hx : x 0) :
                (Polynomial.C x * f).natSepDegree = f.natSepDegree
                @[simp]
                theorem Polynomial.natSepDegree_smul_nonzero {F : Type u} [Field F] (f : Polynomial F) {x : F} (hx : x 0) :
                (x f).natSepDegree = f.natSepDegree
                @[simp]
                theorem Polynomial.natSepDegree_pow {F : Type u} [Field F] (f : Polynomial F) {n : } :
                (f ^ n).natSepDegree = if n = 0 then 0 else f.natSepDegree
                theorem Polynomial.natSepDegree_pow_of_ne_zero {F : Type u} [Field F] (f : Polynomial F) {n : } (hn : n 0) :
                (f ^ n).natSepDegree = f.natSepDegree
                theorem Polynomial.natSepDegree_X_pow {F : Type u} [Field F] {n : } :
                (Polynomial.X ^ n).natSepDegree = if n = 0 then 0 else 1
                theorem Polynomial.natSepDegree_X_sub_C_pow {F : Type u} [Field F] {x : F} {n : } :
                ((Polynomial.X - Polynomial.C x) ^ n).natSepDegree = if n = 0 then 0 else 1
                theorem Polynomial.natSepDegree_C_mul_X_sub_C_pow {F : Type u} [Field F] {x : F} {y : F} {n : } (hx : x 0) :
                (Polynomial.C x * (Polynomial.X - Polynomial.C y) ^ n).natSepDegree = if n = 0 then 0 else 1
                theorem Polynomial.natSepDegree_mul {F : Type u} [Field F] (f : Polynomial F) (g : Polynomial F) :
                (f * g).natSepDegree f.natSepDegree + g.natSepDegree
                theorem Polynomial.natSepDegree_mul_eq_iff {F : Type u} [Field F] (f : Polynomial F) (g : Polynomial F) :
                (f * g).natSepDegree = f.natSepDegree + g.natSepDegree f = 0 g = 0 IsCoprime f g
                theorem Polynomial.natSepDegree_mul_of_isCoprime {F : Type u} [Field F] (f : Polynomial F) (g : Polynomial F) (hc : IsCoprime f g) :
                (f * g).natSepDegree = f.natSepDegree + g.natSepDegree
                theorem Polynomial.natSepDegree_le_of_dvd {F : Type u} [Field F] (f : Polynomial F) (g : Polynomial F) (h1 : f g) (h2 : g 0) :
                f.natSepDegree g.natSepDegree
                theorem Polynomial.natSepDegree_expand {F : Type u} [Field F] (f : Polynomial F) (q : ) [hF : ExpChar F q] {n : } :
                ((Polynomial.expand F (q ^ n)) f).natSepDegree = f.natSepDegree

                If a field F is of exponential characteristic q, then Polynomial.expand F (q ^ n) f and f have the same separable degree.

                theorem Polynomial.natSepDegree_X_pow_char_pow_sub_C {F : Type u} [Field F] (q : ) [ExpChar F q] (n : ) (y : F) :
                (Polynomial.X ^ q ^ n - Polynomial.C y).natSepDegree = 1
                theorem Polynomial.IsSeparableContraction.natSepDegree_eq {F : Type u} [Field F] {f : Polynomial F} {g : Polynomial F} {q : } [ExpChar F q] (h : Polynomial.IsSeparableContraction q f g) :
                f.natSepDegree = g.natDegree

                If g is a separable contraction of f, then the separable degree of f is equal to the degree of g.

                theorem Polynomial.HasSeparableContraction.natSepDegree_eq {F : Type u} [Field F] {f : Polynomial F} {q : } [ExpChar F q] (hf : Polynomial.HasSeparableContraction q f) :
                f.natSepDegree = hf.degree

                If a polynomial has separable contraction, then its separable degree is equal to the degree of the given separable contraction.

                theorem Irreducible.natSepDegree_dvd_natDegree {F : Type u} [Field F] {f : Polynomial F} (h : Irreducible f) :
                f.natSepDegree f.natDegree

                The separable degree of an irreducible polynomial divides its degree.

                theorem Irreducible.natSepDegree_eq_one_iff_of_monic' {F : Type u} [Field F] {f : Polynomial F} (q : ) [ExpChar F q] (hm : f.Monic) (hi : Irreducible f) :
                f.natSepDegree = 1 ∃ (n : ) (y : F), f = (Polynomial.expand F (q ^ n)) (Polynomial.X - Polynomial.C y)

                A monic irreducible polynomial over a field F of exponential characteristic q has separable degree one if and only if it is of the form Polynomial.expand F (q ^ n) (X - C y) for some n : ℕ and y : F.

                theorem Irreducible.natSepDegree_eq_one_iff_of_monic {F : Type u} [Field F] {f : Polynomial F} (q : ) [ExpChar F q] (hm : f.Monic) (hi : Irreducible f) :
                f.natSepDegree = 1 ∃ (n : ) (y : F), f = Polynomial.X ^ q ^ n - Polynomial.C y

                A monic irreducible polynomial over a field F of exponential characteristic q has separable degree one if and only if it is of the form X ^ (q ^ n) - C y for some n : ℕ and y : F.

                theorem Polynomial.Monic.natSepDegree_eq_one_iff_of_irreducible' {F : Type u} [Field F] {f : Polynomial F} (q : ) [ExpChar F q] (hm : f.Monic) (hi : Irreducible f) :
                f.natSepDegree = 1 ∃ (n : ) (y : F), f = (Polynomial.expand F (q ^ n)) (Polynomial.X - Polynomial.C y)

                Alias of Irreducible.natSepDegree_eq_one_iff_of_monic'.


                A monic irreducible polynomial over a field F of exponential characteristic q has separable degree one if and only if it is of the form Polynomial.expand F (q ^ n) (X - C y) for some n : ℕ and y : F.

                theorem Polynomial.Monic.natSepDegree_eq_one_iff_of_irreducible {F : Type u} [Field F] {f : Polynomial F} (q : ) [ExpChar F q] (hm : f.Monic) (hi : Irreducible f) :
                f.natSepDegree = 1 ∃ (n : ) (y : F), f = Polynomial.X ^ q ^ n - Polynomial.C y

                Alias of Irreducible.natSepDegree_eq_one_iff_of_monic.


                A monic irreducible polynomial over a field F of exponential characteristic q has separable degree one if and only if it is of the form X ^ (q ^ n) - C y for some n : ℕ and y : F.

                theorem Polynomial.Monic.eq_X_sub_C_pow_of_natSepDegree_eq_one_of_splits {F : Type u} [Field F] {f : Polynomial F} (hm : f.Monic) (hs : Polynomial.Splits (RingHom.id F) f) (h : f.natSepDegree = 1) :
                ∃ (m : ) (y : F), m 0 f = (Polynomial.X - Polynomial.C y) ^ m

                If a monic polynomial of separable degree one splits, then it is of form (X - C y) ^ m for some non-zero natural number m and some element y of F.

                theorem Polynomial.Monic.eq_X_pow_char_pow_sub_C_of_natSepDegree_eq_one_of_irreducible {F : Type u} [Field F] {f : Polynomial F} (q : ) [ExpChar F q] (hm : f.Monic) (hi : Irreducible f) (h : f.natSepDegree = 1) :
                ∃ (n : ) (y : F), (n = 0 y(frobenius F q).range) f = Polynomial.X ^ q ^ n - Polynomial.C y

                If a monic irreducible polynomial over a field F of exponential characteristic q has separable degree one, then it is of the form X ^ (q ^ n) - C y for some natural number n, and some element y of F, such that either n = 0 or y has no q-th root in F.

                theorem Polynomial.Monic.eq_X_pow_char_pow_sub_C_pow_of_natSepDegree_eq_one {F : Type u} [Field F] {f : Polynomial F} (q : ) [ExpChar F q] (hm : f.Monic) (h : f.natSepDegree = 1) :
                ∃ (m : ) (n : ) (y : F), m 0 (n = 0 y(frobenius F q).range) f = (Polynomial.X ^ q ^ n - Polynomial.C y) ^ m

                If a monic polynomial over a field F of exponential characteristic q has separable degree one, then it is of the form (X ^ (q ^ n) - C y) ^ m for some non-zero natural number m, some natural number n, and some element y of F, such that either n = 0 or y has no q-th root in F.

                theorem Polynomial.Monic.natSepDegree_eq_one_iff {F : Type u} [Field F] {f : Polynomial F} (q : ) [ExpChar F q] (hm : f.Monic) :
                f.natSepDegree = 1 ∃ (m : ) (n : ) (y : F), m 0 f = (Polynomial.X ^ q ^ n - Polynomial.C y) ^ m

                A monic polynomial over a field F of exponential characteristic q has separable degree one if and only if it is of the form (X ^ (q ^ n) - C y) ^ m for some non-zero natural number m, some natural number n, and some element y of F.

                theorem minpoly.natSepDegree_eq_one_iff_eq_expand_X_sub_C {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (q : ) [hF : ExpChar F q] {x : E} :
                (minpoly F x).natSepDegree = 1 ∃ (n : ) (y : F), minpoly F x = (Polynomial.expand F (q ^ n)) (Polynomial.X - Polynomial.C y)

                The minimal polynomial of an element of E / F of exponential characteristic q has separable degree one if and only if the minimal polynomial is of the form Polynomial.expand F (q ^ n) (X - C y) for some n : ℕ and y : F.

                theorem minpoly.natSepDegree_eq_one_iff_eq_X_pow_sub_C {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (q : ) [hF : ExpChar F q] {x : E} :
                (minpoly F x).natSepDegree = 1 ∃ (n : ) (y : F), minpoly F x = Polynomial.X ^ q ^ n - Polynomial.C y

                The minimal polynomial of an element of E / F of exponential characteristic q has separable degree one if and only if the minimal polynomial is of the form X ^ (q ^ n) - C y for some n : ℕ and y : F.

                theorem minpoly.natSepDegree_eq_one_iff_pow_mem {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (q : ) [hF : ExpChar F q] {x : E} :
                (minpoly F x).natSepDegree = 1 ∃ (n : ), x ^ q ^ n (algebraMap F E).range

                The minimal polynomial of an element x of E / F of exponential characteristic q has separable degree one if and only if x ^ (q ^ n) ∈ F for some n : ℕ.

                theorem minpoly.natSepDegree_eq_one_iff_eq_X_sub_C_pow {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (q : ) [hF : ExpChar F q] {x : E} :
                (minpoly F x).natSepDegree = 1 ∃ (n : ), Polynomial.map (algebraMap F E) (minpoly F x) = (Polynomial.X - Polynomial.C x) ^ q ^ n

                The minimal polynomial of an element x of E / F of exponential characteristic q has separable degree one if and only if the minimal polynomial is of the form (X - x) ^ (q ^ n) for some n : ℕ.

                theorem IntermediateField.finSepDegree_adjoin_simple_eq_natSepDegree (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] {α : E} (halg : IsAlgebraic F α) :
                Field.finSepDegree F Fα = (minpoly F α).natSepDegree

                The separable degree of F⟮α⟯ / F is equal to the separable degree of the minimal polynomial of α over F.

                theorem IntermediateField.finSepDegree_adjoin_simple_le_finrank (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (α : E) (halg : IsAlgebraic F α) :
                Field.finSepDegree F Fα FiniteDimensional.finrank F Fα

                The separable degree of F⟮α⟯ / F is smaller than the degree of F⟮α⟯ / F if α is algebraic over F.

                theorem IntermediateField.finSepDegree_adjoin_simple_eq_finrank_iff (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (α : E) (halg : IsAlgebraic F α) :
                Field.finSepDegree F Fα = FiniteDimensional.finrank F Fα IsSeparable F α

                If α is algebraic over F, then the separable degree of F⟮α⟯ / F is equal to the degree of F⟮α⟯ / F if and only if α is a separable element.

                The separable degree of any field extension E / F divides the degree of E / F.

                The separable degree of a finite extension E / F is smaller than the degree of E / F.

                If E / F is a separable extension, then its separable degree is equal to its degree. When E / F is infinite, it means that Field.Emb F E has infinitely many elements. (But the cardinality of Field.Emb F E is not equal to Module.rank F E in general!)

                Alias of Field.finSepDegree_eq_finrank_of_isSeparable.


                If E / F is a separable extension, then its separable degree is equal to its degree. When E / F is infinite, it means that Field.Emb F E has infinitely many elements. (But the cardinality of Field.Emb F E is not equal to Module.rank F E in general!)

                If E / F is a finite extension, then its separable degree is equal to its degree if and only if it is a separable extension.

                theorem IntermediateField.isSeparable_of_mem_isSeparable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] {L : IntermediateField F E} [Algebra.IsSeparable F L] {x : E} (h : x L) :

                F⟮x⟯ / F is a separable extension if and only if x is a separable element. As a consequence, any rational function of x is also a separable element.

                theorem IsSeparable.of_algebra_isSeparable_of_isSeparable (F : Type u) {E : Type v} [Field F] [Field E] [Algebra F E] {K : Type w} [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] [Algebra.IsSeparable F E] {x : K} (hsep : IsSeparable E x) :

                If K / E / F is an extension tower such that E / F is separable, x : K is separable over E, then it's also separable over F.

                theorem Algebra.IsSeparable.trans (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type w) [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] [Algebra.IsSeparable F E] [Algebra.IsSeparable E K] :

                If E / F and K / E are both separable extensions, then K / F is also separable.

                theorem IntermediateField.isSeparable_adjoin_pair_of_isSeparable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] {x : E} {y : E} (hx : IsSeparable F x) (hy : IsSeparable F y) :
                Algebra.IsSeparable F Fx, y

                If x and y are both separable elements, then F⟮x, y⟯ / F is a separable extension. As a consequence, any rational function of x and y is also a separable element.

                theorem Field.isSeparable_algebraMap {F : Type u} (E : Type v) [Field F] [Field E] [Algebra F E] (x : F) :

                Any element x of F is a separable element of E / F when embedded into E.

                theorem Field.isSeparable_mul {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {x : E} {y : E} (hx : IsSeparable F x) (hy : IsSeparable F y) :
                IsSeparable F (x * y)

                If x and y are both separable elements, then x * y is also a separable element.

                theorem Field.isSeparable_add {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {x : E} {y : E} (hx : IsSeparable F x) (hy : IsSeparable F y) :
                IsSeparable F (x + y)

                If x and y are both separable elements, then x + y is also a separable element.

                theorem Field.isSeparable_inv {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {x : E} (hx : IsSeparable F x) :

                If x is a separable element, then x⁻¹ is also a separable element.

                theorem perfectField_iff_splits_of_natSepDegree_eq_one (F : Type u_1) [Field F] :
                PerfectField F ∀ (f : Polynomial F), f.natSepDegree = 1Polynomial.Splits (RingHom.id F) f

                A field is a perfect field (which means that any irreducible polynomial is separable) if and only if every separable degree one polynomial splits.