project: normal closures

Stream: LftCM22

[Kevin Buzzard]

Right now Lean has normal extensions of fields, and it has algebraic closures, but it doesn't have the theory of normal closures. I made a start on this on a normal closure branch and also on branch#kbuzzard/normal_universal where I started a more foundational attempt. This is actually holding up a project of mine. Would anyone like to take it on?

[Thomas Browning]

Looking into it.

[Kevin Buzzard]

I think @María Inés de Frutos Fernández wanted something like

noncomputable! def normal_closure : intermediate_field K (algebraic_closure L) :=
supr (λ φ : (L →ₐ[K] algebraic_closure L), φ.field_range) -- or whatever

namespace normal_closure

lemma is_normal (h : algebra.is_algebraic K L) : normal K (normal_closure K L) := sorry

lemma is_finite_dimensional [finite_dimensional K L] : finite_dimensional K (normal_closure K L) :=
sorry

end normal_closure

[Kevin Buzzard]

but she might be more flexible with the algebraic closure thing. Oh she also wanted a map L -> normal_closure K L