# 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.

source
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
source
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
source
theorem InfiniteGalois.fixedField_bot {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsGalois k K] :
IntermediateField.fixedField ⊤ = ⊥
source
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
source
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`.

source
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
source
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.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
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`

Equations

- InfiniteGalois.GaloisInsertionIntermediateFieldClosedSubgroup = InfiniteGalois.IntermediateFieldEquivClosedSubgroup.toGaloisInsertion

Instances For

source
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`

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
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
source
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
source
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