comap_eq_of_algHom — Mathlib

English

For any F-algebra hom i: E → K, the preimage of perfectClosure(F,K) under i equals perfectClosure(F,E).

Русский

Для любого гомоморфизма i: E → K над F предобразPerfectClosure(F,K) равен PerfectClosure(F,E).

LaTeX

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

Lean4

/-- If `i` is an `F`-algebra homomorphism from `E` to `K`, then the preimage of `perfectClosure F K`
under the map `i` is equal to `perfectClosure F E`. -/
theorem comap_eq_of_algHom (i : E →ₐ[F] K) : (perfectClosure F K).comap i = perfectClosure F E :=
  by
  ext x
  exact map_mem_perfectClosure_iff i

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