English
Given a Normal F E, there is a canonical F-algebra homomorphism from the range of the restriction of an F-algebra homomorphism K1→K2 to itself, effectively restricting ϕ to the image under the normal subfield.
Русский
При условии Normal F E существует канонический F-алгебровый однородный гомоморфизм от образа ограничения гомоморфизма F-алгебр K1→K2 к самому образу, т.е. ограничение ϕ на нормальное подполе.
LaTeX
$$$\exists \rho:\operatorname{range}(\mathrm{toAlgHom}\ F\ E\ K_1) \to_{F}\operatorname{range}(\mathrm{toAlgHom}\ F\ E\ K_2)$ с нужными свойствами, не нарушающими структуру, такая что $\rho(\varphi|_{\text{range}})=\varphi$ на соответствующем образе.$$
Lean4
/-- Restrict algebra homomorphism to image of normal subfield -/
def restrictNormalAux [h : Normal F E] : (toAlgHom F E K₁).range →ₐ[F] (toAlgHom F E K₂).range
where
toFun
x :=
⟨ϕ x, by
suffices (toAlgHom F E K₁).range.map ϕ ≤ _ by exact this ⟨x, Subtype.mem x, rfl⟩
rintro x ⟨y, ⟨z, hy⟩, hx⟩
rw [← hx, ← hy]
apply minpoly.mem_range_of_degree_eq_one E
refine
Or.resolve_left (h.splits z).def (minpoly.ne_zero (h.isIntegral z)) (minpoly.irreducible ?_)
(minpoly.dvd E _ (by simp [aeval_algHom_apply]))
simp only [AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom]
suffices IsIntegral F _ by exact this.tower_top
exact ((h.isIntegral z).map <| toAlgHom F E K₁).map ϕ⟩
map_zero' := Subtype.ext (map_zero _)
map_one' := Subtype.ext (map_one _)
map_add' x y := Subtype.ext <| by simp
map_mul' x y := Subtype.ext <| by simp
commutes' x := Subtype.ext (ϕ.commutes x)
