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

source

@[class]

structure is_galois (F : Type u_1) [field F] (E : Type u_2) [field E] [algebra F E] :

Prop

separable' : is_separable F E
normal' : normal F E

A field extension E/F is galois if it is both separable and normal

Instances

source

theorem is_galois_iff {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] :

is_galois F E ↔ is_separable F E ∧ normal F E

source

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

is_separable F E

source

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

normal F E

source

@[instance]

def is_galois.normal'' {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] [h : is_galois F E] :

normal F E

source

@[instance]

def is_galois.self (F : Type u_1) [field F] :

is_galois F F

source

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

is_separable F E

source

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

source

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

is_integral F x

source

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

(minpoly F x).separable

source

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

polynomial.splits (algebra_map F E) (minpoly F x)

source

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

is_galois ↥(mul_action.fixed_points G E) E

source

theorem is_galois.intermediate_field.adjoin_simple.card_aut_eq_findim (F : Type u_1) [field F] (E : Type u_2) [field E] [algebra F E] [finite_dimensional F E] {α : E} (hα : is_integral F α) (h_sep : (minpoly F α).separable) (h_splits : polynomial.splits (algebra_map F ↥(F⟮α⟯)) (minpoly F α)) :

fintype.card (↥(F⟮α⟯) ≃ₐ[F] ↥(F⟮α⟯)) = finite_dimensional.findim F ↥(F⟮α⟯)

source

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

fintype.card (E ≃ₐ[F] E) = finite_dimensional.findim F E

source

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] [is_galois F E] :

is_galois K E

source

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

is_galois ↥K E

source

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

is_galois ↥⊥ E ↔ is_galois F E

source

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

is_galois F E'

source

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

is_galois F E ↔ is_galois F E'

source

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

is_galois F ↥⊤ ↔ is_galois F E

source

@[instance]

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

is_galois F ↥⊥

source

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

faithful_mul_semiring_action ↥H E

Equations

intermediate_field.subgroup_action H = {to_mul_semiring_action := {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := λ (h : ↥H) (x : E), ⇑h x}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, smul_one := _, smul_mul := _}, eq_of_smul_eq_smul' := _}

source

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

intermediate_field F E

The intermediate_field fixed by a subgroup

Equations

