# mathlibdocumentation

field_theory.galois

# Galois Extensions #

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

## Main definitions #

• is_galois F E where E is an extension of F
• fixed_field H where H : subgroup (E ≃ₐ[F] E)
• fixing_subgroup K where K : intermediate_field F E
• galois_correspondence where E/F is finite dimensional and Galois

## Main results #

• fixing_subgroup_of_fixed_field : If E/F is finite dimensional (but not necessarily Galois) then fixing_subgroup (fixed_field H) = H

• fixed_field_of_fixing_subgroup: If E/F is finite dimensional and Galois then fixed_field (fixing_subgroup K) = K Together, these two result prove the Galois correspondence

• is_galois.tfae : Equivalent characterizations of a Galois extension of finite degree

@[class]
structure is_galois (F : Type u_1) [field F] (E : Type u_2) [field E] [ E] :
Prop
• to_is_separable : E
• to_normal : 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 is_galois_iff {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] :
E E E
@[protected, instance]
def is_galois.self (F : Type u_1) [field F] :
F
theorem is_galois.integral (F : Type u_1) [field F] {E : Type u_2} [field E] [ E] [ E] (x : E) :
x
theorem is_galois.separable (F : Type u_1) [field F] {E : Type u_2} [field E] [ E] [ E] (x : E) :
theorem is_galois.splits (F : Type u_1) [field F] {E : Type u_2} [field E] [ E] [ E] (x : E) :
(minpoly F x)
@[protected, instance]
def is_galois.of_fixed_field (E : Type u_2) [field E] (G : Type u_1) [group G] [fintype G] [ E] :
E
theorem is_galois.intermediate_field.adjoin_simple.card_aut_eq_finrank (F : Type u_1) [field F] (E : Type u_2) [field E] [ E] [ E] {α : E} (hα : α) (h_sep : (minpoly F α).separable) (h_splits : polynomial.splits (Fα)) (minpoly F α)) :
theorem is_galois.card_aut_eq_finrank (F : Type u_1) [field F] (E : Type u_2) [field E] [ E] [ E] [ E] :
theorem is_galois.tower_top_of_is_galois (F : Type u_1) (K : Type u_2) (E : Type u_3) [field F] [field K] [field E] [ K] [ E] [ E] [ E] [ E] :
E
@[protected, instance]
def is_galois.tower_top_intermediate_field {F : Type u_1} {E : Type u_3} [field F] [field E] [ E] (K : E) [h : E] :
E
theorem is_galois_iff_is_galois_bot {F : Type u_1} {E : Type u_3} [field F] [field E] [ E] :
E
theorem is_galois.of_alg_equiv {F : Type u_1} {E : Type u_3} [field F] [field E] {E' : Type u_4} [field E'] [ E'] [ E] [h : E] (f : E ≃ₐ[F] E') :
E'
theorem alg_equiv.transfer_galois {F : Type u_1} {E : Type u_3} [field F] [field E] {E' : Type u_4} [field E'] [ E'] [ E] (f : E ≃ₐ[F] E') :
E E'
theorem is_galois_iff_is_galois_top {F : Type u_1} {E : Type u_3} [field F] [field E] [ E] :
E
@[protected, instance]
def is_galois_bot {F : Type u_1} {E : Type u_3} [field F] [field E] [ E] :
def intermediate_field.fixed_field {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] (H : subgroup (E ≃ₐ[F] E)) :

The intermediate_field fixed by a subgroup

Equations
theorem intermediate_field.finrank_fixed_field_eq_card {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] (H : subgroup (E ≃ₐ[F] E)) [ E] :
def intermediate_field.fixing_subgroup {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] (K : E) :

The subgroup fixing an intermediate_field

Equations
theorem intermediate_field.le_iff_le {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] (H : subgroup (E ≃ₐ[F] E)) (K : E) :
noncomputable def intermediate_field.fixing_subgroup_equiv {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] (K : E) :

The fixing_subgroup of K : intermediate_field F E is isomorphic to E ≃ₐ[K] E

Equations
theorem intermediate_field.fixing_subgroup_fixed_field {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] (H : subgroup (E ≃ₐ[F] E)) [ E] :
@[protected, instance]
def intermediate_field.fixed_field.algebra {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] (K : E) :
Equations
@[protected, instance]
def intermediate_field.fixed_field.is_scalar_tower {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] (K : E) :
theorem is_galois.fixed_field_fixing_subgroup {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] (K : E) [ E] [h : E] :
theorem is_galois.card_fixing_subgroup_eq_finrank {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] (K : E) [ E] [ E] :
def is_galois.intermediate_field_equiv_subgroup {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] [ E] [ E] :

The Galois correspondence from intermediate fields to subgroups

Equations
def is_galois.galois_insertion_intermediate_field_subgroup {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] [ E] :

The Galois correspondence as a galois_insertion

Equations
def is_galois.galois_coinsertion_intermediate_field_subgroup {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] [ E] [ E] :

The Galois correspondence as a galois_coinsertion

Equations
theorem is_galois.is_separable_splitting_field (F : Type u_1) [field F] (E : Type u_2) [field E] [ E] [ E] [ E] :
∃ (p : ,
theorem is_galois.of_fixed_field_eq_bot (F : Type u_1) [field F] (E : Type u_2) [field E] [ E] [ E]  :
E
theorem is_galois.of_card_aut_eq_finrank (F : Type u_1) [field F] (E : Type u_2) [field E] [ E] [ E] (h : fintype.card (E ≃ₐ[F] E) = ) :
E
theorem is_galois.of_separable_splitting_field_aux {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] {p : polynomial F} [hFE : E] [sp : p] (hp : p.separable) (K : E) {x : E} (hx : x (polynomial.map E) p).roots) :
theorem is_galois.of_separable_splitting_field {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] {p : polynomial F} [sp : p] (hp : p.separable) :
E
theorem is_galois.tfae {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] [ E] :
E, , fintype.card (E ≃ₐ[F] E) = , ∃ (p : , .tfae

Equivalent characterizations of a Galois extension of finite degree