map_mem_separableClosure_iff — Mathlib

English

The comap of separable closure along an algebra homomorphism equals the separable closure of the domain.

Русский

Обратный образ разделимого замыкания по алгебраическому гомоморфизму равен разделимому замыканию области.

LaTeX

$$$(separableClosure F K).comap i = separableClosure F E$$$

Lean4

/-- If `i` is an `F`-algebra homomorphism from `E` to `K`, then `i x` is contained in
`separableClosure F K` if and only if `x` is contained in `separableClosure F E`. -/
theorem map_mem_separableClosure_iff (i : E →ₐ[F] K) {x : E} : i x ∈ separableClosure F K ↔ x ∈ separableClosure F E :=
  by simp_rw [mem_separableClosure_iff, IsSeparable, minpoly.algHom_eq i i.injective]

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