algEquivOfAlgEquiv — Mathlib

English

If E and K are isomorphic as F-algebras, then their perfect closures are isomorphic as F-algebras.

Русский

Если E и K изоморфны как F-алгебры, то их идеальные замыкания изоморфны как F-алгебры.

LaTeX

$$$\mathrm{PerfectClosure}(F,E) \cong_F \mathrm{PerfectClosure}(F,K)$$$

Lean4

/-- If `E` and `K` are isomorphic as `F`-algebras, then `perfectClosure F E` and
`perfectClosure F K` are also isomorphic as `F`-algebras. -/
def algEquivOfAlgEquiv (i : E ≃ₐ[F] K) : perfectClosure F E ≃ₐ[F] perfectClosure F K :=
  (intermediateFieldMap i _).trans (equivOfEq (map_eq_of_algEquiv i))

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