mathlib documentation

field_theory.galois

Galois Extensions

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

Main definitions

Main results

@[class]
def is_galois (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

Equations
Instances
@[instance]
def is_galois.self (F : Type u_1) [field F] :

@[instance]
def is_galois.to_is_separable (F : Type u_1) [field F] (E : Type u_2) [field E] [algebra F E] [h : is_galois F E] :

@[instance]
def is_galois.to_normal (F : Type u_1) [field F] (E : Type u_2) [field E] [algebra F E] [h : is_galois F E] :
normal F E

theorem is_galois.integral {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] (h : is_galois F E) (x : E) :

theorem is_galois.separable {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] (h : is_galois F E) (x : E) :

theorem is_galois.normal {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] (h : is_galois F E) (x : E) :

@[instance]
def is_galois.of_fixed_field (E : Type u_2) [field E] (G : Type u_1) [group G] [fintype G] [mul_semiring_action G E] :

theorem is_galois.card_aut_eq_findim (F : Type u_1) [field F] (E : Type u_2) [field E] [algebra F E] [finite_dimensional F E] [h : is_galois F 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] [algebra F K] [algebra F E] [algebra K E] [is_scalar_tower F K E] [h : is_galois F E] :

@[instance]
def is_galois.tower_top_intermediate_field {F : Type u_1} {E : Type u_3} [field F] [field E] [algebra F E] (K : intermediate_field F E) [h : is_galois F E] :

theorem is_galois_iff_is_galois_bot {F : Type u_1} {E : Type u_3} [field F] [field E] [algebra F 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'] [algebra F E'] [algebra F E] [h : is_galois F E] (f : E ≃ₐ[F] E') :

theorem alg_equiv.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') :

theorem is_galois_iff_is_galois_top {F : Type u_1} {E : Type u_3} [field F] [field E] [algebra F E] :

@[instance]
def is_galois_bot {F : Type u_1} {E : Type u_3} [field F] [field E] [algebra F E] :

@[instance]
def intermediate_field.subgroup_action {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] (H : subgroup (E ≃ₐ[F] E)) :

Equations
def intermediate_field.fixed_field {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] (H : subgroup (E ≃ₐ[F] E)) :

The intermediate_field fixed by a subgroup

Equations
def intermediate_field.fixing_subgroup {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] (K : intermediate_field F 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] [algebra F E] (H : subgroup (E ≃ₐ[F] E)) (K : intermediate_field F E) :

def intermediate_field.fixing_subgroup_equiv {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] (K : intermediate_field F E) :

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

Equations

The Galois correspondence from intermediate fields to subgroups

Equations
theorem is_galois.is_separable_splitting_field (F : Type u_1) [field F] (E : Type u_2) [field E] [algebra F E] [finite_dimensional F E] [h : is_galois F E] :

theorem is_galois.of_fixed_field_eq_bot (F : Type u_1) [field F] (E : Type u_2) [field E] [algebra F E] [finite_dimensional F E] (h : intermediate_field.fixed_field = ) :

theorem is_galois.of_card_aut_eq_findim (F : Type u_1) [field F] (E : Type u_2) [field E] [algebra F E] [finite_dimensional F E] (h : fintype.card (E ≃ₐ[F] E) = finite_dimensional.findim F E) :

theorem is_galois.of_separable_splitting_field {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] {p : polynomial F} [sp : polynomial.is_splitting_field F E p] (hp : p.separable) :

Equivalent characterizations of a Galois extension of finite degree