Main definitions and results

In a field extension K/k

• FiniteGaloisIntermediateField : The type of intermediate fields of K/k that are finite and Galois over k

• adjoin : The finite Galois intermediate field obtained from the normal closure of adjoining a finite s : Set K to k.

TODO

• FiniteGaloisIntermediateField should be a ConditionallyCompleteLattice but isn't proved yet.

structure FiniteGaloisIntermediateField (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] extends IntermediateField k K : Type u_2

The type of intermediate fields of K/k that are finite and Galois over k

• carrier : Set K
• mul_mem' {a b : K} : a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
• one_mem' : 1 ∈ self.carrier
• add_mem' {a b : K} : a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
• zero_mem' : 0 ∈ self.carrier
• algebraMap_mem' (r : k) : (algebraMap k K) r ∈ self.carrier
• inv_mem' (x : K) : x ∈ self.carrier → x⁻¹ ∈ self.carrier
• finiteDimensional : FiniteDimensional k ↥self.toIntermediateField
• isGalois : IsGalois k ↥self.toIntermediateField

instance FiniteGaloisIntermediateField.instCoeIntermediateField (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] : Coe (FiniteGaloisIntermediateField k K) (IntermediateField k K)

instance FiniteGaloisIntermediateField.instCoeSortType (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] : CoeSort (FiniteGaloisIntermediateField k K) (Type u_2)

instance FiniteGaloisIntermediateField.instFiniteDimensionalSubtypeMemIntermediateField (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] (L : FiniteGaloisIntermediateField k K) : FiniteDimensional k ↥L.toIntermediateField

instance FiniteGaloisIntermediateField.instIsGaloisSubtypeMemIntermediateField (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] (L : FiniteGaloisIntermediateField k K) : IsGalois k ↥L.toIntermediateField

theorem FiniteGaloisIntermediateField.val_injective {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] : Function.Injective toIntermediateField

instance FiniteGaloisIntermediateField.instIsGaloisSubtypeMemIntermediateFieldMax {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] (L₁ L₂ : IntermediateField k K) [IsGalois k ↥L₁] [IsGalois k ↥L₂] : IsGalois k ↥(L₁ ⊔ L₂)

Turns the collection of finite Galois IntermediateFields of K/k into a lattice.

instance FiniteGaloisIntermediateField.instFiniteDimensionalSubtypeMemIntermediateFieldMin {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] (L₁ L₂ : IntermediateField k K) [FiniteDimensional k ↥L₁] : FiniteDimensional k ↥(L₁ ⊓ L₂)

instance FiniteGaloisIntermediateField.instFiniteDimensionalSubtypeMemIntermediateFieldMin_1 {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] (L₁ L₂ : IntermediateField k K) [FiniteDimensional k ↥L₂] : FiniteDimensional k ↥(L₁ ⊓ L₂)

instance FiniteGaloisIntermediateField.instIsSeparableSubtypeMemIntermediateFieldMin {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] (L₁ L₂ : IntermediateField k K) [Algebra.IsSeparable k ↥L₁] : Algebra.IsSeparable k ↥(L₁ ⊓ L₂)

instance FiniteGaloisIntermediateField.instIsSeparableSubtypeMemIntermediateFieldMin_1 {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] (L₁ L₂ : IntermediateField k K) [Algebra.IsSeparable k ↥L₂] : Algebra.IsSeparable k ↥(L₁ ⊓ L₂)

instance FiniteGaloisIntermediateField.instIsGaloisSubtypeMemIntermediateFieldMin {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] (L₁ L₂ : IntermediateField k K) [IsGalois k ↥L₁] [IsGalois k ↥L₂] : IsGalois k ↥(L₁ ⊓ L₂)

instance FiniteGaloisIntermediateField.instMax {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] : Max (FiniteGaloisIntermediateField k K)

instance FiniteGaloisIntermediateField.instMin {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] : Min (FiniteGaloisIntermediateField k K)

instance FiniteGaloisIntermediateField.instPartialOrder {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] : PartialOrder (FiniteGaloisIntermediateField k K)

instance FiniteGaloisIntermediateField.instLattice {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] : Lattice (FiniteGaloisIntermediateField k K)

instance FiniteGaloisIntermediateField.instOrderBot {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] : OrderBot (FiniteGaloisIntermediateField k K)

@[simp]

theorem FiniteGaloisIntermediateField.le_iff {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] (L₁ L₂ : FiniteGaloisIntermediateField k K) : L₁ ≤ L₂ ↔ L₁.toIntermediateField ≤ L₂.toIntermediateField

noncomputable def FiniteGaloisIntermediateField.adjoin (k : Type u_1) {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsGalois k K] (s : Set K) [Finite ↑s] : FiniteGaloisIntermediateField k K

The minimal (finite) Galois intermediate field containing a finite set s : Set K in a Galois extension K/k defined as the normal closure of the field obtained by adjoining the set s : Set K to k.

@[simp]

theorem FiniteGaloisIntermediateField.adjoin_val {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsGalois k K] (s : Set K) [Finite ↑s] : (adjoin k s).toIntermediateField = IntermediateField.normalClosure k (↥(IntermediateField.adjoin k s)) K

theorem FiniteGaloisIntermediateField.subset_adjoin (k : Type u_1) {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsGalois k K] (s : Set K) [Finite ↑s] : s ⊆ ↑(adjoin k s).toIntermediateField

theorem FiniteGaloisIntermediateField.adjoin_simple_le_iff {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsGalois k K] {x : K} {L : FiniteGaloisIntermediateField k K} : adjoin k {x} ≤ L ↔ x ∈ L.toIntermediateField

@[simp]

theorem FiniteGaloisIntermediateField.adjoin_map {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsGalois k K] (f : K →ₐ[k] K) (s : Set K) [Finite ↑s] : adjoin k (⇑f '' s) = adjoin k s

@[simp]

theorem FiniteGaloisIntermediateField.adjoin_simple_map_algHom {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsGalois k K] (f : K →ₐ[k] K) (x : K) : adjoin k {f x} = adjoin k {x}

@[simp]

theorem FiniteGaloisIntermediateField.adjoin_simple_map_algEquiv {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsGalois k K] (f : Gal(K/k)) (x : K) : adjoin k {f x} = adjoin k {x}

theorem FiniteGaloisIntermediateField.mem_fixingSubgroup_iff {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] (α : Gal(K/k)) (L : FiniteGaloisIntermediateField k K) : α ∈ L.fixingSubgroup ↔ (AlgEquiv.restrictNormalHom ↥L.toIntermediateField) α = 1