Main definitions and results

In a field extension K/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.

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.