The normal closure of a finite intermediate field

In a Galois extension K/k, the normal closure of a finite intermediate field L is finite and Galois over k. This file records it as an element of FiniteGaloisIntermediateField k K (FiniteGaloisIntermediateField.normalClosure), the smallest one containing L (FiniteGaloisIntermediateField.normalClosure_le_iff). In particular every finite intermediate field lies in a finite Galois one, which is how statements about the finite Galois subextensions of an infinite Galois extension reach its other finite subextensions.

Main definitions

• FiniteGaloisIntermediateField.normalClosure k L: the normal closure of L, as a finite Galois intermediate field.

Main results

• FiniteGaloisIntermediateField.le_normalClosure: L lies in its normal closure.
• FiniteGaloisIntermediateField.normalClosure_le_iff: the normal closure of L is the smallest finite Galois intermediate field containing L.
• IntermediateField.fixingSubgroup_normalClosure: in a Galois extension, the subgroup fixing the normal closure of L is the normal core of the subgroup fixing L.
• IntermediateField.normalClosure_fixedField: in a finite Galois extension, the normal closure of the fixed field of H is the fixed field of the normal core of H.

noncomputable def FiniteGaloisIntermediateField.normalClosure (k : Type u_1) {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsGalois k K] (L : IntermediateField k K) [FiniteDimensional k ↥L] : FiniteGaloisIntermediateField k K

The normal closure of a finite intermediate field L of a Galois extension K/k, as a finite Galois intermediate field. It is the smallest finite Galois intermediate field containing L (normalClosure_le_iff).

@[simp]

theorem FiniteGaloisIntermediateField.normalClosure_toIntermediateField (k : Type u_1) {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsGalois k K] (L : IntermediateField k K) [FiniteDimensional k ↥L] : (normalClosure k L).toIntermediateField = IntermediateField.normalClosure k (↥L) K

The underlying intermediate field of normalClosure k L is the normal closure of L.

theorem FiniteGaloisIntermediateField.le_normalClosure (k : Type u_1) {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsGalois k K] (L : IntermediateField k K) [FiniteDimensional k ↥L] : L ≤ (normalClosure k L).toIntermediateField

A finite intermediate field lies in its normal closure.

theorem FiniteGaloisIntermediateField.normalClosure_le_iff {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsGalois k K] {L : IntermediateField k K} [FiniteDimensional k ↥L] {M : FiniteGaloisIntermediateField k K} : normalClosure k L ≤ M ↔ L ≤ M.toIntermediateField

The universal property of the normal closure: it lies in a finite Galois intermediate field M exactly when L does.

theorem IntermediateField.fixingSubgroup_normalClosure {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsGalois k K] (L : IntermediateField k K) : (normalClosure k (↥L) K).fixingSubgroup = L.fixingSubgroup.normalCore

The subgroup fixing a normal closure is a normal core. In a Galois extension K/k, the subgroup fixing the normal closure of an intermediate field L is the largest normal subgroup fixing L, that is, the normal core of the subgroup fixing L.

theorem IntermediateField.normalClosure_fixedField {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsGalois k K] [FiniteDimensional k K] (H : Subgroup Gal(K/k)) : normalClosure k (↥(fixedField H)) K = fixedField H.normalCore

The normal closure of a fixed field. In a finite Galois extension K/k, the normal closure of the fixed field of a subgroup H of Gal(K/k) is the fixed field of the normal core of H.