Documentation

Mathlib.FieldTheory.Galois

Galois Extensions #

In this file we define Galois extensions as extensions which are both separable and normal.

Main definitions #

Main results #

Together, these two results prove the Galois correspondence.

class IsGalois (F : Type u_1) [Field F] (E : Type u_2) [Field E] [Algebra F E] :

A field extension E/F is Galois if it is both separable and normal. Note that in mathlib a separable extension of fields is by definition algebraic.

Instances
    theorem IsGalois.to_isSeparable {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] [self : IsGalois F E] :
    theorem IsGalois.to_normal {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] [self : IsGalois F E] :
    Normal F E
    theorem isGalois_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
    instance IsGalois.self (F : Type u_1) [Field F] :
    Equations
    • =
    theorem IsGalois.integral (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] [IsGalois F E] (x : E) :
    theorem IsGalois.separable (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] [IsGalois F E] (x : E) :
    theorem IsGalois.splits (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] [IsGalois F E] (x : E) :
    instance IsGalois.of_fixed_field (E : Type u_2) [Field E] (G : Type u_3) [Group G] [Finite G] [MulSemiringAction G E] :
    IsGalois { x : E // x FixedPoints.subfield G E } E
    Equations
    • =
    theorem IsGalois.IntermediateField.AdjoinSimple.card_aut_eq_finrank (F : Type u_1) [Field F] (E : Type u_2) [Field E] [Algebra F E] [FiniteDimensional F E] {α : E} (hα : IsIntegral F α) (h_sep : IsSeparable F α) (h_splits : Polynomial.Splits (algebraMap F { x : E // x Fα }) (minpoly F α)) :
    Fintype.card ({ x : E // x Fα } ≃ₐ[F] { x : E // x Fα }) = FiniteDimensional.finrank F { x : E // x Fα }
    theorem IsGalois.tower_top_of_isGalois (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] [IsGalois F E] :
    @[instance 100]
    instance IsGalois.tower_top_intermediateField {F : Type u_1} {E : Type u_3} [Field F] [Field E] [Algebra F E] (K : IntermediateField F E) [IsGalois F E] :
    IsGalois { x : E // x K } E
    Equations
    • =
    theorem isGalois_iff_isGalois_bot {F : Type u_1} {E : Type u_3} [Field F] [Field E] [Algebra F E] :
    IsGalois { x : E // x } E IsGalois F E
    theorem IsGalois.of_algEquiv {F : Type u_1} {E : Type u_3} [Field F] [Field E] {E' : Type u_4} [Field E'] [Algebra F E'] [Algebra F E] [IsGalois F E] (f : E ≃ₐ[F] E') :
    theorem AlgEquiv.transfer_galois {F : Type u_1} {E : Type u_3} [Field F] [Field E] {E' : Type u_4} [Field E'] [Algebra F E'] [Algebra F E] (f : E ≃ₐ[F] E') :
    theorem isGalois_iff_isGalois_top {F : Type u_1} {E : Type u_3} [Field F] [Field E] [Algebra F E] :
    IsGalois F { x : E // x } IsGalois F E
    instance isGalois_bot {F : Type u_1} {E : Type u_3} [Field F] [Field E] [Algebra F E] :
    IsGalois F { x : E // x }
    Equations
    • =
    def FixedPoints.intermediateField {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (M : Type u_3) [Monoid M] [MulSemiringAction M E] [SMulCommClass M F E] :

    The intermediate field of fixed points fixed by a monoid action that commutes with the F-action on E.

    Equations
    Instances For
      def IntermediateField.fixedField {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (H : Subgroup (E ≃ₐ[F] E)) :

      The intermediate field fixed by a subgroup

      Equations
      Instances For
        theorem IntermediateField.finrank_fixedField_eq_card {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (H : Subgroup (E ≃ₐ[F] E)) [FiniteDimensional F E] [DecidablePred fun (x : E ≃ₐ[F] E) => x H] :
        def IntermediateField.fixingSubgroup {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) :

        The subgroup fixing an intermediate field

        Equations
        Instances For
          theorem IntermediateField.le_iff_le {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (H : Subgroup (E ≃ₐ[F] E)) (K : IntermediateField F E) :
          K IntermediateField.fixedField H H K.fixingSubgroup
          def IntermediateField.fixingSubgroupEquiv {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) :
          { x : E ≃ₐ[F] E // x K.fixingSubgroup } ≃* E ≃ₐ[{ x : E // x K }] E

          The fixing subgroup of K : IntermediateField F E is isomorphic to E ≃ₐ[K] E

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            theorem IntermediateField.fixingSubgroup_fixedField {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (H : Subgroup (E ≃ₐ[F] E)) [FiniteDimensional F E] :
            (IntermediateField.fixedField H).fixingSubgroup = H
            instance IntermediateField.fixedField.smul {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) :
            SMul { x : E // x K } { x : E // x IntermediateField.fixedField K.fixingSubgroup }
            Equations
            instance IntermediateField.fixedField.algebra {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) :
            Algebra { x : E // x K } { x : E // x IntermediateField.fixedField K.fixingSubgroup }
            Equations
            instance IntermediateField.fixedField.isScalarTower {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) :
            IsScalarTower { x : E // x K } { x : E // x IntermediateField.fixedField K.fixingSubgroup } E
            Equations
            • =
            theorem IsGalois.fixedField_fixingSubgroup {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) [FiniteDimensional F E] [h : IsGalois F E] :
            IntermediateField.fixedField K.fixingSubgroup = K
            theorem IsGalois.card_fixingSubgroup_eq_finrank {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) [DecidablePred fun (x : E ≃ₐ[F] E) => x K.fixingSubgroup] [FiniteDimensional F E] [IsGalois F E] :
            Fintype.card { x : E ≃ₐ[F] E // x K.fixingSubgroup } = FiniteDimensional.finrank { x : E // x K } E

            The Galois correspondence from intermediate fields to subgroups

            Equations
            • IsGalois.intermediateFieldEquivSubgroup = { toFun := IntermediateField.fixingSubgroup, invFun := IntermediateField.fixedField, left_inv := , right_inv := , map_rel_iff' := }
            Instances For
              def IsGalois.galoisInsertionIntermediateFieldSubgroup {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] [FiniteDimensional F E] :
              GaloisInsertion (OrderDual.toDual IntermediateField.fixingSubgroup) (IntermediateField.fixedField OrderDual.toDual)

              The Galois correspondence as a GaloisInsertion

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                def IsGalois.galoisCoinsertionIntermediateFieldSubgroup {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] [FiniteDimensional F E] [IsGalois F E] :
                GaloisCoinsertion (OrderDual.toDual IntermediateField.fixingSubgroup) (IntermediateField.fixedField OrderDual.toDual)

                The Galois correspondence as a GaloisCoinsertion

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  theorem IsGalois.is_separable_splitting_field (F : Type u_1) [Field F] (E : Type u_2) [Field E] [Algebra F E] [FiniteDimensional F E] [IsGalois F E] :
                  ∃ (p : Polynomial F), p.Separable Polynomial.IsSplittingField F E p
                  theorem IsGalois.of_separable_splitting_field_aux {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {p : Polynomial F} [hFE : FiniteDimensional F E] [sp : Polynomial.IsSplittingField F E p] (hp : p.Separable) (K : Type u_3) [Field K] [Algebra F K] [Algebra K E] [IsScalarTower F K E] {x : E} (hx : x p.aroots E) [Fintype (K →ₐ[F] E)] [Fintype ({ x_1 : E // x_1 IntermediateField.restrictScalars F Kx } →ₐ[F] E)] :
                  Fintype.card ({ x_1 : E // x_1 IntermediateField.restrictScalars F Kx } →ₐ[F] E) = Fintype.card (K →ₐ[F] E) * FiniteDimensional.finrank K { x_1 : E // x_1 Kx }
                  theorem IsGalois.of_separable_splitting_field {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {p : Polynomial F} [sp : Polynomial.IsSplittingField F E p] (hp : p.Separable) :
                  theorem IsGalois.tfae {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] [FiniteDimensional F E] :

                  Equivalent characterizations of a Galois extension of finite degree

                  instance IsGalois.normalClosure (k : Type u_1) (K : Type u_2) (F : Type u_3) [Field k] [Field K] [Field F] [Algebra k K] [Algebra k F] [IsGalois k F] :
                  IsGalois k { x : F // x normalClosure k K F }
                  Equations
                  • =
                  @[instance 100]
                  instance IsAlgClosure.isGalois (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [IsAlgClosure k K] [CharZero k] :
                  Equations
                  • =