normalClosure — Mathlib

English

The normal closure of K over F inside L is the intermediate field generated by all images of K under F-algebra homomorphisms into L. Equivalently, it is the supremum of the ranges of all such embeddings.

Русский

Нормальное замыкание K над F внутри L — это промежуточное поле, порожденное всеми образами K под F-алгебраными гомоморфизмами в L. Эквивалентно, это наибольшее (по включению) поле, порожденное всеми такими вложениями.

LaTeX

$$$\operatorname{normalClosure}(F,K,L)=\bigvee_{f:K\to_{F}L} f.fieldRange$$$

Lean4

/-- The normal closure of `K/F` in `L/F`. -/
@[stacks 0BMF]
noncomputable def normalClosure : IntermediateField F L :=
  ⨆ f : K →ₐ[F] L, f.fieldRange

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