English
Let K/k and E be normal, and L an intermediate field of E/k. Then the index of the fixing subgroup after mapping L to K equals the index of L fixingSubgroup in E.
Русский
Пусть K/k и E нормальны, L — промежуточное поле E/k. Тогда индекс фиксационной подгруппы после отображения L в K равен индексу фиксационной подгруппы L в E.
LaTeX
$$$ (L.map (IsScalarTower.toAlgHom k E K)).fixingSubgroup.index = L.fixingSubgroup.index $$$
Lean4
/-- If `K / E / k` is a field extension tower with `E / k` and `K / k` normal,
`L` is an intermediate field of `E / k`, then the index of the fixing subgroup of `L` viewed as an
intermediate field of `K / k` is equal to the index of the fixing subgroup of `L` viewed as an
intermediate field of `E / k`. -/
theorem map_fixingSubgroup_index [Normal k E] [Normal k K] :
(L.map (IsScalarTower.toAlgHom k E K)).fixingSubgroup.index = L.fixingSubgroup.index := by
rw [L.map_fixingSubgroup K, L.fixingSubgroup.index_comap_of_surjective (AlgEquiv.restrictNormalHom_surjective _)]
