Zulip Chat Archive

Stream: new members

Topic: intermediate_field.lifts

Xavier Roblot (May 26 2022 at 14:36):

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 FF, EE, KK with EE and KK being FF-algebras, intermediate_fields.lifts is the collection of FF-algebra maps LKL \to K extending the natural map FKF \to K to some field LL with FLEF \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 FF and its minimal polynomial splits in KK :
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 (May 26 2022 at 15:06):

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.

Last updated: Dec 20 2023 at 11:08 UTC