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 ∈ 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)

Equations

• FiniteGaloisIntermediateField.instCoeIntermediateField k K = { coe := FiniteGaloisIntermediateField.toIntermediateField }

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)

Equations

• FiniteGaloisIntermediateField.instCoeSortType k K = { coe := fun (L : FiniteGaloisIntermediateField k K) => ↥L.toIntermediateField }

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

theorem FiniteGaloisIntermediateField.val_injective {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] : Function.Injective FiniteGaloisIntermediateField.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.

Equations

• ⋯ = ⋯

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₂)

Equations

• ⋯ = ⋯

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₂)

Equations

• ⋯ = ⋯

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₂)

Equations

• ⋯ = ⋯

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₂)

Equations

• ⋯ = ⋯

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₂)

Equations

• ⋯ = ⋯

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

Equations

• FiniteGaloisIntermediateField.instMax = { max := fun (L₁ L₂ : FiniteGaloisIntermediateField k K) => FiniteGaloisIntermediateField.mk (L₁.toIntermediateField ⊔ L₂.toIntermediateField) }

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

Equations

• FiniteGaloisIntermediateField.instMin = { min := fun (L₁ L₂ : FiniteGaloisIntermediateField k K) => FiniteGaloisIntermediateField.mk (L₁.toIntermediateField ⊓ L₂.toIntermediateField) }

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

Equations

• FiniteGaloisIntermediateField.instLattice = Function.Injective.lattice FiniteGaloisIntermediateField.toIntermediateField ⋯ ⋯ ⋯

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

Equations

• FiniteGaloisIntermediateField.instOrderBot = OrderBot.mk ⋯

@[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 the normal closure of the field obtained by adjoining the set s : Set K to k.

Equations

• FiniteGaloisIntermediateField.adjoin k s = FiniteGaloisIntermediateField.mk (normalClosure k (↥(IntermediateField.adjoin k s)) 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] : (FiniteGaloisIntermediateField.adjoin k s).toIntermediateField = 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 ⊆ ↑(FiniteGaloisIntermediateField.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} : FiniteGaloisIntermediateField.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] : FiniteGaloisIntermediateField.adjoin k (⇑f '' s) = FiniteGaloisIntermediateField.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) : FiniteGaloisIntermediateField.adjoin k {f x} = FiniteGaloisIntermediateField.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 : K ≃ₐ[k] K) (x : K) : FiniteGaloisIntermediateField.adjoin k {f x} = FiniteGaloisIntermediateField.adjoin k {x}