Galois Extensions #

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

Main definitions #

• IsGalois F E where E is an extension of F
• fixedField H where H : Subgroup (E ≃ₐ[F] E)
• fixingSubgroup K where K : IntermediateField F E
• intermediateFieldEquivSubgroup where E/F is finite dimensional and Galois

Main results #

• IntermediateField.fixingSubgroup_fixedField : If E/F is finite dimensional (but not necessarily Galois) then fixingSubgroup (fixedField H) = H
• IntermediateField.fixedField_fixingSubgroup: If E/F is finite dimensional and Galois then fixedField (fixingSubgroup K) = K

Together, these two results prove the Galois correspondence.

• IsGalois.tfae : Equivalent characterizations of a Galois extension of finite degree
class IsGalois (F : Type u_1) [] (E : Type u_2) [] [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.

• to_isSeparable :
• to_normal : Normal F E
Instances
theorem IsGalois.to_isSeparable {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] [self : IsGalois F E] :
theorem IsGalois.to_normal {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] [self : IsGalois F E] :
Normal F E
theorem isGalois_iff {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] :
instance IsGalois.self (F : Type u_1) [] :
Equations
• =
theorem IsGalois.integral (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] [IsGalois F E] (x : E) :
theorem IsGalois.separable (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] [IsGalois F E] (x : E) :
theorem IsGalois.splits (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] [IsGalois F E] (x : E) :
instance IsGalois.of_fixed_field (E : Type u_2) [] (G : Type u_3) [] [] [] :
IsGalois (()) E
Equations
• =
theorem IsGalois.IntermediateField.AdjoinSimple.card_aut_eq_finrank (F : Type u_1) [] (E : Type u_2) [] [Algebra F E] [] {α : E} (hα : ) (h_sep : ) (h_splits : Polynomial.Splits (algebraMap F Fα) (minpoly F α)) :
Fintype.card (Fα ≃ₐ[F] Fα) =
theorem IsGalois.card_aut_eq_finrank (F : Type u_1) [] (E : Type u_2) [] [Algebra F E] [] [IsGalois F E] :
theorem IsGalois.tower_top_of_isGalois (F : Type u_1) (K : Type u_2) (E : Type u_3) [] [] [] [Algebra F K] [Algebra F E] [Algebra K E] [] [IsGalois F E] :
@[instance 100]
instance IsGalois.tower_top_intermediateField {F : Type u_1} {E : Type u_3} [] [] [Algebra F E] (K : ) [IsGalois F E] :
IsGalois (K) E
Equations
• =
theorem isGalois_iff_isGalois_bot {F : Type u_1} {E : Type u_3} [] [] [Algebra F E] :
theorem IsGalois.of_algEquiv {F : Type u_1} {E : Type u_3} [] [] {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} [] [] {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} [] [] [Algebra F E] :
instance isGalois_bot {F : Type u_1} {E : Type u_3} [] [] [Algebra F E] :
Equations
• =
def FixedPoints.intermediateField {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] (M : Type u_3) [] [] [] :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def IntermediateField.fixedField {F : Type u_1} [] {E : Type u_2} [] [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} [] {E : Type u_2} [] [Algebra F E] (H : Subgroup (E ≃ₐ[F] E)) [] [DecidablePred fun (x : E ≃ₐ[F] E) => x H] :
def IntermediateField.fixingSubgroup {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] (K : ) :

The subgroup fixing an intermediate field

Equations
Instances For
theorem IntermediateField.le_iff_le {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] (H : Subgroup (E ≃ₐ[F] E)) (K : ) :
H K.fixingSubgroup
def IntermediateField.fixingSubgroupEquiv {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] (K : ) :
K.fixingSubgroup ≃* E ≃ₐ[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} [] {E : Type u_2} [] [Algebra F E] (H : Subgroup (E ≃ₐ[F] E)) [] :
.fixingSubgroup = H
instance IntermediateField.fixedField.smul {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] (K : ) :
SMul K (IntermediateField.fixedField K.fixingSubgroup)
Equations
instance IntermediateField.fixedField.algebra {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] (K : ) :
Algebra K (IntermediateField.fixedField K.fixingSubgroup)
Equations
• = Algebra.mk { toFun := fun (x : K) => x, , map_one' := , map_mul' := , map_zero' := , map_add' := }
instance IntermediateField.fixedField.isScalarTower {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] (K : ) :
IsScalarTower (K) ((IntermediateField.fixedField K.fixingSubgroup)) E
Equations
• =
theorem IsGalois.fixedField_fixingSubgroup {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] (K : ) [] [h : IsGalois F E] :
IntermediateField.fixedField K.fixingSubgroup = K
theorem IsGalois.card_fixingSubgroup_eq_finrank {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] (K : ) [DecidablePred fun (x : E ≃ₐ[F] E) => x K.fixingSubgroup] [] [IsGalois F E] :
Fintype.card K.fixingSubgroup =
def IsGalois.intermediateFieldEquivSubgroup {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] [] [IsGalois F 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} [] {E : Type u_2} [] [Algebra 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} [] {E : Type u_2} [] [Algebra 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) [] (E : Type u_2) [] [Algebra F E] [] [IsGalois F E] :
∃ (p : ), p.Separable
theorem IsGalois.of_fixedField_eq_bot (F : Type u_1) [] (E : Type u_2) [] [Algebra F E] [] (h : ) :
theorem IsGalois.of_card_aut_eq_finrank (F : Type u_1) [] (E : Type u_2) [] [Algebra F E] [] (h : Fintype.card (E ≃ₐ[F] E) = ) :
theorem IsGalois.of_separable_splitting_field_aux {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {p : } [hFE : ] [sp : ] (hp : p.Separable) (K : Type u_3) [] [Algebra F K] [Algebra K E] [] {x : E} (hx : x p.aroots E) [Fintype (K →ₐ[F] E)] [Fintype (() →ₐ[F] E)] :
theorem IsGalois.of_separable_splitting_field {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {p : } [sp : ] (hp : p.Separable) :
theorem IsGalois.tfae {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] [] :
[IsGalois F E, , Fintype.card (E ≃ₐ[F] E) = , ∃ (p : ), p.Separable ].TFAE

Equivalent characterizations of a Galois extension of finite degree

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