comap_eq_of_algHom — Mathlib

English

The comap of algebraicClosure F K along any F-algebra homomorphism i: E →ₐ[F] K equals algebraicClosure F E.

Русский

Обратное отображение algebraicClosure F K по гомоморфизму i равно algebraicClosure F E.

LaTeX

$$$$\text{IntermediateField.comap } i (\text{algebraicClosure } F K) = \text{algebraicClosure } F E$$$$

Lean4

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

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