Normal Closure

Stream: maths

[Riccardo Brasca]

Currently the type of the normal closure, IntermediateField.normalClosure is

noncomputable def IntermediateField.normalClosure (F : Type u_1) (K : Type u_2) (L : Type u_3)
    [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] :
  IntermediateField F L := ...

In particular there are three fields F, K and L and two extensions K/F and L/F. The result is an IntermediateField F L. Note that we don't require L to be an K-algebra.

Do we really want such a generality rather than having a tower of fields L/K/F? I am asking because in this case the normal closure could be an IntermediateField K L, something that looks more reasonable to me. I suspect that the current generality is one the cause of the slowness of #28797: indeed the definition of normalClosure.algebra (that requires to have a tower) is rather indirect and would be automatic if the normal closure is an IntermediateField K L.

[Riccardo Brasca]

Another possibility is to just forget all this IntermediateField and defining the normal closure as a type with the required instances (as we did for the ring of integers), but I don't know how much work is needed.

[Filippo A. E. Nuccio]

Concerning having it only as an IntermediateField K L I think that this would not be a good idea, because as it is now you can claim that IntermediateField.normalClosureis Galois over F but if you throw it away you lose some mathematical information. On the other hand, I do not see any counterargument for adding that L be a K-algebra.

[Riccardo Brasca]

Ah yes, for Galois considerations it is actually better as it is.