intermediate_field.fixed_field H = {carrier := mul_action.fixed_points ↥H E distrib_mul_action.to_mul_action, one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _, algebra_map_mem' := _, neg_mem' := _, inv_mem' := _}

source

theorem intermediate_field.findim_fixed_field_eq_card {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] (H : subgroup (E ≃ₐ[F] E)) [finite_dimensional F E] :

finite_dimensional.findim ↥(intermediate_field.fixed_field H) E = fintype.card ↥H

source

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

subgroup (E ≃ₐ[F] E)

The subgroup fixing an intermediate_field

Equations

K.fixing_subgroup = {carrier := λ (ϕ : E ≃ₐ[F] E), ∀ (x : ↥K), ⇑ϕ ↑x = ↑x, one_mem' := _, mul_mem' := _, inv_mem' := _}

source

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

K ≤ intermediate_field.fixed_field H ↔ H ≤ K.fixing_subgroup

source

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

↥(K.fixing_subgroup) ≃* E ≃ₐ[↥K] E

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

Equations

K.fixing_subgroup_equiv = {to_fun := λ (ϕ : ↥(K.fixing_subgroup)), alg_equiv.of_bijective {to_fun := ⇑ϕ, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _} _, inv_fun := λ (ϕ : E ≃ₐ[↥K] E), ⟨alg_equiv.of_bijective {to_fun := ⇑ϕ, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _} _, _⟩, left_inv := _, right_inv := _, map_mul' := _}

source

theorem intermediate_field.fixing_subgroup_fixed_field {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] (H : subgroup (E ≃ₐ[F] E)) [finite_dimensional F E] :

(intermediate_field.fixed_field H).fixing_subgroup = H

source

@[instance]

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

algebra ↥K ↥(intermediate_field.fixed_field K.fixing_subgroup)

Equations

intermediate_field.fixed_field.algebra K = {to_has_scalar := {smul := λ (x : ↥K) (y : ↥(intermediate_field.fixed_field K.fixing_subgroup)), ⟨(↑x) * ↑y, _⟩}, to_ring_hom := {to_fun := λ (x : ↥K), ⟨↑x, _⟩, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}

source

@[instance]

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

is_scalar_tower ↥K ↥(intermediate_field.fixed_field K.fixing_subgroup) E

source

theorem is_galois.fixed_field_fixing_subgroup {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] (K : intermediate_field F E) [finite_dimensional F E] [h : is_galois F E] :

intermediate_field.fixed_field K.fixing_subgroup = K

source

theorem is_galois.card_fixing_subgroup_eq_findim {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] (K : intermediate_field F E) [finite_dimensional F E] [is_galois F E] :

fintype.card ↥(K.fixing_subgroup) = finite_dimensional.findim ↥K E

source

def is_galois.intermediate_field_equiv_subgroup {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] [finite_dimensional F E] [is_galois F E] :

intermediate_field F E ≃o order_dual (subgroup (E ≃ₐ[F] E))

The Galois correspondence from intermediate fields to subgroups

Equations

is_galois.intermediate_field_equiv_subgroup = {to_equiv := {to_fun := intermediate_field.fixing_subgroup _inst_3, inv_fun := intermediate_field.fixed_field _inst_3, left_inv := _, right_inv := _}, map_rel_iff' := _}

source

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

galois_insertion (⇑order_dual.to_dual ∘ intermediate_field.fixing_subgroup) (intermediate_field.fixed_field ∘ ⇑order_dual.to_dual)

The Galois correspondence as a galois_insertion

Equations

is_galois.galois_insertion_intermediate_field_subgroup = {choice := λ (K : intermediate_field F E) (_x : (intermediate_field.fixed_field ∘ ⇑order_dual.to_dual) ((⇑order_dual.to_dual ∘ intermediate_field.fixing_subgroup) K) ≤ K), K.fixing_subgroup, gc := _, le_l_u := _, choice_eq := _}

source

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

galois_coinsertion (⇑order_dual.to_dual ∘ intermediate_field.fixing_subgroup) (intermediate_field.fixed_field ∘ ⇑order_dual.to_dual)

The Galois correspondence as a galois_coinsertion

Equations

is_galois.galois_coinsertion_intermediate_field_subgroup = {choice := λ (H : order_dual (subgroup (E ≃ₐ[F] E))) (_x : H ≤ (⇑order_dual.to_dual ∘ intermediate_field.fixing_subgroup) ((intermediate_field.fixed_field ∘ ⇑order_dual.to_dual) H)), intermediate_field.fixed_field H, gc := _, u_l_le := _, choice_eq := _}

source

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

∃ (p : polynomial F), p.separable ∧ polynomial.is_splitting_field F E p

source

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 ⊤ = ⊥) :

is_galois F E

source

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

is_galois F E

source

theorem is_galois.of_separable_splitting_field_aux {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] {p : polynomial F} [hFE : finite_dimensional F E] [sp : polynomial.is_splitting_field F E p] (hp : p.separable) (K : intermediate_field F E) {x : E} (hx : x ∈ (polynomial.map (algebra_map F E) p).roots) :

fintype.card (↥↑(↥K⟮x⟯) →ₐ[F] E) = (fintype.card (↥K →ₐ[F] E)) * finite_dimensional.findim ↥K ↥(↥K⟮x⟯)

source

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

is_galois F E

source

theorem is_galois.tfae {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] [finite_dimensional F E] :

[is_galois F E, intermediate_field.fixed_field ⊤ = ⊥, fintype.card (E ≃ₐ[F] E) = finite_dimensional.findim F E, ∃ (p : polynomial F), p.separable ∧ polynomial.is_splitting_field F E p].tfae

Equivalent characterizations of a Galois extension of finite degree