Properties of prime subfield

Stream: Is there code for X?

[Scott Carnahan]

I was thinking about showing that Galois groups of extensions of finite fields are cyclic and generated by Frobenius. As a first step, I thought I would show:

import Mathlib

example (p : ℕ) [Fact (Nat.Prime p)] {K : Type*} [Field K] [CharP K p]
    {x : K} : x ^ p = x ↔ x ∈ (⊥ : Subfield K) := by
  sorry

Do we have anything like this?

[Scott Carnahan]

Oh, I see this was discussed in #mathlib4 > Are there theorems about prime fields in Mathlib4? but without much conclusion.

[Adam Topaz]

Mathlib doesn’t have something like this as far as I’m aware. But we should! And the analogous characterization of $\mathbb{F}_q$ as the roots of x^q-x in an extension of $\mathbb{F}_q$.

[Kevin Buzzard]

In FLT we need that the absolute Galois group of a finite field is topologically isomorphic to $\widehat{\Z}$ with Frobenius a topological generator. Right now I'm still on the fence about whether to state this with a bespoke Zhat, with some kind of completion of Z, or with something coming from the finite adele part of the library

[David Loeffler]

We should definitely have a type for $\widehat{\mathbb{Z}}$ defined somewhere, and a proof that it is a completion of $\mathbb{Z}$ and an open subring of the finite adeles (which of those we take to be "the" definition is an implementation detail).

[Kevin Buzzard]

Right now we have FiniteIntegralAdeles \Z \Q (defined as the product of completions over HeightOneSpectrum so it will be difficult to relate to anything) and also an ad-hoc definition in FLT which is very low-level and has been nice to work with. There may be others, e.g. maybe one coming from I-adic completions somehow? Do we have profinite completion of e.g. a group?

[Adam Topaz]

We do have profinite groups, so presumably we should create a profinite analogue of docs#IsFreeGroup for profinite groups. Then $\widehat{\Z}$ is any profinite group satisfying IsProfiniteFreeGroup Unit.

[Kevin Buzzard]

Aha, yes that sounds right, so then we have Zhat and IsZhat.

[Kevin Buzzard]

This takes us back on topic: how do we say "I'm cyclic and generated by Frobenius"? It sounds initially like a Prop, and IsCyclic is a Prop, but here probably want the isomorphism from ZMod n sending 1 to Frobenius, which is data.

[Sébastien Gouëzel]

For free groups, we have a Prop predicate IsFreeGroup G, and a data FreeGroupBasis ι G. You could have the same here.

[Scott Carnahan]

The characterization of the prime subfield is now #22843. Finite Galois group computations will be in a follow-up.