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 #
intermediate_field.fixing_subgroup_fixed_field: IfE/Fis finite dimensional (but not necessarily Galois) thenfixing_subgroup (fixed_field H) = Hintermediate_field.fixed_field_fixing_subgroup: IfE/Fis finite dimensional and Galois thenfixed_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
@[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. Note that in mathlib a separable extension of fields is by definition algebraic.
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)
@[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
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
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] :
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' := _}
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)] :
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
- K.fixing_subgroup = fixing_subgroup (E ≃ₐ[F] E) ↑K
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)), {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' := _}
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] :
@[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) :
Equations
@[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) :
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)
[decidable_pred (λ (_x : E ≃ₐ[F] E), _x ∈ K.fixing_subgroup)]
[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] :
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 : (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 : 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⟯
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
@[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