map_eq_of_algEquiv — Mathlib

English

If i is an F-algebra isomorphism E ≃ₐ[F] K, then the image of the perfect closure of E under i equals the perfect closure of K.

Русский

Если i — изоморфизм F-алгебр между E и K, то образ идеального замыкания E под i равен идеальному замыканию K.

LaTeX

$$$(\mathrm{perfectClosure}(F,E)).map i.toAlgHom = \mathrm{perfectClosure}(F,K)$$$

Lean4

/-- If `i` is an `F`-algebra isomorphism of `E` and `K`, then the image of `perfectClosure F E`
under the map `i` is equal to in `perfectClosure F K`. -/
theorem map_eq_of_algEquiv (i : E ≃ₐ[F] K) : (perfectClosure F E).map i.toAlgHom = perfectClosure F K :=
  (map_le_of_algHom i.toAlgHom).antisymm
    (fun x hx ↦ ⟨i.symm x, (map_mem_perfectClosure_iff i.symm.toAlgHom).2 hx, i.right_inv x⟩)

Похожие утверждения