intermediate_field.lifts

Stream: new members

[Xavier Roblot]

I am trying to make sense of how intermediate_field.lifts works and more precisely intermediate_field.lifts.lift_of_splits.

If I understand correctly, for fields $F$, $E$, $K$ with $E$ and $K$ being $F$-algebras, intermediate_fields.lifts is the collection of $F$-algebra maps $L \to K$ extending the natural map $F \to K$ to some field $L$ with $F \subseteq L \subseteq E$.

Now, the doc for intermediate_field.lifts.lift_of_splits says: assuming that (x : intermediate_field.lifts F E K) and s : E is integral over $F$ and its minimal polynomial splits in $K$ :
Extend a lift x : lifts F E K to an element s : E whose conjugates are all in K.
I am not really sure what that means in this context since I thought x was a map. I am getting this all wrong?

[Eric Rodriguez]

x is not a map, it's a dependent pair of both an intermediate field and a map. if you dig into the definition a bit, you can see that the intermediate field ends up being x.1⟮s⟯ for the new map (modulo technical details); that is, if the original map is L -> K then this new map is L(s) -> K.