comap_eq_of_algHom — Mathlib

English

For an F-algebra hom i, the preimage of separableClosure F K under i equals separableClosure F E.

Русский

Для гомоморфизма i выполняется: предобраз разделимого замыкания равен разделимому замыканию.

LaTeX

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

Lean4

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

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