preimage of quotient galois group

Stream: new members

[Junjie Bai]

Suppose L/K galois extension, and G its galois group, H normal subgroup of G, t is element of G/H, how can i write the preimage of t in G?

[Johan Commelin]

Do you know how to write down the quotient map G -> G/H?

[Kevin Buzzard]

In other words, can you formalise the question? Questions of the form "please fill in this sorry in this fully working code" are usually answered much more quickly than questions in natural language.

[Junjie Bai]

I don't know how to write it in a galois group. I try to use the function "QuotientGroup.mk' ", but i can't state that H is normal if I state the intermediateField K' first, or I can't state K' as a field(I need to use K' in the following steps) if I state H first.
I can understand the question in natural language, but I can't formalise it.

[Johan Commelin]

So let's go with your original formulation, in which you state H first.

[Johan Commelin]

Can you then get the preimage of t as you want?

[Junjie Bai]

I try to do it in this way:

open QuotientGroup
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable {G : Group (L ≃ₐ[K] L)} {H : Subgroup (L ≃ₐ[K] L)} [Subgroup.Normal H]

example (t : (L ≃ₐ[K] L) ⧸ H) : ((mk' H)⁻¹' t) := by sorry

but it seems wrong becuse t is not type of Set

[Johan Commelin]

Good start. So now you can write {t}

[Johan Commelin]

But {G : Group (L ≃ₐ[K] L)} is suspicious.

[Junjie Bai]

OK, I think that works.

[Johan Commelin]

You are assuming a brand-new-unrelated group structure on the automorphisms

[Johan Commelin]

And there will be no guarantee that the unit element of the group structure that you call G will be the identity map, etc...

[Johan Commelin]

So just leave out that variable, because it isn't doing anything useful.

[Junjie Bai]

Yes, I realize that, I think this version can get the preimage of t

open QuotientGroup
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable {H : Subgroup (L ≃ₐ[K] L)} [Subgroup.Normal H]

example (t : (L ≃ₐ[K] L) ⧸ H) : ((mk' H)⁻¹' {t}) := by sorry

[Junjie Bai]

But in this way I can't use the Field structure of K', which is the FixedField of H, it is a IntermediaField, is there any way to solve this?

[Johan Commelin]

Can you please be a bit more explicit?

[Johan Commelin]

Lean knows that FixedFields are Fields

[Junjie Bai]

I want to state the lemma4 of <Local fields> serre chap 4, sec 3, I need to get the preimage of a element in the quotient group of the galois group, suppose they are s_i, I want to get the sup of their image of the function i_G, where G is the galois group, and i_G is the identify function of the ramification group.

[Johan Commelin]

I don't have Serre's book nearby atm. Can you please copy the (informal) statement here on zulip?

[Junjie Bai]

sure, here is the proposition I want to state:
Let $\theta \in G/H$, and let j($\theta$) be the upper bound of the integers $i_G(s)$ as s runs through the pre-image of $$\theta$$in G. Then:

$i_{G/H}(\theta) - 1 =\varphi_{L/K'}(j(\theta) - 1)$

here L/K'/K is galois extension ,G is the Galois(L/K), H is Galois(K'/K), $i_G$ is the identify function of ramification group, $i_G(s) = min v_L(s(x) - x)$, x runs in the valuation ring of L, and $\varphi$ is the function which turns the lowernumbering ramification group to the uppernumbering ramification group.

[Kevin Buzzard]

Is K a local field, or an arbitrary field equipped with a nonarchimedean valuation? Or an arbitrary field equipped with discrete valuation? There are some foundational questions to be discussed here.

@María Inés de Frutos Fernández do you have an opinion?

Hot take (which I was thinking about last week when reading Fontaine's proof that there is no nontrivial abelian variety over the integers): the normalisation of the upper numbering in the literature is off by one from the best choice :-) (not least because it starts at -1!!). However we should unfortunately not deviate from the literature.

[Johan Commelin]

@Junjie Bai Ok, so now I know the informal statement... where exactly are you stuck? Is i_G(s) already defined in Lean?

[Jiang Jiedong]

@Kevin Buzzard In Serre's book, he extends the definition of lower numbering so that it can take value in Real. This is used to define the $\phi$ and $\psi$ function for upper numbering. (I think extends to $\mathbb{Q}$ is enough?) This extension of definition of lower numbering only holds for rank 1 valuation.

[Junjie Bai]

@Johan Commelin Yes , I have defined $i_G$, but I don't get the Field structure at fixedField H.

[Junjie Bai]

@Kevin Buzzard K is complete under the discrete valuation, but don't have to be local

[Jiang Jiedong]

And the function $i_G$ is well-defined depends on at least one of these two properties holds:
(1) we can take Sup in the less than one part of the value group (This is true in the case of value group to be Zm0, by the discreteness) we can define i_G(s) to be sup of v(s(x) -x) among all elements x in the ring of integer.
(2) the ring extension of the integers of the valuation is generated by one element (or finitely many) (This is true in the case of local field) we can define i_G(s) to be max of v(s(x) -x) among all generators.

[Jiang Jiedong]

My personal experience is that in majority of the literature, one use the lower numbering index starting from -1... (in order to make $G_0$ = inertia group) Is it a good idea that we drop this -1 and use index starting from 0 in mathlib? This -1 will definitely prevent us from defining ramification group to general cases other than $\mathbb{Z}_{m0}$.

[Kevin Buzzard]

My instinct is that it is really important to stick to the literature so that mathematicians can read what we are doing. My instinct is also that the literature made an absolutely terrible choice (reasons: (1) we have two functions on a group, one taking values in {-1,0,1,2,3,...} and the other taking values in {x \in Q | -1 <= x}; neither of these are types in Lean (2) one of the first lines in Fontaine's paper is "we define a new upper numbering grading function on the Galois group to be 1 + the standard one" and then he states all his results for this renormalised grading). My suggestion is that the lower numbering takes values in $\mathbb{Z}$ and the upper one in $\mathbb{Q}$, and that we also define renormalised (+1) ones taking values in $\mathbb{N}$ and $\mathbb{Q}_{\geq0}$; all of these are types in Lean.

@Junjie Bai I don't see any reason why $K$ has to be complete under the discrete valuation. If we develop the basic theory for general fields equipped with a discrete valuation then it will apply to finite Galois groups of number fields
, the decomposition group will be the $-1$ part, inertia the $0$ part etc. It would in theory be possible to develop a theory of lower ramification groups for more general valuations (for example nondiscrete ones, or higher rank ones), indexed by the totally ordered group-with-zero which is the target of the valuation, however I do not see the point in doing this right now. I am not an expert in higher local fields though, I don't know what these guys do. What I do know is that we're not going to need any higher local fields to prove FLT, but we're definitely going to need the lower and upper numbering.