Glue map from finite intermediate field

Stream: new members

[Jiang Jiedong]

Hi everyone,

Is there a theorem in Lean talking about: To define an algebra map on an algebraic field extension (possibly infinite) $L/K$ it suffices to define it on every finite intermediate field $F/K$ compatibly?

The background of this question is a bit lengthy. I am trying to translate the following argument into lean:

Given a field $K$, suppose we have defined a subgroup $G_L$ of each $\text{Gal} (L/K)$ for any finite Galois extension $L/K$, satisfying that for any tower of finite Galois extensions $L/M/K$, the image of $G_L$ in the quotient group $\text{Gal} (M/K)$ is exactly $G_M$. (In my case, this $G_L$ is exactly the upper numbering ramification group.) In other words, $G_L$ is compatible with quotients.

Now I extend the definition of $G_L$ to infinite algebraic Galois extensions $L/K$ by setting

$$G_L = \varprojlim_{L/F/K, F \text{ finite Galois over} K} G_F \\ = \{ s \in \text{Gal} (L/K) | \, \left(s|_F\right) \in G_F, \forall L/F/K, F \text{ finite Galois over} K\}.$$

I want to show that this property of "compatible with quotients" still holds for this extended $G_L$, i.e. let $L_1/L_2/K$ be a tower of (not necessarily finite) Galois extension of fields,

$$\text{image of } G_{L_1} \text{ in quotient group Gal} (L_2/K) = G_{L_2} .$$

Tricky things occur here. Expanding the definition, it suffices to show this key equivalence

$$\begin{align} s \in \text{LHS} & \iff \exist t \in \text{Gal} (L_1/K) (\text{i.e. } \forall F, t|_F \in G_F), \text{ s.t. } t|_{L_2} = s \\ & \iff \forall F, \exists t_F \in G_F, \text{ s.t. } t_F|_{L_2 \cap F} = s|_{L_2 \cap F} \\ & \iff s \in \text{RHS} \end{align}$$

Here $F$ is always taken among $L_1/F/K, \, F \text{ finite Galois over } K$.
The difficulty lies in $(2)$. LHS implies RHS is trivial. For RHS implies LHS, one needs to do the following two things.
(a) To define an element $t_0$ in $\text{Gal} (L_1/K)$ on L, it suffices to find compatible elements $t_{F,0}$ in each $\text{Gal} (F/K)$.
(b) To construct compatible elements $t_{F,0}$ in each $\text{Gal} (F/K)$ from possibly incompatible elements $t_F$, one need to use the fact that finite Galois extensions $F$ is filtered, and each $\text{Gal} (F/K)$ is finite.

Mathematically, the tricky thing here is one must somehow use something "cofiltered limit commutes with finite colimit" like (b) here. I didn't find this category theory theorem CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit in mathlib, although it is claimed in the beginning of Mathlib.CategoryTheory.Filtered.Basic

This is my current attempt. I will be very grateful if anyone has a better roadmap to prove the same goal. Thank you!

[Joël Riou]

The result about the commutation of filtered colimits with finite limits is in the file https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.html

Jiang Jiedong said:

Is there a theorem in Lean talking about: To define an algebra map on an algebraic field extension (possibly infinite) $L/K$ it suffices to define it on every finite intermediate field $F/K$ compatibly?

However, I would recommend you try to formulate this result in Lean without using category theory. Then, you should see that it is largely independent from Galois theory.

[Andrew Yang]

I did something similar here