English
The finite Galois intermediate field L over k of K has an associated finite Galois group Gal(L/k).
Русский
У конечного Галуа-подполя L/k существует соответствующая конечная Галуа-группа Gal(L/k).
LaTeX
$$finGaloisGroup (L) : FiniteGrp$$
Lean4
/-- For `FiniteGaloisIntermediateField` s `L₁` and `L₂` with `L₂ ≤ L₁`
the restriction homomorphism from `Gal(L₁/k)` to `Gal(L₂/k)` -/
noncomputable def finGaloisGroupMap {L₁ L₂ : (FiniteGaloisIntermediateField k K)ᵒᵖ} (le : L₁ ⟶ L₂) :
L₁.unop.finGaloisGroup ⟶ L₂.unop.finGaloisGroup :=
haveI : Normal k L₂.unop := IsGalois.to_normal
letI : Algebra L₂.unop L₁.unop := RingHom.toAlgebra (Subsemiring.inclusion <| leOfHom le.1)
haveI : IsScalarTower k L₂.unop L₁.unop := IsScalarTower.of_algebraMap_eq (congrFun rfl)
FiniteGrp.ofHom (AlgEquiv.restrictNormalHom L₂.unop)
