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.

• finGaloisGroup L : The (finite) Galois group Gal(L/k) associated to a L : FiniteGaloisIntermediateField k K L.

• finGaloisGroupMap : For FiniteGaloisIntermediateField s L₁ and L₂ with L₂ ≤ L₁ giving the restriction of Gal(L₁/k) to Gal(L₂/k)

• finGaloisGroupFunctor : Mapping FiniteGaloisIntermediateField ordered by inverse inclusion to its corresponding Galois Group as FiniteGrp.

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 : 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

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₂] : IsGalois k ↥(L₁ ⊔ 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₂] : IsGalois k ↥(L₁ ⊓ L₂)

Equations

• ⋯ = ⋯

instance FiniteGaloisIntermediateField.instSup {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] : Sup (FiniteGaloisIntermediateField 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] : Inf (FiniteGaloisIntermediateField 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] : 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₁ : FiniteGaloisIntermediateField k K) (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}

def FiniteGaloisIntermediateField.finGaloisGroup {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] (L : FiniteGaloisIntermediateField k K) : FiniteGrp.{u_2}

The (finite) Galois group Gal(L / k) associated to a L : FiniteGaloisIntermediateField k K L.

Equations

• L.finGaloisGroup = FiniteGrp.of (↥L.toIntermediateField ≃ₐ[k] ↥L.toIntermediateField)

noncomputable def finGaloisGroupMap {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] {L₁ : (FiniteGaloisIntermediateField k K)ᵒᵖ} {L₂ : (FiniteGaloisIntermediateField k K)ᵒᵖ} (le : L₁ ⟶ L₂) : (Opposite.unop L₁).finGaloisGroup ⟶ (Opposite.unop L₂).finGaloisGroup

For FiniteGaloisIntermediateField s L₁ and L₂ with L₂ ≤ L₁ the restriction homomorphism from Gal(L₁/k) to Gal(L₂/k)

Equations

• finGaloisGroupMap le = FiniteGrp.ofHom (AlgEquiv.restrictNormalHom ↥(Opposite.unop L₂).toIntermediateField)

@[simp]

theorem finGaloisGroupMap.map_id {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] (L : (FiniteGaloisIntermediateField k K)ᵒᵖ) : finGaloisGroupMap (CategoryTheory.CategoryStruct.id L) = CategoryTheory.CategoryStruct.id (Opposite.unop L).finGaloisGroup

@[simp]

theorem finGaloisGroupMap.map_comp {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] {L₁ : (FiniteGaloisIntermediateField k K)ᵒᵖ} {L₂ : (FiniteGaloisIntermediateField k K)ᵒᵖ} {L₃ : (FiniteGaloisIntermediateField k K)ᵒᵖ} (f : L₁ ⟶ L₂) (g : L₂ ⟶ L₃) : finGaloisGroupMap (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (finGaloisGroupMap f) (finGaloisGroupMap g)

noncomputable def finGaloisGroupFunctor (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] : CategoryTheory.Functor (FiniteGaloisIntermediateField k K)ᵒᵖ FiniteGrp.{u_2}

The functor from FiniteGaloisIntermediateField (ordered by reverse inclusion) to FiniteGrp, mapping each intermediate field K/L/k to Gal (L/k).

Equations

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