Galois Extensions #
In this file we define Galois extensions as extensions which are both separable and normal.
Main definitions #
is_galois F EwhereEis an extension ofFfixed_field HwhereH : subgroup (E ≃ₐ[F] E)fixing_subgroup KwhereK : intermediate_field F Egalois_correspondencewhereE/Fis finite dimensional and Galois
Main results #
-
fixing_subgroup_of_fixed_field: IfE/Fis finite dimensional (but not necessarily Galois) thenfixing_subgroup (fixed_field H) = H -
fixed_field_of_fixing_subgroup: IfE/Fis finite dimensional and Galois thenfixed_field (fixing_subgroup K) = KTogether, these two result prove the Galois correspondence -
is_galois.tfae: Equivalent characterizations of a Galois extension of finite degree
@[class]
- 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
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
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
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)
@[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 ↥(fixed_points.subfield 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]
[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 α)) :
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
@[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] :
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
- intermediate_field.fixed_field H = {carrier := mul_action.fixed_points ↥H E H.mul_action, one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _, algebra_map_mem' := _, neg_mem' := _, inv_mem' := _}
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] :
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
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
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
- 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' := _}
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] :
@[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) :
Equations
@[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) :
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] :
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)
[finite_dimensional F E]
[is_galois F E] :
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' := _}
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] :
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 := _}
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] :
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 := _}
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
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
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
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) :
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
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