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
IsGalois.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

Additional results #

Instances for Algebra.IsQuadraticExtension: a quadratic extension is Galois (if separable) with cyclic and thus abelian Galois group.

source

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

Prop

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

Instances

source

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

IsGalois F E ↔ Algebra.IsSeparable F E ∧ Normal F E

source

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

IsGalois F F

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

IsSeparable 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 (↥(FixedPoints.subfield G E)) E

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

Stacks Tag 09I3 (first part)

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 : IsSeparable F α) (h_splits : Polynomial.Splits (algebraMap F ↥F⟮α⟯) (minpoly F α)) :

Nat.card (↥F⟮α⟯ ≃ₐ[F] ↥F⟮α⟯) = Module.finrank F ↥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] :

Nat.card (E ≃ₐ[F] E) = Module.finrank F E

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

Stacks Tag 09I1 ('only if' part)

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

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

source

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

source

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

IsGalois (↥⊥) 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 ↥⊤ ↔ IsGalois F E

source

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

IsGalois F ↥⊥

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

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

Instances For

source

@[simp]

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 ↔ ∀ f ∈ H, f x = x

source

@[simp]

theorem IntermediateField.fixedField_bot {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

fixedField ⊥ = ⊤

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

Module.finrank (↥(fixedField H)) E = Nat.card ↥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

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 ≤ fixedField H ↔ H ≤ K.fixingSubgroup

source

theorem IntermediateField.fixingSubgroup_le {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K1 K2 : IntermediateField F E} (h12 : K1 ≤ K2) :

K2.fixingSubgroup ≤ K1.fixingSubgroup

The map K ↦ Gal(E/K) is inclusion-reversing.

source

@[deprecated IntermediateField.fixingSubgroup_le (since := "2025-05-02")]

theorem IntermediateField.fixingSubgroup.antimono {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K1 K2 : IntermediateField F E} (h12 : K1 ≤ K2) :

K2.fixingSubgroup ≤ K1.fixingSubgroup

Alias of IntermediateField.fixingSubgroup_le.

The map K ↦ Gal(E/K) is inclusion-reversing.

source

theorem IntermediateField.fixedField_le {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {H1 H2 : Subgroup (E ≃ₐ[F] E)} (h12 : H1 ≤ H2) :

fixedField H2 ≤ fixedField H1

source

theorem IntermediateField.fixingSubgroup_antitone {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

Antitone fixingSubgroup

source

@[deprecated IntermediateField.fixingSubgroup_antitone (since := "2025-05-02")]

theorem IntermediateField.fixingSubgroup_anti {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

Antitone fixingSubgroup

Alias of IntermediateField.fixingSubgroup_antitone.

source

theorem IntermediateField.fixedField_antitone {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

Antitone fixedField

source

@[simp]

theorem IntermediateField.mem_fixingSubgroup_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) (σ : E ≃ₐ[F] E) :

σ ∈ K.fixingSubgroup ↔ ∀ x ∈ K, σ x = x

source

@[simp]

theorem IntermediateField.fixingSubgroup_top {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

⊤.fixingSubgroup = ⊥

source

@[simp]

theorem IntermediateField.fixingSubgroup_bot {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

⊥.fixingSubgroup = ⊤

source

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

↥K.fixingSubgroup ≃* E ≃ₐ[↥K] E

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

Equations

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

(fixedField H).fixingSubgroup = H

source

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

↥H ≃* E ≃ₐ[↥(fixedField H)] E

A subgroup is isomorphic to the Galois group of its fixed field.

Equations

Instances For

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 ↥K ↥(fixedField K.fixingSubgroup)

Equations

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 ↥K ↥(fixedField K.fixingSubgroup)

Equations

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 (↥K) (↥(fixedField K.fixingSubgroup)) E

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

source

@[simp]

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

IntermediateField.fixedField ⊤ = ⊥

source

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

x ∈ ⊥ ↔ ∀ (f : E ≃ₐ[F] E), f x = x

source

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

x ∈ Set.range ⇑(algebraMap F E) ↔ ∀ (f : E ≃ₐ[F] E), f x = x

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) [FiniteDimensional F E] [IsGalois F E] :

Nat.card ↥K.fixingSubgroup = Module.finrank (↥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.

Stacks Tag 09DW

Equations

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

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

Instances For

source

theorem IntermediateField.restrictNormalHom_ker {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (E : IntermediateField K L) [Normal K ↥E] :

(AlgEquiv.restrictNormalHom ↥E).ker = E.fixingSubgroup

source

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

IsGalois K ↥(IntermediateField.fixedField H)

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

source

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

(L ≃ₐ[K] L) ⧸ H ≃* ↥(IntermediateField.fixedField H) ≃ₐ[K] ↥(IntermediateField.fixedField H)

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

Equations

Instances For

source

theorem IsGalois.normalAutEquivQuotient_apply {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] (σ : L ≃ₐ[K] L) :

(normalAutEquivQuotient H) ↑σ = (AlgEquiv.restrictNormalHom ↥(IntermediateField.fixedField H)) σ

source

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

(IntermediateField.map (↑σ) E).fixingSubgroup = MulAut.conj σ • E.fixingSubgroup

source

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

E.fixingSubgroup.Normal

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).

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 F), p.Separable ∧ 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 : Nat.card (E ≃ₐ[F] E) = Module.finrank F E) :

IsGalois F E

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

Stacks Tag 09I1 ('if' part)

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

Nat.card (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) = Nat.card (K →ₐ[F] E) * Module.finrank K ↥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 : p.Separable) :

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

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

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

IsGalois k ↥(IntermediateField.normalClosure k 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

source

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

IsGalois k K

source

instance Algebra.IsQuadraticExtension.isGalois (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [IsQuadraticExtension F K] [Algebra.IsSeparable F K] :

IsGalois F K

A quadratic separable extension is Galois.

source

instance Algebra.IsQuadraticExtension.isCyclic (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [IsQuadraticExtension F K] :

IsCyclic (K ≃ₐ[F] K)

A quadratic extension has cyclic Galois group.

source

instance Algebra.IsQuadraticExtension.isMulCommutative_galoisGroup (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [IsQuadraticExtension F K] :

IsMulCommutative (K ≃ₐ[F] K)

A quadratic extension has abelian Galois group.

Documentation

Mathlib.FieldTheory.Galois.Basic

Galois Extensions #

Main definitions #

Main results #

Additional results #