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

source

@[class]

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

Prop

to_is_separable : is_separable F E
to_normal : normal F 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

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

@[protected, instance]

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

is_galois F F

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

@[protected, instance]

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

is_galois ↥(fixed_points.subfield G E) E

source

theorem is_galois.intermediate_field.adjoin_simple.card_aut_eq_finrank (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.finrank F ↥F⟮α⟯

source

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

fintype.card (E ≃ₐ[F] E) = finite_dimensional.finrank 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

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

@[protected, instance]

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

is_galois F ↥⊥

source

def fixed_points.intermediate_field {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] (M : Type u_3) [monoid M] [mul_semiring_action M E] [smul_comm_class M F E] :

intermediate_field F E

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

Equations

fixed_points.intermediate_field M = {to_subalgebra := {carrier := mul_action.fixed_points M E mul_distrib_mul_action.to_mul_action, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _, algebra_map_mem' := _}, neg_mem' := _, inv_mem' := _}

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 = fixed_points.intermediate_field ↥H

Instances for ↥intermediate_field.fixed_field

source

theorem intermediate_field.finrank_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] [decidable_pred (λ (_x : E ≃ₐ[F] E), _x ∈ H)] :

finite_dimensional.finrank ↥(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 = fixing_subgroup (E ≃ₐ[F] E) ↑K

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)), {to_fun := ↑ϕ.to_ring_equiv.to_fun, inv_fun := ↑ϕ.to_ring_equiv.inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}, inv_fun := λ (ϕ : E ≃ₐ[↥K] E), ⟨alg_equiv.restrict_scalars F ϕ, _⟩, 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

@[protected, 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_smul := {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

@[protected, 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_finrank {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] (K : intermediate_field F E) [decidable_pred (λ (_x : E ≃ₐ[F] E), _x ∈ K.fixing_subgroup)] [finite_dimensional F E] [is_galois F E] :

fintype.card ↥(K.fixing_subgroup) = finite_dimensional.finrank ↥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 (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 : (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] [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_finrank (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.finrank 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 : Type u_3) [field K] [algebra F K] [algebra K E] [is_scalar_tower F K E] {x : E} (hx : x ∈ (polynomial.map (algebra_map F E) p).roots) [fintype (K →ₐ[F] E)] [fintype (↥(intermediate_field.restrict_scalars F K⟮x⟯) →ₐ[F] E)] :

fintype.card (↥(intermediate_field.restrict_scalars F K⟮x⟯) →ₐ[F] E) = fintype.card (K →ₐ[F] E) * finite_dimensional.finrank 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.finrank F E, ∃ (p : polynomial F), p.separable ∧ polynomial.is_splitting_field F E p].tfae

Equivalent characterizations of a Galois extension of finite degree

source

@[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] [algebra k K] [algebra k F] [algebra K F] [is_scalar_tower k K F] [is_galois k F] :

is_galois k ↥(normal_closure k K F)

source

@[protected, instance]

def is_alg_closure.is_galois (k : Type u_1) (K : Type u_2) [field k] [field K] [algebra k K] [is_alg_closure k K] [char_zero k] :

is_galois k K