English
In a tower F ⊆ K ⊆ L with L normal over F, the normal closure of K in L over F equals the supremum of all images K.map f as f runs over all F-algebra homomorphisms f: L → L.
Русский
В тензоре F ⊆ K ⊆ L, где L нормально над F, нормальное замыкание K в L над F равно наибольшему элементу, получаемому как образ K под все гомоморфизмы F-алгебр из L в L.
LaTeX
$$$\operatorname{normalClosure} F K L = \bigvee_{f: L \to_{F} L} K^{f}$$$
Lean4
theorem normalClosure_def' : normalClosure F K L = ⨆ f : L →ₐ[F] L, K.map f :=
by
refine (normalClosure_def F K L).trans (le_antisymm (iSup_le (fun f ↦ ?_)) (iSup_le (fun f ↦ ?_)))
· exact le_iSup_of_le (f.liftNormal L) (fun b ⟨a, h⟩ ↦ ⟨a, a.2, h ▸ f.liftNormal_commutes L a⟩)
· exact le_iSup_of_le (f.comp K.val) (fun b ⟨a, h⟩ ↦ ⟨⟨a, h.1⟩, h.2⟩)
