English
Under appropriate finiteness and normality hypotheses (e.g., K ∩ L = F and E/Galois), the restriction map Aut_L(E) → Aut_K(E) is surjective.
Русский
При надлежащих условиях конечности и нормальности (например, K ∩ L = F и E галуа над L), отображение ограничение Автоморфизмов галуа сюръективно.
LaTeX
$$$K\cap L = F \Rightarrow \operatorname{restrictRestrictAlgEquivMapHom}_{F}(K,L,E) \text{ is surjective}$ (при дополнительных предположениях).$$
Lean4
theorem restrictRestrictAlgEquivMapHom_surjective [FiniteDimensional F K] [FiniteDimensional L E] [IsGalois L E]
(h : K ⊓ L = ⊥) : Function.Surjective (restrictRestrictAlgEquivMapHom F K L E) :=
by
suffices fixedField (restrictRestrictAlgEquivMapHom F K L E).range = ⊥ from
MonoidHom.range_eq_top.mp <|
fixingSubgroup_fixedField (restrictRestrictAlgEquivMapHom F K L E).range ▸ this ▸ fixingSubgroup_bot
refine eq_bot_iff.mpr fun ⟨x, hx₁⟩ hx₂ ↦ ?_
obtain ⟨⟨y, hy⟩, rfl⟩ : x ∈ Set.range (algebraMap L E) :=
by
refine mem_bot.mp <| (IsGalois.mem_bot_iff_fixed _).mpr fun φ ↦ ?_
rw [← restrictRestrictAlgEquivMapHom_apply K L φ ⟨x, hx₁⟩]
rw [mem_fixedField_iff] at hx₂
exact congr_arg ((↑) : K → E) <| hx₂ (restrictRestrictAlgEquivMapHom F K L E φ) ⟨φ, rfl⟩
obtain ⟨z, rfl⟩ : y ∈ (⊥ : IntermediateField F E) := h ▸ mem_inf.mpr ⟨hx₁, hy⟩
exact mem_bot.mp ⟨z, rfl⟩
