Documentation

Mathlib.FieldTheory.Galois.Basic

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.

Stacks Tag 09I0

Instances
    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] :
    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] :

    Let E be a field. Let G be a finite group acting on E. Then the extension E/EG is Galois.

    Stacks Tag 09I3 (first part)

    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 Fα) (minpoly F α)) :
    Fintype.card (Fα ≃ₐ[F] Fα) = Module.finrank F Fα
    theorem IsGalois.card_aut_eq_finrank (F : Type u_1) [Field F] (E : Type u_2) [Field E] [Algebra F E] [FiniteDimensional F E] [IsGalois F E] :

    Let E/F be a finite extension of fields. If E is Galois over F, then |Aut(E/F)|=[E:F].

    Stacks Tag 09I1 ('only if' part)

    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] :

    Let E/K/F be a tower of field extensions. If E is Galois over F, then E is Galois over K.

    Stacks Tag 09I2

    @[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 (↥K) E
    theorem isGalois_iff_isGalois_bot {F : Type u_1} {E : Type u_3} [Field F] [Field E] [Algebra 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] :
    instance isGalois_bot {F : Type u_1} {E : Type u_3} [Field F] [Field E] [Algebra F E] :
    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
    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
    theorem IntermediateField.mem_fixedField_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (H : Subgroup (E ≃ₐ[F] E)) (x : E) :
    x fixedField H fH, f x = x
    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
    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) :
    def IntermediateField.fixingSubgroupEquiv {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F 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.
    instance IntermediateField.fixedField.smul {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) :
    Equations
    instance IntermediateField.fixedField.algebra {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) :
    Equations

    The Galois correspondence from intermediate fields to subgroups.

    Stacks Tag 09DW

    Equations

    The Galois correspondence as a GaloisInsertion

    Equations
    • One or more equations did not get rendered due to their size.
    instance IsGalois.of_fixedField_normal_subgroup {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] [IsGalois K L] (H : Subgroup (L ≃ₐ[K] L)) [hn : H.Normal] :

    If H is a normal Subgroup of Gal(L / K), then fixedField H is Galois over K.

    noncomputable def IsGalois.normalAutEquivQuotient {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (H : Subgroup (L ≃ₐ[K] L)) [H.Normal] :

    If H is a normal Subgroup of Gal(L / K), then Gal(fixedField H / K) is isomorphic to Gal(L / K) ⧸ H.

    Equations
    @[simp]
    theorem IsGalois.map_fixingSubgroup {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (E : IntermediateField K L) (σ : L ≃ₐ[K] L) :
    instance IsGalois.fixingSubgroup_normal_of_isGalois {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (E : IntermediateField K L) [IsGalois K L] [IsGalois K E] :

    Let E be an intermediateField of a Galois extension L / K. If E / K is Galois extension, then E.fixingSubgroup is a normal subgroup of Gal(L / K).

    theorem IsGalois.of_card_aut_eq_finrank (F : Type u_1) [Field F] (E : Type u_2) [Field E] [Algebra F E] [FiniteDimensional F E] (h : Fintype.card (E ≃ₐ[F] E) = Module.finrank F E) :

    Let E/F be a finite extension of fields. If |Aut(E/F)|=[E:F], then E is Galois over F.

    Stacks Tag 09I1 ('if' part)

    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 ((IntermediateField.restrictScalars F Kx) →ₐ[F] E)] :
    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) :

    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] :

    Let F/K/k be a tower of field extensions. If F is Galois over k, then the normal closure of K over k in F is Galois over k.

    Stacks Tag 0EXM

    @[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] :