English
Let k ⊆ E ⊆ K be a tower with E/K normal; for an intermediate field L ⊆ E, the fixing subgroup after mapping L to K equals the preimage of the fixing subgroup of L in E under the natural restriction map Aut(K/k) → Aut(E/k).
Русский
Пусть k ⊆ E ⊆ K — тessel; для промежуточного поля L ⊆ E фиксационная подгруппа после отображения L в K равна предобразу фиксационной подгруппы L над E через естественное отображение Aut(K/k) → Aut(E/k).
LaTeX
$$$\\,(L.map (IsScalarTower.toAlgHom k E K)).fixingSubgroup = L.fixingSubgroup \\, .\\!comap\\, (AlgEquiv.restrictNormalHom (F := k) (K_1 := K) E).$$$
Lean4
/-- If `K / E / k` is a field extension tower with `E / k` normal,
`L` is an intermediate field of `E / k`, then the fixing subgroup of `L` viewed as an
intermediate field of `K / k` is equal to the preimage of the fixing subgroup of `L` viewed as an
intermediate field of `E / k` under the natural map `Aut(K / k) → Aut(E / k)`
(`AlgEquiv.restrictNormalHom`). -/
theorem map_fixingSubgroup [Normal k E] :
(L.map (IsScalarTower.toAlgHom k E K)).fixingSubgroup =
L.fixingSubgroup.comap (AlgEquiv.restrictNormalHom (F := k) (K₁ := K) E) :=
by
ext f
simp only [Subgroup.mem_comap, mem_fixingSubgroup_iff]
constructor
· rintro h x hx
change f.restrictNormal E x = x
apply_fun _ using (algebraMap E K).injective
rw [AlgEquiv.restrictNormal_commutes]
exact h _ ⟨x, hx, rfl⟩
· rintro h _ ⟨x, hx, rfl⟩
replace h := congr(algebraMap E K $(show f.restrictNormal E x = x from h x hx))
rwa [AlgEquiv.restrictNormal_commutes] at h
