Main definitions and results #
In a field extension K/k
FiniteGaloisIntermediateField
: The type of intermediate fields ofK/k
that are finite and Galois overk
adjoin
: The finite Galois intermediate field obtained from the normal closure of adjoining a finites : Set K
tok
.
TODO #
FiniteGaloisIntermediateField
should be aConditionallyCompleteLattice
but isn't proved yet.
structure
FiniteGaloisIntermediateField
(k : Type u_1)
(K : Type u_2)
[Field k]
[Field K]
[Algebra k K]
extends
IntermediateField
:
Type u_2
The type of intermediate fields of K/k
that are finite and Galois over k
- carrier : Set K
- one_mem' : 1 ∈ self.carrier
- zero_mem' : 0 ∈ self.carrier
- algebraMap_mem' : ∀ (r : k), (algebraMap k K) r ∈ self.carrier
- finiteDimensional : FiniteDimensional k ↥self.toIntermediateField
- isGalois : IsGalois k ↥self.toIntermediateField
Instances For
theorem
FiniteGaloisIntermediateField.finiteDimensional
{k : Type u_1}
{K : Type u_2}
[Field k]
[Field K]
[Algebra k K]
(self : FiniteGaloisIntermediateField k K)
:
FiniteDimensional k ↥self.toIntermediateField
theorem
FiniteGaloisIntermediateField.isGalois
{k : Type u_1}
{K : Type u_2}
[Field k]
[Field K]
[Algebra k K]
(self : FiniteGaloisIntermediateField k K)
:
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.instIsGaloisSubtypeMemIntermediateFieldSup
{k : Type u_1}
{K : Type u_2}
[Field k]
[Field K]
[Algebra k K]
(L₁ : IntermediateField k K)
(L₂ : IntermediateField k K)
[IsGalois k ↥L₁]
[IsGalois k ↥L₂]
:
Turns the collection of finite Galois IntermediateFields of K/k
into a lattice.
Equations
- ⋯ = ⋯
instance
FiniteGaloisIntermediateField.instFiniteDimensionalSubtypeMemIntermediateFieldInf
{k : Type u_1}
{K : Type u_2}
[Field k]
[Field K]
[Algebra k K]
(L₁ : IntermediateField k K)
(L₂ : IntermediateField k K)
[FiniteDimensional k ↥L₁]
:
FiniteDimensional k ↥(L₁ ⊓ L₂)
Equations
- ⋯ = ⋯
instance
FiniteGaloisIntermediateField.instFiniteDimensionalSubtypeMemIntermediateFieldInf_1
{k : Type u_1}
{K : Type u_2}
[Field k]
[Field K]
[Algebra k K]
(L₁ : IntermediateField k K)
(L₂ : IntermediateField k K)
[FiniteDimensional k ↥L₂]
:
FiniteDimensional k ↥(L₁ ⊓ L₂)
Equations
- ⋯ = ⋯
instance
FiniteGaloisIntermediateField.instIsSeparableSubtypeMemIntermediateFieldInf
{k : Type u_1}
{K : Type u_2}
[Field k]
[Field K]
[Algebra k K]
(L₁ : IntermediateField k K)
(L₂ : IntermediateField k K)
[Algebra.IsSeparable k ↥L₁]
:
Algebra.IsSeparable k ↥(L₁ ⊓ L₂)
Equations
- ⋯ = ⋯
instance
FiniteGaloisIntermediateField.instIsSeparableSubtypeMemIntermediateFieldInf_1
{k : Type u_1}
{K : Type u_2}
[Field k]
[Field K]
[Algebra k K]
(L₁ : IntermediateField k K)
(L₂ : IntermediateField k K)
[Algebra.IsSeparable k ↥L₂]
:
Algebra.IsSeparable k ↥(L₁ ⊓ L₂)
Equations
- ⋯ = ⋯
instance
FiniteGaloisIntermediateField.instIsGaloisSubtypeMemIntermediateFieldInf
{k : Type u_1}
{K : Type u_2}
[Field k]
[Field K]
[Algebra k K]
(L₁ : IntermediateField k K)
(L₂ : IntermediateField k K)
[IsGalois k ↥L₁]
[IsGalois k ↥L₂]
:
Equations
- ⋯ = ⋯
instance
FiniteGaloisIntermediateField.instSup
{k : Type u_1}
{K : Type u_2}
[Field k]
[Field K]
[Algebra k K]
:
Equations
- FiniteGaloisIntermediateField.instSup = { sup := fun (L₁ L₂ : FiniteGaloisIntermediateField k K) => FiniteGaloisIntermediateField.mk (L₁.toIntermediateField ⊔ L₂.toIntermediateField) }
instance
FiniteGaloisIntermediateField.instInf
{k : Type u_1}
{K : Type u_2}
[Field k]
[Field K]
[Algebra k K]
:
Equations
- FiniteGaloisIntermediateField.instInf = { inf := 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]
:
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]
:
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₁ : FiniteGaloisIntermediateField k K)
(L₂ : FiniteGaloisIntermediateField k K)
:
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]
:
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
Instances For
@[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.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