# 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 $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 (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