map_le_of_algHom — Mathlib

English

The image of perfectClosure(F,E) under an F-algebra homomorphism i is contained in perfectClosure(F,K).

Русский

Образ идеального замыкания F в E под отображением i содержится в идеальном замыкании F в K.

LaTeX

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

Lean4

/-- If `i` is an `F`-algebra homomorphism from `E` to `K`, then the image of `perfectClosure F E`
under the map `i` is contained in `perfectClosure F K`. -/
theorem map_le_of_algHom (i : E →ₐ[F] K) : (perfectClosure F E).map i ≤ perfectClosure F K :=
  map_le_iff_le_comap.mpr (perfectClosure.comap_eq_of_algHom i).ge

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