The Fundamental Theorem of Infinite Galois Theory

In this file, we prove the fundamental theorem of infinite Galois theory and the special case for open subgroups and normal subgroups. We first verify that IntermediateField.fixingSubgroup and IntermediateField.fixedField are inverses of each other between intermediate fields and closed subgroups of the Galois group.

Main definitions and results

In K/k, for any intermediate field L :

• fixingSubgroup_isClosed : the subgroup fixing L (Gal(K/L)) is closed.

• fixedField_fixingSubgroup : the field fixed by the subgroup fixing L is equal to L itself.

For any subgroup H of Gal(K/k) :

• restrict_fixedField : For a Galois intermediate field M, the fixed field of the image of H restricted to M is equal to the fixed field of H intersected with M.
• fixingSubgroup_fixedField : If H is closed, the fixing subgroup of the fixed field of H is equal to H itself.

The fundamental theorem of infinite Galois theory :

• IntermediateFieldEquivClosedSubgroup : The order equivalence is given by mapping any intermediate field L to the subgroup fixing L, and the inverse maps any closed subgroup of Gal(K/k) H to the fixed field of H. The composition is equal to the identity as described in the lemmas above, and compatibility with the order follows easily.

Special cases :

• isOpen_iff_finite : The fixing subgroup of an intermediate field L is open if and only if L is finite-dimensional.

• normal_iff_isGalois : The fixing subgroup of an intermediate field L is normal if and only if L is Galois.

theorem InfiniteGalois.fixingSubgroup_isClosed {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] (L : IntermediateField k K) [IsGalois k K] : IsClosed ↑L.fixingSubgroup

theorem InfiniteGalois.fixedField_fixingSubgroup {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] (L : IntermediateField k K) [IsGalois k K] : IntermediateField.fixedField L.fixingSubgroup = L

theorem InfiniteGalois.fixedField_bot {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsGalois k K] : IntermediateField.fixedField ⊤ = ⊥

theorem InfiniteGalois.mem_bot_iff_fixed {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsGalois k K] (x : K) : x ∈ ⊥ ↔ ∀ (f : Gal(K/k)), f x = x

theorem InfiniteGalois.mem_range_algebraMap_iff_fixed {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsGalois k K] (x : K) : x ∈ Set.range ⇑(algebraMap k K) ↔ ∀ (f : Gal(K/k)), f x = x

theorem InfiniteGalois.restrict_fixedField {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] (H : Subgroup Gal(K/k)) (L : IntermediateField k K) [Normal k ↥L] : IntermediateField.fixedField H ⊓ L = IntermediateField.lift (IntermediateField.fixedField (Subgroup.map (AlgEquiv.restrictNormalHom ↥L) H))

For a subgroup H of Gal(K/k), the fixed field of the image of H under the restriction to a normal intermediate field E is equal to the fixed field of H in K intersecting with E.

theorem InfiniteGalois.fixingSubgroup_fixedField {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] (H : ClosedSubgroup Gal(K/k)) [IsGalois k K] : (IntermediateField.fixedField ↑H).fixingSubgroup = ↑H

def InfiniteGalois.IntermediateFieldEquivClosedSubgroup {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsGalois k K] : IntermediateField k K ≃o (ClosedSubgroup Gal(K/k))ᵒᵈ

The Galois correspondence from intermediate fields to closed subgroups.

def InfiniteGalois.GaloisInsertionIntermediateFieldClosedSubgroup {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsGalois k K] : GaloisInsertion (⇑OrderDual.toDual ∘ fun (E : IntermediateField k K) => { toSubgroup := E.fixingSubgroup, isClosed' := ⋯ }) ((fun (H : ClosedSubgroup Gal(K/k)) => IntermediateField.fixedField ↑H) ∘ ⇑OrderDual.toDual)

The Galois correspondence as a GaloisInsertion

def InfiniteGalois.GaloisCoinsertionIntermediateFieldSubgroup {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsGalois k K] : GaloisCoinsertion (⇑OrderDual.toDual ∘ fun (E : IntermediateField k K) => E.fixingSubgroup) ((fun (H : Subgroup Gal(K/k)) => IntermediateField.fixedField H) ∘ ⇑OrderDual.toDual)

The Galois correspondence as a GaloisCoinsertion

noncomputable def InfiniteGalois.normalAutEquivQuotient {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsGalois k K] (H : ClosedSubgroup Gal(K/k)) [(↑H).Normal] : Gal(K/k) ⧸ ↑H ≃* Gal(↥(IntermediateField.fixedField ↑H)/k)

If H is a closed normal subgroup of Gal(K / k), then Gal(fixedField H / k) is isomorphic to Gal(K / k) ⧸ H.

theorem InfiniteGalois.normalAutEquivQuotient_apply {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsGalois k K] (H : ClosedSubgroup Gal(K/k)) [(↑H).Normal] (σ : Gal(K/k)) : (normalAutEquivQuotient H) ↑σ = (AlgEquiv.restrictNormalHom ↥(IntermediateField.fixedField ↑H)) σ

theorem InfiniteGalois.isOpen_iff_finite {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] (L : IntermediateField k K) [IsGalois k K] : IsOpen L.fixingSubgroup.carrier ↔ FiniteDimensional k ↥L

theorem InfiniteGalois.normal_iff_isGalois {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] (L : IntermediateField k K) [IsGalois k K] : L.fixingSubgroup.Normal ↔ IsGalois k ↥L

theorem InfiniteGalois.isOpen_and_normal_iff_finite_and_isGalois {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] (L : IntermediateField k K) [IsGalois k K] : IsOpen L.fixingSubgroup.carrier ∧ L.fixingSubgroup.Normal ↔ FiniteDimensional k ↥L ∧ IsGalois k ↥L