mathlib3documentation

field_theory.galois

Galois Extensions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

• intermediate_field.fixing_subgroup_fixed_field : If E/F is finite dimensional (but not necessarily Galois) then fixing_subgroup (fixed_field H) = H
• intermediate_field.fixed_field_fixing_subgroup: If E/F is finite dimensional and Galois then fixed_field (fixing_subgroup K) = K

Together, these two results 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 of this typeclass
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] [finite 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 : (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 fixed_points.intermediate_field {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] (M : Type u_3) [monoid M] [ E] [ E] :

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

Equations
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
Instances for ↥intermediate_field.fixed_field
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] [decidable_pred (λ (_x : E ≃ₐ[F] E), _x H)] :
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) :
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) [decidable_pred (λ (_x : E ≃ₐ[F] E), _x K.fixing_subgroup)] [ 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

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 : Type u_3) [field K] [ K] [ E] [ E] {x : E} (hx : x (polynomial.map E) p).roots) [fintype (K →ₐ[F] E)] [fintype →ₐ[F] E)] :
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

@[protected, instance]
def is_galois.normal_closure (k : Type u_1) (K : Type u_2) (F : Type u_3) [field k] [field K] [field F] [ K] [ F] [ F] [ F] [ F] :
K F)
@[protected, instance]
def is_alg_closure.is_galois (k : Type u_1) (K : Type u_2) [field k] [field K] [ K] [ K] [char_zero k] :
K