English
The map K ↦ normalClosure F K L defines a closure operator on the lattice of intermediate fields between F and L: C(K)=normalClosure F K L, with K ≤ C(K), monotonicity, and idempotency C(C(K))=C(K).
Русский
Отображение K ↦ normalClosure F K L задаёт замыкательный оператор на решетке промежуточных полей между F и L: C(K)=normalClosure F K L, при котором выполняются K ≤ C(K), монотонность и идемпотентность C(C(K))=C(K).
LaTeX
$$$C(K)=\operatorname{normalClosure} F K L$ defines a closure operator, i.e.\; (i) K \le C(K), (ii) K \le K' \Rightarrow C(K) \le C(K'), (iii) C(C(K))=C(K).$$
Lean4
/-- `normalClosure` as a `ClosureOperator`. -/
@[simps]
noncomputable def closureOperator : ClosureOperator (IntermediateField F L)
where
toFun := fun K ↦ normalClosure F K L
monotone' := fun K K' ↦ normalClosure_mono K K'
le_closure' := le_normalClosure
idempotent' := fun K ↦ normalClosure_of_normal (normalClosure F K L)
