Chain of intermediate fields

Stream: Is there code for X?

[Ludwig Monnerjahn]

I want to state the theorem:
$x\in M$ if and only if there is a $n\le 0$ and chain
$K_0 = L_1 \subset L_2 \subset \ldots \subset L_n \subset \mathbb{C}$ of subfields of $\mathbb{C}$ so that $z \in L_n$ and $[L_{i+1}:L_i] = 2 \quad \text{for} \quad i = 0, \dots, n-1$. $K_0$ is $\mathbb{Q}(N)$ for a set $N\subset\mathbb{C}$.

How do I formulate the chain to keep all the properties?

[Daniel Weber]

The chain itself can be a strictly monotone function Fin n → IntermediateField ℚ ℂ

[Floris van Doorn]

One tricky thing is that we want to be able to treat L (i+1) as a module over L i, because we want to talk about the dimension. I believe that is not easy to get from L i ≤ L (i + 1), since that is not a type-class.

[Johan Commelin]

In group theory there is docs#Subgroup.relIndex or something like that. Which computes the index between two subgroups. We could have a relDegree here.

[Johan Commelin]

It just returns junk if the side condition isn't met

[Floris van Doorn]

docs#Subgroup.relindex
That could be useful...

[Antoine Chambert-Loir]

As docs#Subgroup.relindex does for subgroups, you are not forced to return a junk stuff, you could return $[L : K \cap L]$ when you expect that $K\le L$.

[Jz Pan]

Floris van Doorn said:

One tricky thing is that we want to be able to treat L (i+1) as a module over L i, because we want to talk about the dimension. I believe that is not easy to get from L i ≤ L (i + 1), since that is not a type-class.

I think you can use docs#IntermediateField.extendScalars:

-- suppose you have `h : L i ≤ L (i + 1)`
Module.rank (L i) (IntermediateField.extendScalars h)

Meanwhile, I have a WIP IntermediateField.relrank in my computer (edit: #14987).

[Ludwig Monnerjahn]

Is there a way to mark this as a solved topic?

[Ruben Van de Velde]

Please don't (it exists, but doesn't work well)

[Ludwig Monnerjahn]

Ok, thank you.