English
If i is an F-algebra homomorphism from E to K, then an element x maps into perfectClosure(F,K) exactly when x lies in perfectClosure(F,E).
Русский
Пусть i: E →_F K — алгебровый однородник. Тогда i(x) ∈ perfectClosure(F,K) тогда и только тогда, когда x ∈ perfectClosure(F,E).
LaTeX
$$$i(x) \in \mathrm{perfectClosure}(F,K) \iff x \in \mathrm{perfectClosure}(F,E)$$$
Lean4
/-- If `i` is an `F`-algebra homomorphism from `E` to `K`, then `i x` is contained in
`perfectClosure F K` if and only if `x` is contained in `perfectClosure F E`. -/
theorem map_mem_perfectClosure_iff (i : E →ₐ[F] K) {x : E} : i x ∈ perfectClosure F K ↔ x ∈ perfectClosure F E :=
by
simp_rw [mem_perfectClosure_iff]
refine ⟨fun ⟨n, y, h⟩ ↦ ⟨n, y, ?_⟩, fun ⟨n, y, h⟩ ↦ ⟨n, y, ?_⟩⟩
· apply_fun i using i.injective
rwa [AlgHom.commutes, map_pow]
simpa only [AlgHom.commutes, map_pow] using congr_arg i h
