Galois Group as a profinite group

In this file, we prove that given a field extension K/k, there is a continuous isomorphism between Gal(K/k) and the limit of Gal(L/k), where L is a finite Galois intermediate field ordered by inverse inclusion, thus making Gal(K/k) profinite as a limit of finite groups.

Main definitions and results

In a field extension K/k

• finGaloisGroup L : The (finite) Galois group Gal(L/k) associated to a L : FiniteGaloisIntermediateField k K L.

• finGaloisGroupMap : For FiniteGaloisIntermediateField s L₁ and L₂ with L₂ ≤ L₁ giving the restriction of Gal(L₁/k) to Gal(L₂/k)

• finGaloisGroupFunctor : The functor from FiniteGaloisIntermediateField (ordered by reverse inclusion) to FiniteGrp, mapping each FiniteGaloisIntermediateField L to Gal (L/k).

• InfiniteGalois.algEquivToLimit : The homomorphism from K ≃ₐ[k] K to limit (asProfiniteGaloisGroupFunctor k K), induced by the projections from Gal(K/k) to any Gal(L/k) where L is a FiniteGaloisIntermediateField.

• InfiniteGalois.limitToAlgEquiv : The inverse of InfiniteGalois.algEquivToLimit, in which the elements of K ≃ₐ[k] K are constructed pointwise.

• InfiniteGalois.mulEquivToLimit : The mulEquiv obtained from combining the above two.

• InfiniteGalois.mulEquivToLimit_continuous : The inverse of InfiniteGalois.mulEquivToLimit is continuous.

• InfiniteGalois.continuousMulEquivToLimit ：The ContinuousMulEquiv between Gal(K/k) and limit (asProfiniteGaloisGroupFunctor k K) given by InfiniteGalois.mulEquivToLimit

• InfiniteGalois.ProfiniteGalGrp : Gal(K/k) as a profinite group as there is a ContinuousMulEquiv to a ProfiniteGrp given above.

• InfiniteGalois.restrictNormalHomContinuous : Any restrictNormalHom is continuous.

def FiniteGaloisIntermediateField.finGaloisGroup {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] (L : FiniteGaloisIntermediateField k K) : FiniteGrp.{u_2}

The (finite) Galois group Gal(L / k) associated to a L : FiniteGaloisIntermediateField k K L.

noncomputable def finGaloisGroupMap {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] {L₁ L₂ : (FiniteGaloisIntermediateField k K)ᵒᵖ} (le : L₁ ⟶ L₂) : (Opposite.unop L₁).finGaloisGroup ⟶ (Opposite.unop L₂).finGaloisGroup

For FiniteGaloisIntermediateField s L₁ and L₂ with L₂ ≤ L₁ the restriction homomorphism from Gal(L₁/k) to Gal(L₂/k)

@[simp]

theorem finGaloisGroupMap.map_id {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] (L : (FiniteGaloisIntermediateField k K)ᵒᵖ) : finGaloisGroupMap (CategoryTheory.CategoryStruct.id L) = CategoryTheory.CategoryStruct.id (Opposite.unop L).finGaloisGroup

@[simp]

