Galois Extensions
In this file we define Galois extensions as extensions which are both separable and normal.
Main definitions
is_galois F E
whereE
is an extension ofF
fixed_field H
whereH : subgroup (E ≃ₐ[F] E)
fixing_subgroup K
whereK : intermediate_field F E
galois_correspondence
whereE/F
is finite dimensional and Galois
Main results
fixing_subgroup_of_fixed_field
: IfE/F
is finite dimensional (but not necessarily Galois) thenfixing_subgroup (fixed_field H) = H
fixed_field_of_fixing_subgroup
: IfE/F
is finite dimensional and Galois thenfixed_field (fixing_subgroup K) = K
Together, these two result prove the Galois correspondenceis_galois.tfae
: Equivalent characterizations of a Galois extension of finite degree
A field extension E/F is galois if it is both separable and normal
Equations
- is_galois F E = (is_separable F E ∧ normal F 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' := _}
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' := _}
The subgroup fixing an intermediate_field
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' := _}
Equations
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' := _}
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 := _}
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 := _}
Equivalent characterizations of a Galois extension of finite degree