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

source

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

Prop

to_isSeparable : IsSeparable F E
to_normal : Normal 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

source

theorem isGalois_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

IsGalois F E ↔ IsSeparable F E ∧ Normal F E

source

instance IsGalois.self (F : Type u_1) [Field F] :

IsGalois F F

Equations

IsGalois.self = IsGalois.self.proof_1

source

theorem IsGalois.integral (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] [IsGalois F E] (x : E) :

IsIntegral F x

source

theorem IsGalois.separable (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] [IsGalois F E] (x : E) :

Polynomial.Separable (minpoly F x)

source

theorem IsGalois.splits (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] [IsGalois F E] (x : E) :

Polynomial.Splits (algebraMap F E) (minpoly F x)

source

instance IsGalois.of_fixed_field (E : Type u_2) [Field E] (G : Type u_3) [Group G] [Finite G] [MulSemiringAction G E] :

IsGalois { x // x ∈ FixedPoints.subfield G E } E

Equations

IsGalois.of_fixed_field = IsGalois.of_fixed_field.proof_1

source

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 : Polynomial.Separable (minpoly F α)) (h_splits : Polynomial.Splits (algebraMap F { x // x ∈ F⟮α⟯ }) (minpoly F α)) :

Fintype.card ({ x // x ∈ F⟮α⟯ } ≃ₐ[F] { x // x ∈ F⟮α⟯ }) = FiniteDimensional.finrank F { x // x ∈ F⟮α⟯ }

source

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

Fintype.card (E ≃ₐ[F] E) = FiniteDimensional.finrank F E

source

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

IsGalois K E

source

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 // x ∈ K } E

Equations

@IsGalois.tower_top_intermediateField = @IsGalois.tower_top_intermediateField.proof_1

source

theorem isGalois_iff_isGalois_bot {F : Type u_1} {E : Type u_3} [Field F] [Field E] [Algebra F E] :

IsGalois { x // x ∈ ⊥ } E ↔ IsGalois F E

source

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') :

IsGalois F E'

source

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') :

IsGalois F E ↔ IsGalois F E'

source

theorem isGalois_iff_isGalois_top {F : Type u_1} {E : Type u_3} [Field F] [Field E] [Algebra F E] :

IsGalois F { x // x ∈ ⊤ } ↔ IsGalois F E

source

instance isGalois_bot {F : Type u_1} {E : Type u_3} [Field F] [Field E] [Algebra F E] :

IsGalois F { x // x ∈ ⊥ }

Equations

@isGalois_bot = @isGalois_bot.proof_1

source

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

IntermediateField F E

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

source

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

IntermediateField F E

The intermediate field fixed by a subgroup

Equations

IntermediateField.fixedField H = FixedPoints.intermediateField { x // x ∈ H }

Instances For

source

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 => x ∈ H] :

FiniteDimensional.finrank { x // x ∈ IntermediateField.fixedField H } E = Fintype.card { x // x ∈ H }

source

def IntermediateField.fixingSubgroup {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) :

Subgroup (E ≃ₐ[F] E)

The subgroup fixing an intermediate field

Equations

IntermediateField.fixingSubgroup K = fixingSubgroup (E ≃ₐ[F] E) ↑K

Instances For

source

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 ≤ IntermediateField.fixingSubgroup K

source

def IntermediateField.fixingSubgroupEquiv {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) :

{ x // x ∈ IntermediateField.fixingSubgroup K } ≃* E ≃ₐ[{ x // 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

source

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.fixingSubgroup (IntermediateField.fixedField H) = H

source

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 // x ∈ K } { x // x ∈ IntermediateField.fixedField (IntermediateField.fixingSubgroup K) }

Equations

One or more equations did not get rendered due to their size.

source

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 // x ∈ K } { x // x ∈ IntermediateField.fixedField (IntermediateField.fixingSubgroup K) }

Equations

One or more equations did not get rendered due to their size.

source

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 // x ∈ K } { x // x ∈ IntermediateField.fixedField (IntermediateField.fixingSubgroup K) } E

Equations

@IntermediateField.fixedField.isScalarTower = @IntermediateField.fixedField.isScalarTower.proof_1

source

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 (IntermediateField.fixingSubgroup K) = K

source

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 => x ∈ IntermediateField.fixingSubgroup K] [FiniteDimensional F E] [IsGalois F E] :

Fintype.card { x // x ∈ IntermediateField.fixingSubgroup K } = FiniteDimensional.finrank { x // x ∈ K } E

source

def IsGalois.intermediateFieldEquivSubgroup {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] [FiniteDimensional F E] [IsGalois F E] :

IntermediateField F E ≃o (Subgroup (E ≃ₐ[F] E))ᵒᵈ

The Galois correspondence from intermediate fields to subgroups

Equations

One or more equations did not get rendered due to their size.

Instances For

source

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

source

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

source

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.Separable p ∧ Polynomial.IsSplittingField F E p

source

theorem IsGalois.of_fixedField_eq_bot (F : Type u_1) [Field F] (E : Type u_2) [Field E] [Algebra F E] [FiniteDimensional F E] (h : IntermediateField.fixedField ⊤ = ⊥) :

IsGalois F E

source

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) = FiniteDimensional.finrank F E) :

IsGalois F E

source

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 : Polynomial.Separable p) (K : Type u_3) [Field K] [Algebra F K] [Algebra K E] [IsScalarTower F K E] {x : E} (hx : x ∈ Polynomial.aroots p E) [Fintype (K →ₐ[F] E)] [Fintype ({ x // x ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E)] :

Fintype.card ({ x // x ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E) = Fintype.card (K →ₐ[F] E) * FiniteDimensional.finrank K { x // x ∈ K⟮x⟯ }

source

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 : Polynomial.Separable p) :

IsGalois F E

source

theorem IsGalois.tfae {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] [FiniteDimensional F E] :

List.TFAE [IsGalois F E, IntermediateField.fixedField ⊤ = ⊥, Fintype.card (E ≃ₐ[F] E) = FiniteDimensional.finrank F E, ∃ p, Polynomial.Separable p ∧ Polynomial.IsSplittingField F E p]

Equivalent characterizations of a Galois extension of finite degree

source

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] [Algebra K F] [IsScalarTower k K F] [IsGalois k F] :

IsGalois k { x // x ∈ normalClosure k K F }

Equations

IsGalois.normalClosure = IsGalois.normalClosure.proof_1

source

instance IsAlgClosure.isGalois (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [IsAlgClosure k K] [CharZero k] :

IsGalois k K

Equations

IsAlgClosure.isGalois = IsAlgClosure.isGalois.proof_1