Documentation

Mathlib.FieldTheory.SeparableClosure

Separable closure #

This file contains basics about the (relative) separable closure of a field extension.

Main definitions #

Main results #

Tags #

separable degree, degree, separable closure

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

The (relative) separable closure of F in E, or called maximal separable subextension of E / F, is defined to be the intermediate field of E / F consisting of all separable elements. The previous results prove that these elements are closed under field operations.

Equations
  • separableClosure F E = { carrier := {x : E | IsSeparable F x}, mul_mem' := , one_mem' := , add_mem' := , zero_mem' := , algebraMap_mem' := , inv_mem' := }
Instances For
    theorem mem_separableClosure_iff {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {x : E} :

    An element is contained in the separable closure of F in E if and only if it is a separable element.

    theorem map_mem_separableClosure_iff {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) {x : E} :

    If i is an F-algebra homomorphism from E to K, then i x is contained in separableClosure F K if and only if x is contained in separableClosure F E.

    If i is an F-algebra homomorphism from E to K, then the preimage of separableClosure F K under the map i is equal to separableClosure F E.

    theorem separableClosure.map_le_of_algHom {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 i is an F-algebra homomorphism from E to K, then the image of separableClosure F E under the map i is contained in separableClosure F K.

    If K / E / F is a field extension tower, such that K / E has no non-trivial separable subextensions (when K / E is algebraic, this means that it is purely inseparable), then the image of separableClosure F E in K is equal to separableClosure F K.

    theorem separableClosure.map_eq_of_algEquiv {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 i is an F-algebra isomorphism of E and K, then the image of separableClosure F E under the map i is equal to separableClosure F K.

    def separableClosure.algEquivOfAlgEquiv {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 separableClosure F E and separableClosure F K are also isomorphic as F-algebras.

    Equations
    Instances For
      def AlgEquiv.separableClosure {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) :

      Alias of separableClosure.algEquivOfAlgEquiv.


      If E and K are isomorphic as F-algebras, then separableClosure F E and separableClosure F K are also isomorphic as F-algebras.

      Equations
      Instances For

        The separable closure of F in E is algebraic over F.

        Equations
        • =

        The separable closure of F in E is separable over F.

        Equations
        • =
        theorem le_separableClosure' (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] {L : IntermediateField F E} (hs : ∀ (x : L), IsSeparable F x) :

        An intermediate field of E / F is contained in the separable closure of F in E if all of its elements are separable over F.

        theorem le_separableClosure (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (L : IntermediateField F E) [Algebra.IsSeparable F L] :

        An intermediate field of E / F is contained in the separable closure of F in E if it is separable over F.

        theorem le_separableClosure_iff (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (L : IntermediateField F E) :

        An intermediate field of E / F is contained in the separable closure of F in E if and only if it is separable over F.

        The separable closure in E of the separable closure of F in E is equal to itself.

        The normal closure in E/F of the separable closure of F in E is equal to itself.

        instance separableClosure.isGalois (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [Normal F E] :

        If E is normal over F, then the separable closure of F in E is Galois (i.e. normal and separable) over F.

        Equations
        • =

        If E / F is a field extension and E is separably closed, then the separable closure of F in E is equal to F if and only if F is separably closed.

        instance separableClosure.isSepClosure (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [IsSepClosed E] :

        If E is separably closed, then the separable closure of F in E is an absolute separable closure of F.

        Equations
        • =
        @[reducible, inline]
        abbrev SeparableClosure (F : Type u) [Field F] :

        The absolute separable closure is defined to be the relative separable closure inside the algebraic closure. It is indeed a separable closure (IsSepClosure) by separableClosure.isSepClosure, and it is Galois (IsGalois) by separableClosure.isGalois or IsSepClosure.isGalois, and every separable extension embeds into it (IsSepClosed.lift).

        Equations
        Instances For

          F(S) / F is a separable extension if and only if all elements of S are separable elements.

          The separable closure of F in E is equal to E if and only if E / F is separable.

          If K / E / F is a field extension tower, then separableClosure F K is contained in separableClosure E K.

          If K / E / F is a field extension tower, such that E / F is separable, then separableClosure F K is equal to separableClosure E K.

          theorem separableClosure.adjoin_le (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] :

          If K / E / F is a field extension tower, then E adjoin separableClosure F K is contained in separableClosure E K.

          instance IntermediateField.isSeparable_sup (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (L1 : IntermediateField F E) (L2 : IntermediateField F E) [h1 : Algebra.IsSeparable F L1] [h2 : Algebra.IsSeparable F L2] :

          A compositum of two separable extensions is separable.

          Equations
          • =
          instance IntermediateField.isSeparable_iSup (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] {ι : Type u_1} {t : ιIntermediateField F E} [h : ∀ (i : ι), Algebra.IsSeparable F (t i)] :
          Algebra.IsSeparable F (⨆ (i : ι), t i)

          A compositum of separable extensions is separable.

          Equations
          • =
          def Field.sepDegree (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] :

          The (infinite) separable degree for a general field extension E / F is defined to be the degree of separableClosure F E / F.

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

            The (infinite) inseparable degree for a general field extension E / F is defined to be the degree of E / separableClosure F E.

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

              The finite inseparable degree for a general field extension E / F is defined to be the degree of E / separableClosure F E as a natural number. It is defined to be zero if such field extension is infinite.

              Equations
              Instances For
                theorem Field.finInsepDegree_def' (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] :
                Field.finInsepDegree F E = Cardinal.toNat (Field.insepDegree F E)
                instance Field.instNeZeroSepDegree (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] :
                Equations
                • =
                instance Field.instNeZeroInsepDegree (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] :
                Equations
                • =
                Equations
                • =

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

                theorem Field.sepDegree_eq_of_equiv (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type v) [Field K] [Algebra F K] (i : E ≃ₐ[F] K) :

                The same-universe version of Field.lift_sepDegree_eq_of_equiv.

                The separable degree multiplied by the inseparable degree is equal to the (infinite) field extension degree.

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

                theorem Field.insepDegree_eq_of_equiv (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type v) [Field K] [Algebra F K] (i : E ≃ₐ[F] K) :

                The same-universe version of Field.lift_insepDegree_eq_of_equiv.

                theorem Field.finInsepDegree_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 finite inseparable degree over F.

                @[simp]
                theorem Field.sepDegree_self (F : Type u) [Field F] :
                @[simp]
                @[simp]
                theorem IntermediateField.sepDegree_bot (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] :
                @[simp]
                theorem IntermediateField.insepDegree_bot (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] :
                @[simp]
                @[simp]
                @[simp]
                theorem IntermediateField.sepDegree_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] :
                @[simp]
                theorem IntermediateField.insepDegree_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] :
                @[simp]
                theorem IntermediateField.finInsepDegree_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] :
                @[simp]
                theorem IntermediateField.sepDegree_bot' {F : Type u} (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type v) [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] :
                @[simp]
                theorem IntermediateField.insepDegree_bot' {F : Type u} (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type v) [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] :

                A separable extension has separable degree equal to degree.

                A separable extension has inseparable degree one.

                A separable extension has finite inseparable degree one.