Documentation

Mathlib.FieldTheory.NormalClosure

Normal closures #

Main definitions #

Given field extensions K/F and L/F, the predicate IsNormalClosure F K L says that the minimal polynomial of every element of K over F splits in L, and that L is generated by the roots of such minimal polynomials. These conditions uniquely characterize L/F up to F-algebra isomorphisms (IsNormalClosure.equiv).

The explicit construction normalClosure F K L of a field extension K/F inside another field extension L/F is the smallest intermediate field of L/F that contains the image of every F-algebra embedding K →ₐ[F] L. It satisfies the IsNormalClosure predicate if L/F satisfies the abovementioned splitting condition, in particular if L/K/F form a tower and L/F is normal.

class IsNormalClosure (F : Type u_1) (K : Type u_2) (L : Type u_3) [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] :

L/F is a normal closure of K/F if the minimal polynomial of every element of K over F splits in L, and L is generated by roots of such minimal polynomials over F. (Since the minimal polynomial of a transcendental element is 0, the normal closure of K/F is the same as the normal closure over F of the algebraic closure of F in K.)

Instances
    theorem IsNormalClosure.splits {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [self : IsNormalClosure F K L] (x : K) :
    theorem IsNormalClosure.adjoin_rootSet {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [self : IsNormalClosure F K L] :
    ⨆ (x : K), IntermediateField.adjoin F ((minpoly F x).rootSet L) =
    noncomputable def normalClosure (F : Type u_1) (K : Type u_2) (L : Type u_3) [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] :

    The normal closure of K/F in L/F.

    Equations
    Instances For
      theorem normalClosure_def (F : Type u_1) (K : Type u_2) (L : Type u_3) [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] :
      normalClosure F K L = ⨆ (f : K →ₐ[F] L), f.fieldRange
      theorem IsNormalClosure.normal {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [h : IsNormalClosure F K L] :
      Normal F L

      A normal closure is always normal.

      theorem normalClosure_le_iff {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] {K' : IntermediateField F L} :
      normalClosure F K L K' ∀ (f : K →ₐ[F] L), f.fieldRange K'
      theorem AlgHom.fieldRange_le_normalClosure {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] (f : K →ₐ[F] L) :
      f.fieldRange normalClosure F K L
      theorem Algebra.IsAlgebraic.normalClosure_le_iSup_adjoin {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [Algebra.IsAlgebraic F K] :
      normalClosure F K L ⨆ (x : K), IntermediateField.adjoin F ((minpoly F x).rootSet L)
      theorem Algebra.IsAlgebraic.normalClosure_eq_iSup_adjoin_of_splits {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [Algebra.IsAlgebraic F K] (splits : ∀ (x : K), Polynomial.Splits (algebraMap F L) (minpoly F x)) :
      normalClosure F K L = ⨆ (x : K), IntermediateField.adjoin F ((minpoly F x).rootSet L)
      theorem Algebra.IsAlgebraic.isNormalClosure_iff {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [Algebra.IsAlgebraic F K] :

      If K/F is algebraic, the "generated by roots" condition in IsNormalClosure can be replaced by "generated by images of embeddings".

      theorem Algebra.IsAlgebraic.isNormalClosure_normalClosure {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [Algebra.IsAlgebraic F K] (splits : ∀ (x : K), Polynomial.Splits (algebraMap F L) (minpoly F x)) :

      normalClosure F K L is a valid normal closure if K/F is algebraic and all minimal polynomials of K/F splits in L/F.

      noncomputable def IsNormalClosure.lift {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [h : IsNormalClosure F K L] {L' : Type u_4} [Field L'] [Algebra F L'] (splits : ∀ (x : K), Polynomial.Splits (algebraMap F L') (minpoly F x)) :
      L →ₐ[F] L'

      A normal closure of K/F embeds into any L/F where the minimal polynomials of K/F splits.

      Equations
      Instances For
        noncomputable def IsNormalClosure.equiv {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] {L' : Type u_4} [Field L'] [Algebra F L'] [h : IsNormalClosure F K L] [h' : IsNormalClosure F K L'] :
        L ≃ₐ[F] L'

        Normal closures of K/F are unique up to F-algebra isomorphisms.

        Equations
        Instances For
          instance isNormalClosure_normalClosure (F : Type u_1) (K : Type u_2) (L : Type u_3) [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [ne : Nonempty (K →ₐ[F] L)] [h : Normal F L] :
          Equations
          • =
          theorem normalClosure_eq_iSup_adjoin' (F : Type u_1) (K : Type u_2) (L : Type u_3) [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [ne : Nonempty (K →ₐ[F] L)] [h : Normal F L] :
          normalClosure F K L = ⨆ (x : K), IntermediateField.adjoin F ((minpoly F x).rootSet L)
          theorem normalClosure_eq_iSup_adjoin (F : Type u_1) (K : Type u_2) (L : Type u_3) [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [Algebra K L] [IsScalarTower F K L] [Normal F L] :
          normalClosure F K L = ⨆ (x : K), IntermediateField.adjoin F ((minpoly F x).rootSet L)
          noncomputable def normalClosure.algHomEquiv (F : Type u_1) (K : Type u_2) (L : Type u_3) [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] :
          (K →ₐ[F] (normalClosure F K L)) (K →ₐ[F] L)

          All F-AlgHoms from K to L factor through the normal closure of K/F in L/F.

          Equations
          Instances For
            instance normalClosure.normal (F : Type u_1) (K : Type u_2) (L : Type u_3) [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [h : Normal F L] :
            Normal F (normalClosure F K L)
            Equations
            • =
            instance normalClosure.is_finiteDimensional (F : Type u_1) (K : Type u_2) (L : Type u_3) [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [FiniteDimensional F K] :
            Equations
            • =
            noncomputable instance normalClosure.algebra (F : Type u_1) (K : Type u_2) (L : Type u_3) [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [Algebra K L] [IsScalarTower F K L] :
            Algebra K (normalClosure F K L)
            Equations
            • normalClosure.algebra F K L = (let __src := ⨆ (f : K →ₐ[F] L), f.fieldRange; { toSubsemiring := __src.toSubsemiring, algebraMap_mem' := , inv_mem' := }).algebra
            instance normalClosure.instIsScalarTowerSubtypeMemIntermediateField (F : Type u_1) (K : Type u_2) (L : Type u_3) [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [Algebra K L] [IsScalarTower F K L] :
            Equations
            • =
            instance normalClosure.instIsScalarTowerSubtypeMemIntermediateField_1 (F : Type u_1) (K : Type u_2) (L : Type u_3) [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [Algebra K L] [IsScalarTower F K L] :
            IsScalarTower K ((normalClosure F K L)) L
            Equations
            • =
            theorem normalClosure.restrictScalars_eq (F : Type u_1) (K : Type u_2) (L : Type u_3) [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [Algebra K L] [IsScalarTower F K L] :
            noncomputable def Algebra.IsAlgebraic.algHomEmbeddingOfSplits {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [Algebra.IsAlgebraic F K] (h : ∀ (x : K), Polynomial.Splits (algebraMap F L) (minpoly F x)) (L' : Type u_4) [Field L'] [Algebra F L'] :
            (K →ₐ[F] L') K →ₐ[F] L

            An extension L/F in which every minimal polynomial of K/F splits is maximal with respect to F-embeddings of K, in the sense that K →ₐ[F] L achieves maximal cardinality. We construct an explicit injective function from an arbitrary K →ₐ[F] L' into K →ₐ[F] L, using an embedding of normalClosure F K L' into L.

            Equations
            Instances For
              theorem IntermediateField.le_normalClosure {F : Type u_1} {L : Type u_3} [Field F] [Field L] [Algebra F L] (K : IntermediateField F L) :
              K normalClosure F (K) L
              theorem IntermediateField.normalClosure_of_normal {F : Type u_1} {L : Type u_3} [Field F] [Field L] [Algebra F L] (K : IntermediateField F L) [Normal F K] :
              normalClosure F (K) L = K
              theorem IntermediateField.normalClosure_def' {F : Type u_1} {L : Type u_3} [Field F] [Field L] [Algebra F L] (K : IntermediateField F L) [Normal F L] :
              normalClosure F (K) L = ⨆ (f : L →ₐ[F] L), IntermediateField.map f K
              theorem IntermediateField.normalClosure_def'' {F : Type u_1} {L : Type u_3} [Field F] [Field L] [Algebra F L] (K : IntermediateField F L) [Normal F L] :
              normalClosure F (K) L = ⨆ (f : L ≃ₐ[F] L), IntermediateField.map (f) K
              theorem IntermediateField.normalClosure_mono {F : Type u_1} {L : Type u_3} [Field F] [Field L] [Algebra F L] (K : IntermediateField F L) (K' : IntermediateField F L) [Normal F L] (h : K K') :
              normalClosure F (K) L normalClosure F (K') L
              @[simp]
              @[simp]
              theorem IntermediateField.closureOperator_isClosed (F : Type u_1) (L : Type u_3) [Field F] [Field L] [Algebra F L] [Normal F L] (x : IntermediateField F L) :
              (IntermediateField.closureOperator F L).IsClosed x = (normalClosure F (x) L = x)
              noncomputable def IntermediateField.closureOperator (F : Type u_1) (L : Type u_3) [Field F] [Field L] [Algebra F L] [Normal F L] :

              normalClosure as a ClosureOperator.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                theorem IntermediateField.normal_iff_normalClosure_eq {F : Type u_1} {L : Type u_3} [Field F] [Field L] [Algebra F L] [Normal F L] {K : IntermediateField F L} :
                Normal F K normalClosure F (K) L = K
                theorem IntermediateField.normal_iff_normalClosure_le {F : Type u_1} {L : Type u_3} [Field F] [Field L] [Algebra F L] [Normal F L] {K : IntermediateField F L} :
                Normal F K normalClosure F (K) L K
                theorem IntermediateField.normal_iff_forall_fieldRange_le {F : Type u_1} {L : Type u_3} [Field F] [Field L] [Algebra F L] [Normal F L] {K : IntermediateField F L} :
                Normal F K ∀ (σ : K →ₐ[F] L), σ.fieldRange K
                theorem IntermediateField.normal_iff_forall_map_le {F : Type u_1} {L : Type u_3} [Field F] [Field L] [Algebra F L] [Normal F L] {K : IntermediateField F L} :
                Normal F K ∀ (σ : L →ₐ[F] L), IntermediateField.map σ K K
                theorem IntermediateField.normal_iff_forall_map_le' {F : Type u_1} {L : Type u_3} [Field F] [Field L] [Algebra F L] [Normal F L] {K : IntermediateField F L} :
                Normal F K ∀ (σ : L ≃ₐ[F] L), IntermediateField.map (σ) K K
                theorem IntermediateField.normal_iff_forall_fieldRange_eq {F : Type u_1} {L : Type u_3} [Field F] [Field L] [Algebra F L] [Normal F L] {K : IntermediateField F L} :
                Normal F K ∀ (σ : K →ₐ[F] L), σ.fieldRange = K
                theorem IntermediateField.normal_iff_forall_map_eq {F : Type u_1} {L : Type u_3} [Field F] [Field L] [Algebra F L] [Normal F L] {K : IntermediateField F L} :
                Normal F K ∀ (σ : L →ₐ[F] L), IntermediateField.map σ K = K
                theorem IntermediateField.normal_iff_forall_map_eq' {F : Type u_1} {L : Type u_3} [Field F] [Field L] [Algebra F L] [Normal F L] {K : IntermediateField F L} :
                Normal F K ∀ (σ : L ≃ₐ[F] L), IntermediateField.map (σ) K = K