theorem finGaloisGroupMap.map_comp {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] {L₁ L₂ L₃ : (FiniteGaloisIntermediateField k K)ᵒᵖ} (f : L₁ ⟶ L₂) (g : L₂ ⟶ L₃) : finGaloisGroupMap (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (finGaloisGroupMap f) (finGaloisGroupMap g)

noncomputable def finGaloisGroupFunctor (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] : CategoryTheory.Functor (FiniteGaloisIntermediateField k K)ᵒᵖ FiniteGrp.{u_2}

The functor from FiniteGaloisIntermediateField (ordered by reverse inclusion) to FiniteGrp, mapping each FiniteGaloisIntermediateField L to Gal (L/k)

@[reducible, inline]

noncomputable abbrev InfiniteGalois.asProfiniteGaloisGroupFunctor (k : Type u_3) (K : Type u_4) [Field k] [Field K] [Algebra k K] : CategoryTheory.Functor (FiniteGaloisIntermediateField k K)ᵒᵖ ProfiniteGrp.{u_4}

The composition of finGaloisGroupFunctor with the forgetful functor from FiniteGrp to ProfiniteGrp.

noncomputable def InfiniteGalois.algEquivToLimit (k : Type u_3) (K : Type u_4) [Field k] [Field K] [Algebra k K] : (K ≃ₐ[k] K) →* ↑(ProfiniteGrp.limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop

The homomorphism from Gal(K/k) to lim Gal(L/k) where L is a FiniteGaloisIntermediateField k K ordered by inverse inclusion. It is induced by the canonical projections from Gal(K/k) to Gal(L/k).

theorem InfiniteGalois.restrictNormalHom_continuous {k : Type u_3} {K : Type u_4} [Field k] [Field K] [Algebra k K] (L : IntermediateField k K) [Normal k ↥L] : Continuous ⇑(AlgEquiv.restrictNormalHom ↥L)

theorem InfiniteGalois.algEquivToLimit_continuous {k : Type u_3} {K : Type u_4} [Field k] [Field K] [Algebra k K] : Continuous ⇑(algEquivToLimit k K)

noncomputable def InfiniteGalois.proj {k : Type u_3} {K : Type u_4} [Field k] [Field K] [Algebra k K] (L : FiniteGaloisIntermediateField k K) : ↑(ProfiniteGrp.limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop →* ↥L.toIntermediateField ≃ₐ[k] ↥L.toIntermediateField

The projection map from lim Gal(L/k) to a specific Gal(L/k).

theorem InfiniteGalois.finGaloisGroupFunctor_map_proj_eq_proj {k : Type u_3} {K : Type u_4} [Field k] [Field K] [Algebra k K] (g : ↑(ProfiniteGrp.limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop) {L₁ L₂ : FiniteGaloisIntermediateField k K} (h : L₁ ⟶ L₂) : (CategoryTheory.ConcreteCategory.hom ((finGaloisGroupFunctor k K).map h.op)) ((proj L₂) g) = (proj L₁) g

theorem InfiniteGalois.proj_of_le {k : Type u_3} {K : Type u_4} [Field k] [Field K] [Algebra k K] (L : FiniteGaloisIntermediateField k K) (g : ↑(ProfiniteGrp.limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop) (x : ↥L.toIntermediateField) (L' : FiniteGaloisIntermediateField k K) (h : L ≤ L') : ↑(((proj L) g) x) = ↑(((proj L') g) ⟨↑x, ⋯⟩)

theorem InfiniteGalois.proj_adjoin_singleton_val {k : Type u_3} {K : Type u_4} [Field k] [Field K] [Algebra k K] [IsGalois k K] (g : ↑(ProfiniteGrp.limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop) (x : K) (y : ↥(FiniteGaloisIntermediateField.adjoin k {x}).toIntermediateField) (L : FiniteGaloisIntermediateField k K) (h : x ∈ L.toIntermediateField) : ↑(((proj (FiniteGaloisIntermediateField.adjoin k {x})) g) y) = ↑(((proj L) g) ⟨↑y, ⋯⟩)

theorem InfiniteGalois.toAlgEquivAux_eq_proj_of_mem {k : Type u_3} {K : Type u_4} [Field k] [Field K] [Algebra k K] [IsGalois k K] (g : ↑(ProfiniteGrp.limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop) (x : K) (L : FiniteGaloisIntermediateField k K) (hx : x ∈ L.toIntermediateField) : InfiniteGalois.toAlgEquivAux✝ g x = ↑(((proj L) g) ⟨x, hx⟩)

theorem InfiniteGalois.mk_toAlgEquivAux {k : Type u_3} {K : Type u_4} [Field k] [Field K] [Algebra k K] [IsGalois k K] (g : ↑(ProfiniteGrp.limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop) (x : K) (L : FiniteGaloisIntermediateField k K) (hx' : InfiniteGalois.toAlgEquivAux✝ g x ∈ L.toIntermediateField) (hx : x ∈ L.toIntermediateField) : ⟨InfiniteGalois.toAlgEquivAux✝ g x, hx'⟩ = ((proj L) g) ⟨x, hx⟩

theorem InfiniteGalois.toAlgEquivAux_eq_liftNormal {k : Type u_3} {K : Type u_4} [Field k] [Field K] [Algebra k K] [IsGalois k K] (g : ↑(ProfiniteGrp.limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop) (x : K) (L : FiniteGaloisIntermediateField k K) (hx : x ∈ L.toIntermediateField) : InfiniteGalois.toAlgEquivAux✝ g x = (((proj L) g).liftNormal K) x

noncomputable def InfiniteGalois.limitToAlgEquiv {k : Type u_3} {K : Type u_4} [Field k] [Field K] [Algebra k K] [IsGalois k K] (g : ↑(ProfiniteGrp.limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop) : K ≃ₐ[k] K

toAlgEquivAux as an AlgEquiv. It is done by using above lifting lemmas on bigger FiniteGaloisIntermediateField.

@[simp]

theorem InfiniteGalois.limitToAlgEquiv_apply {k : Type u_3} {K : Type u_4} [Field k] [Field K] [Algebra k K] [IsGalois k K] (g : ↑(ProfiniteGrp.limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop) (a✝ : K) : (limitToAlgEquiv g) a✝ = InfiniteGalois.toAlgEquivAux✝ g a✝

@[simp]

theorem InfiniteGalois.limitToAlgEquiv_symm_apply {k : Type u_3} {K : Type u_4} [Field k] [Field K] [Algebra k K] [IsGalois k K] (g : ↑(ProfiniteGrp.limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop) (a✝ : K) : (limitToAlgEquiv g).symm a✝ = InfiniteGalois.toAlgEquivAux✝ g⁻¹ a✝

noncomputable def InfiniteGalois.mulEquivToLimit (k : Type u_3) (K : Type u_4) [Field k] [Field K] [Algebra k K] [IsGalois k K] : (K ≃ₐ[k] K) ≃* ↑(ProfiniteGrp.limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop

algEquivToLimit as a MulEquiv.

theorem InfiniteGalois.krullTopology_mem_nhds_one_iff_of_isGalois {k : Type u_3} {K : Type u_4} [Field k] [Field K] [Algebra k K] [IsGalois k K] (A : Set (K ≃ₐ[k] K)) : A ∈ nhds 1 ↔ ∃ (L : FiniteGaloisIntermediateField k K), ↑L.fixingSubgroup ⊆ A

theorem InfiniteGalois.isOpen_mulEquivToLimit_image_fixingSubgroup {k : Type u_3} {K : Type u_4} [Field k] [Field K] [Algebra k K] [IsGalois k K] (L : FiniteGaloisIntermediateField k K) : IsOpen (⇑(mulEquivToLimit k K) '' ↑L.fixingSubgroup)

theorem InfiniteGalois.mulEquivToLimit_symm_continuous {k : Type u_3} {K : Type u_4} [Field k] [Field K] [Algebra k K] [IsGalois k K] : Continuous ⇑(mulEquivToLimit k K).symm

noncomputable def InfiniteGalois.continuousMulEquivToLimit (k : Type u_3) (K : Type u_4) [Field k] [Field K] [Algebra k K] [IsGalois k K] : (K ≃ₐ[k] K) ≃ₜ* ↑(ProfiniteGrp.limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop

The ContinuousMulEquiv between K ≃ₐ[k] K and lim Gal(L/k) where L is a FiniteGaloisIntermediateField ordered by inverse inclusion, obtained from InfiniteGalois.mulEquivToLimit

instance InfiniteGalois.instCompactSpaceAlgEquivOfIsGalois (k : Type u_3) (K : Type u_4) [Field k] [Field K] [Algebra k K] [IsGalois k K] : CompactSpace (K ≃ₐ[k] K)

noncomputable def InfiniteGalois.profiniteGalGrp (k : Type u_3) (K : Type u_4) [Field k] [Field K] [Algebra k K] [IsGalois k K] : ProfiniteGrp.{u_4}

Gal(K/k) as a profinite group as there is a ContinuousMulEquiv to a ProfiniteGrp given above

noncomputable def InfiniteGalois.profiniteGalGrpIsoLimit (k : Type u_3) (K : Type u_4) [Field k] [Field K] [Algebra k K] [IsGalois k K] : profiniteGalGrp k K ≅ ProfiniteGrp.limit (asProfiniteGaloisGroupFunctor k K)

The categorical isomorphism between profiniteGalGrp and lim Gal(L/k) where L is a FiniteGaloisIntermediateField ordered by inverse inclusion