Galois invariants

Stream: new members

[Jiang Jiedong]

Hi, everyone!
I was trying to play with the Galois theory in mathlib3. I found that my thoughts are deeply based on set theory, as a result, I'm confused at the follow problem:
I was trying to formalize the following kind of theorems in Lean, namely 'Let K be a field, K^alg denotes its algebraic closure. If x \in K^alg is an elements satisfies some condition, then x falls in K'. However, the type of x is x : algebraic_closure K. So it does not make sense to state x : K. I wonder what is the best way to state this theorem? I find that I can use intermediate_field K {x} = ⊥. Is there other ways to deal with it?

More background: the final goal I was trying to do is the following theorem
'Let C_p be the completion of the algebraic closure of Q_p, the Galois action of Gal(Q_p^alg / Q_p) extends continuous to C_p. For any finite extension K/Q_p, the fixed subfield of Gal(Q_p^alg / K) in C_p is K itself.'
The proof argues with an arbitrary fixed elements x \in C_p and shows it falls in K. So my plan is to prove a lemma ∀ x : C_p, ... → intermediate_field K {x} = ⊥ , where ... represents 'x fixed by Gal(Q_p^alg / K)'. My problem is how should the final theorem be stated and how to use this to lemma to deduce the final theorem?

[Kevin Buzzard]

@María Inés de Frutos Fernández has formalised $\mathbb{C}_p$ plus its Galois action but the work hasn't hit mathlib yet. But we don't have the computation of the fixed field (which is delicate, it needs some of the theory of deeply ramified extensions as far as I know, although all of the pieces should be there to make this a tractable project).

As for stating the theorem, I would use a type for a base p-adic field, another type for an algebraic closure, a third type for the completion, and then you get a map from intermediate subfields of the alg closure to intermediate subfields of the completion, and you would state the theorems as being properties of this map.

[Riccardo Brasca]

I wouldn't say this is a problem of type theory. Even in set theory field extension are not inclusions. You should use the map from the "small" field to the "big" one.

[Riccardo Brasca]

Note that you may be tempted to say "everything lives in the algebraic closure" and then use subfields of it, but this is going to make you suffer: for example, even if ℚ is inside ℂ, there is no way ℚ[X]/(x^2+1) is a subfield of ℂ (of course there is a "canonical" injective morphism, but you don't want to write it down every time).

[Kevin Buzzard]

@Jiang Jiedong one mathlib-idiomatic way of making the statement would look something like this:

import Mathlib.NumberTheory.Padics.PadicNumbers -- p-adic numbers
import Mathlib.FieldTheory.IsAlgClosed.Basic -- algebraic closures
import Mathlib.FieldTheory.Galois -- Galois theory

-- let p be a prime
variable {p : ℕ} [Fact (p.Prime)]

-- let K be a field, finite-dimensional over Q_p
variable {K : Type} [Field K] [Algebra ℚ_[p] K] [Module.Finite ℚ_[p] K]

-- Let Kbar be an algebraic closure of K
variable {Kbar : Type} [Field Kbar] [Algebra K Kbar] [IsAlgClosure K Kbar]

section not_in_mathlib
-- Some sorried stuff until Maria Ines' work makes it into mathlib4:

def Cp : Type := sorry -- completion of Kbar (the hard part is extending the norm
-- to get the metric to complete with)

-- Cp is a field
instance : Field Cp := sorry

-- Cp is a Kbar-algebra and hence a K-algebra
instance : Algebra Kbar Cp := sorry

-- Galois action extends canonically
instance : DistribMulAction (Kbar ≃ₐ[K] Kbar) Cp := sorry

end not_in_mathlib

-- canonical injection, probably in mathlib already but I couldn't find it immediately
-- Filling in sorries should be a nice exercise, and perhaps some thought should be given
-- about the correct generality of this construction
def i : IntermediateField K Kbar → Subalgebra K Cp := fun L ↦ {
  carrier := (algebraMap Kbar Cp) '' L
  mul_mem' := sorry
  one_mem' := sorry
  add_mem' := sorry
  zero_mem' := sorry
  algebraMap_mem' := sorry
}

open IntermediateField -- for `fixingSubgroup`

theorem Jiedong (L : IntermediateField K Kbar) :
  let H : Subgroup (Kbar ≃ₐ[K] Kbar) := fixingSubgroup L
  -- Theorem: the subset of C_p fixed by H is no bigger than L
  {x : Cp | ∀ h ∈ H, h • x = x } = i L := by
  -- Proof: hard exercise
  sorry

[Jiang Jiedong]

Riccardo Brasca said:

I wouldn't say this is a problem of type theory. Even in set theory field extension are not inclusions. You should use the map from the "small" field to the "big" one.

Thank you! You are right, I should not think every finite extension K of Q_p as a subset of C_p, instead I should choose a specific field map from K into C_p, and state the theorem as the Galois invariant is the image of K. (as long as I show that the completion of algebraic closure of K is isomorphic to C_p so that the Galois action extends to C_p)

[Jiang Jiedong]

@Kevin Buzzard Thank you so much for you help !!! Your code definitely clears my thoughts. I've already written something about how to extend the norm to Q_p bar. And another key ingredient is to formalize the so called Krasner's lemma and Ax-Sen's lemma, which is exactly the reason I ask this question.

[Riccardo Brasca]

You should check with María Inés, you are probably redoing her work (at least a part of her work).

[Johan Commelin]

Which isn't necessarily a problem of course. It's a great way to learn Lean. (-;

[Kevin Buzzard]

My understanding is that Maria Ines didn't do Krasner yet but it's certainly accessible. I don't know how much we have about differents and discriminants of extensions of local fields though, that might be something which needs developing. I know we have $ef=n$ but I'm not sure we have much more.

[Jiang Jiedong]

Riccardo Brasca said:

You should check with María Inés, you are probably redoing her work (at least a part of her work).

Oh thank you for your advice. My original plan was to write about C_p in lean3 not so seriously (leaving many sorries) for now, as an exercise to learn Lean. I want to write more seriously in Lean4 in the future and I will certainly discuss with María Inés about it in the future. I think it may requires more comprehensive development in fundamental theorems in number theory (e. g. theory of valuations under Galois extensions, ramification groups, ...) first before a comprehensive theory of C_p.

[María Inés de Frutos Fernández]

Hi! My definition of C_p is here, and the Galois action is defined here, but as Kevin pointed out, we still have not computed the fixed field.
There are definitely goals related to C_p that are still missing but accessible (for example, that C_p is algebraically closed and that Q_p^alg is not complete). In any case, I would be happy to discuss at any point!