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

source
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

Instances For

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

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

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

source
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₂)
source
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₂)
source
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₂)
source
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₂)
source
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₂)
source
instance FiniteGaloisIntermediateField.instMax {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] :
Max (FiniteGaloisIntermediateField k K)
Equations

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

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

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

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

source
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 = { bot := { toIntermediateField := ⊥, finiteDimensional := ⋯, isGalois := ⋯ }, bot_le := ⋯ }

source
@[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
source
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`.

Equations

- FiniteGaloisIntermediateField.adjoin k s = { toIntermediateField := IntermediateField.normalClosure k (↥(IntermediateField.adjoin k s)) K, finiteDimensional := ⋯, isGalois := ⋯ }

Instances For

source
@[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
source
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
source
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
source
@[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
source
@[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}
source
@[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}
source
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