English
If i is an F-algebra isomorphism between E and K, then the algebraic closures over F are isomorphic via i; precisely, the image of algebraicClosure F E under i equals algebraicClosure F K.
Русский
Если i — изоморфизм E и K как F-алгебр, то их алгебраические замыкания над F совпадают по структуре через i; образ algebraicClosure F E равен algebraicClosure F K.
LaTeX
$$$ (\\operatorname{algebraicClosure}_F(E)).map(i) = \\operatorname{algebraicClosure}_F(K) $$$
Lean4
/-- If `i` is an `F`-algebra isomorphism of `E` and `K`, then the image of `algebraicClosure F E`
under the map `i` is equal to `algebraicClosure F K`. -/
theorem map_eq_of_algEquiv (i : E ≃ₐ[F] K) : (algebraicClosure F E).map i = algebraicClosure F K :=
(map_le_of_algHom i.toAlgHom).antisymm (fun x h ↦ ⟨_, (map_mem_algebraicClosure_iff i.symm).2 h, by simp⟩)
