Working on Frobenius elements

Stream: new members

[Michail Karatarakis]

Hi, I am a PhD candidate at Radboud and currently planning to formalise Frobenius elements. Is there anyone else working on this already? Thank you.

[Johan Commelin]

Frobenius elements of Galois groups, you mean?

[Johan Commelin]

For finite or infinite extensions?

[Johan Commelin]

Also: welcome!

[Michail Karatarakis]

Thank you for the welcome.

Yes, for finite extensions.

[Adam Topaz]

I guess we would need to be able to talk about ramification as well, which we currently cannot do!

[Kevin Buzzard]

Not for Frobenius elements -- this would be precisely avoiding the ramified case! But of course in general we want to one day be able to talk about decomposition and inertia groups, which we currently cannot do.

[Adam Topaz]

Well, to be able to talk about the unramified case, we need to be able to talk about the ramified case as well ;)
Anyway, what I really meant is that we need inertia/decomposition groups.

[Kevin Buzzard]

@Michail Karatarakis I learnt about decomposition and inertia groups from Marcus' book "Number fields".

[Michail Karatarakis]

@Kevin Buzzard and @Adam Topaz Great, thank you.

[Filippo A. E. Nuccio]

Welcome @Michail Karatarakis ! Concerning Inertia and Ramification, consider that we have something in docs#ideal.ramification_idx but it is still a bit incomplete. Having a look there might help, though.

[Michail Karatarakis]

@Filippo A. E. Nuccio It definitely helps - thank you.

[Kevin Buzzard]

@Michail Karatarakis although the applications to FLT are all in the number field case, for decomposition and inertia groups one should work in more generality, although what I'm not sure about is what generality one can get away with. The maximally general (and possibly too general) situation is this: $R$ is a commutative ring with field of fractions $K$, $L$ is a field extension of $K$, $S$ is the integral closure of $R$ in $L$, and $P$ is an ideal of $S$. The decomposition group of $P$ with respect to the data $R,K,L$ is the subgroup of G := L \equiv\_a[K] L (the $K$-algebra isomorphisms from $L$ to $L$) which is the stabiliser of $P$ ($G$ acts on $L$ and $S$ and the ideals of $S$). The group $D_P$ acts on $S$ and $P$ and hence on $S/P$, and the inertia subgroup $I_P$ of $D_P$ is the elements of $D_P$ which fix $S/P$ pointwise. In this generality the definition is probably useless, but everything seems to work.

Actually a variant would be the following: if $v$ is a valuation on $L$ then $D_v$ is the subgroup of $G$ which fixes the valuation (i.e. $v(gx)=v(x)$ for all $x$) and if furthermore $v$ is nonarchimedean (are all valuations nonarchimedean in mathlib??) then $I_v$ is the subgroup of elements $g$ with the property that if $v(x)\leq 1$ then $v(x-gx)<1$. I guess you could even formalise both and prove that they're "the same" in situations of interest ($v$ the discrete valuation coming from a maximal ideal of a Dedekind domain).

In practice number theorists only care about special cases of this definition, but it seems to me that the definitions can be made in huge generality.

[Adam Topaz]

The most comprehensive treatment I know of regarding decomposition theory for (Krull) valuations is in Zariski-Samuel's book on commutative algebra.

[Adam Topaz]

Decomposition theory certainly works (and is very important) for arbitrary valuations, not just discrete ones.

[Adam Topaz]

Arguably we should even make sure that inertia/decomposition groups are defined in large enough generality that would allow us to talk about inertia/decomposition in etale fundamental groups

[Kevin Buzzard]

Do you have to do it for rings first and then extend to schemes? If so then Michail doesn't have to worry about schemes (his aim here will be to be able to talk about Frobenius elements in Galois extensions of number fields)

[Filippo A. E. Nuccio]

I think that defining ramification and inertia for arbitrary valuations would be the best option also for bare-hands algebraic number theory, because I think it will simplify the local-to-global (and viceversa) process. Of course, only rank-1 will be needed, but the language will be the most appropriate, no?

[Paul Lezeau]

@Michail Karatarakis A while back I'd started working on the definition of the decomposition group, here's some of the code I wrote if you haven't written the definition yet :smile:

variables {K L : Type*} [field K] {Γ₀ : Type*} [field L] [algebra K L]
  [linear_ordered_comm_group_with_zero Γ₀] {w : valuation L Γ₀}

@[simp] lemma alg_equiv.mul_eq_trans {a b : L ≃ₐ[K] L} : a * b = b.trans a := rfl

@[simp] lemma alg_equiv.inv_eq_symm {a : L ≃ₐ[K] L} : a⁻¹ = a.symm := rfl

def decomposition_group : subgroup (L ≃ₐ[K] L) :=
{ carrier := {σ : L ≃ₐ[K] L | w ∘ σ = w},
  mul_mem' := λ a b ha hb, by { rw set.mem_set_of_eq at ha hb, simp only [alg_equiv.mul_eq_trans,
    set.mem_set_of_eq, alg_equiv.coe_trans], rw [← function.comp.assoc, ha, hb] },
  one_mem' := by ext x ; simp only [alg_equiv.one_apply, function.comp_app],
  inv_mem' := λ x hx, by { ext z, rw set.mem_set_of_eq at hx, conv_lhs {rw ← hx},
    simp only [alg_equiv.inv_eq_symm, function.comp_app, alg_equiv.apply_symm_apply] } }

[Michail Karatarakis]

@Paul Lezeau Great! Thanks a lot for sharing :smile:

[Adam Topaz]

Note that it's probably better to take the stabilizer of the equivalence class of the valuation $w$ as opposed to the function underlying $w$. We have a fairly good theory of docs#valuation_subring that could be used.

[Michail Karatarakis]

Hi, I've been looking at how to define the equivalence class of w. What's the general way of implementing equivalence classes/relations? We have that two valuations are equivalent iff they have the same valuation ring ( lemma is_equiv_iff_valuation_subring). Do I have to define the set of all equivalence classes as a setoid with such an equivalence relation on it, and then define the equivalence class [[w]] as an element of this set ? Is there a similar implementation, or an example in the library I can look at?

[Adam Topaz]

Why not just use the valuation subring directly?

[Adam Topaz]

There is an issue with equivalence of valuations coming from universes, because a valuation involves not just a ring, but also a totally ordered abelian group, which a priori might have a different universe level. So one has to be somewhat careful in defining the equivalence relation on valuations and ensure that the universe parameters of the ring and the value group are the same.

[Adam Topaz]

If you want to get a valuation out of a valuation subring, we do have docs#valuation_subring.valuation

[Michail Karatarakis]

Adam Topaz said:

Why not just use the valuation subring directly?

Could you please clarify this further? So, if suppose we have the set of equivalence classes of valuations of a ring, then for every valuation w in this set, we consider the valuation subring $A_w$ associated to w? Thank you

[Adam Topaz]

Oh, all I'm saying is that the collection of valuations up to equivalence is "the same" (whatever that means) as the collection of valuation subrings of the given field. So instead of working with an equivalence class of valuations you can just work with a valuation subring

[Adam Topaz]

Then if you want to talk about, say, the decomposition group of a valuation $v$, you could just define that as the decomposition group of the valuation ring associated to $v$.

[Michail Karatarakis]

Hi, I've changed the previous definition for the decomposition group by taking the valuation out of a valuation subring.

variables {K : Type*} {Γ : Type*} [field K] [field L] [algebra K L][A: valuation_subring L]
[linear_ordered_comm_group_with_zero Γ]

@[simp] lemma alg_equiv.mul_eq_trans {a b : L ≃ₐ[K] L} : a * b = b.trans a := rfl

@[simp] lemma alg_equiv.inv_eq_symm {a : L ≃ₐ[K] L} : a⁻¹ = a.symm := rfl

def decomp_group: subgroup (L ≃ₐ[K] L) :=
{ carrier := { σ : L ≃ₐ[K] L | A.valuation ∘ σ = A.valuation },
mul_mem' := λ a b ha hb, by {rw set.mem_set_of_eq at *,
simp only [alg_equiv.mul_eq_trans, alg_equiv.coe_trans], rw [← function.comp.assoc, ha, hb]},
one_mem':= by ext x; simp,
inv_mem' := λ x hx, by { ext x, rw set.mem_set_of_eq at *, conv_lhs {rw ← hx}, simp },}

Is this what you meant by any chance?

[Adam Topaz]

No, not quite. What I meant was to define an action of the Galojs group $Gal(L|K)$ on the type of valuation subrings of $L$, and define the decomposition group as a stabilizer of this action. Presumably we can already talk about stabilizers with what's currently in mathlib.

[Kevin Buzzard]

This looks good to me! You don't need Gamma, it seems to play no role (you do need an L though, and some imports; this thread would be easier to follow if someone posts some code with full imports e.g.

import tactic
import field_theory.abel_ruffini
import ring_theory.valuation.valuation_subring

variables {K : Type*} {L : Type*} [field K] [field L] [algebra K L][A: valuation_subring L]

@[simp] lemma alg_equiv.mul_eq_trans {a b : L ≃ₐ[K] L} : a * b = b.trans a := rfl

@[simp] lemma alg_equiv.inv_eq_symm {a : L ≃ₐ[K] L} : a⁻¹ = a.symm := rfl

def decomp_group: subgroup (L ≃ₐ[K] L) :=
{ carrier := { σ : L ≃ₐ[K] L | A.valuation ∘ σ = A.valuation },
mul_mem' := λ a b ha hb, by {rw set.mem_set_of_eq at *,
simp only [alg_equiv.mul_eq_trans, alg_equiv.coe_trans], rw [← function.comp.assoc, ha, hb]},
one_mem':= by ext x; simp,
inv_mem' := λ x hx, by { ext x, rw set.mem_set_of_eq at *, conv_lhs {rw ← hx}, simp },}

seems to work).

It seems to me that this decomposition group contains a whole host of subgroups. Given any element i of the valuation group which is <= 1, you can look at the subgroup of this decomposition group consisting of the g such that v(gx-x)<i for all x in the valuation ring, or maybe v<=i. Look up definitions of higher ramification groups (with the "lower numbering"), probably there is no reason not to define all of them at this point!

[Michail Karatarakis]

OK, so for the definition of the decomposition group as the stabiliser of the group action on the set of valuation subrings, could you point to me any references or similar constructions in the library?

[Kevin Buzzard]

There is docs#mul_action.stabilizer but you'll need an action of L ≃ₐ[K] L on valuation_subring L, which you might have to make manually. I guess more generally the way to do it would be this: if L -> M is a map of fields then you can pull back a valuation subring of M and get a valuation subring of L (I don't know if we have this). The pullback of the pullback is the pullback and the pullback via the identity map is the identity, and from these facts you can deduce that the pullback along an isomorphism is a bijection. I don't know if we have this stuff but it shouldn't be too hard.

[Michail Karatarakis]

Could we use docs#category_theory.limits.shapes.comm_sq for the pullback in this case?

[Adam Topaz]

I think you''re confused about Kevin's use of the word "pullback". He just means to take the preimage, which would go under the name "comap" in mathlib, i.e. something like this

import ring_theory.valuation.valuation_subring

variables {K L : Type*} [field K] [field L]

def valuation_subring.comap (A : valuation_subring L) (e : K →+* L) :
  valuation_subring K :=
{ mem_or_inv_mem' := sorry,
  ..(A.to_subring.comap e) }

[Michail Karatarakis]

Hi, so the definition above asks to prove that ⊢ e k ∈ A ∨ e k⁻¹ ∈ A. However, shouldn't it be ⊢ e k ∈ A ∨ (e k)⁻¹ ∈ A from the definition of the valution subring? I am not clear about whether this a matter of notation or I am missing something. This is an example of what it's been going on :

import ring_theory.valuation.valuation_subring
variables {K L : Type*} [field K] [field L]
def valuation_subring.comap  (A : valuation_subring L) (e  : K →+* L) :
  valuation_subring K :=
{mem_or_inv_mem' :=
begin
rintro k,
simp,
have h : e k ∈ A ∨ (e k)⁻¹ ∈ A,
exact valuation_subring.mem_or_inv_mem A (e k),
cases h with h hinv,
left,
exact h,
right,
sorry,
end
  ..(A.to_subring.comap e) }

[Kevin Buzzard]

exact hinv, works for me for that sorry. What's your question?

[Michail Karatarakis]

That's interesting - it doesn't seem to work for me:

invalid type ascription, term has type
  (⇑e k)⁻¹ ∈ A
but is expected to have type
  ⇑e k⁻¹ ∈ A

[Kevin Buzzard]

The non-terminal simp is doing a different thing on your box to mine.

[Kevin Buzzard]

Nonterminal simps are a bad idea. You ran simp but it didn't close the goal. Thus what happened is a function of what simp lemmas are on the system at a given time.

[Michail Karatarakis]

OK, so how do I fix this?

[Kevin Buzzard]

For the version of mathlib I was using, simp found map_inv₀. But you should remove the non-terminal simp anyway. Replace it with squeeze_simp and then the corresponding rewrite.

[Kevin Buzzard]

and then post your question again and I'll be much more likely to be in the same position as you.

[Kevin Buzzard]

On master exact hinv works for the sorry.

[Kevin Buzzard]

Where are you working? If on a branch of mathlib you could try merging master. If on a separate project you could try bumping mathlib.

[Michail Karatarakis]

So, now I am getting the same error as before whilst rewriting to :

def valuation_subring.comap  (A : valuation_subring L) (e  : K →+* L) :
  valuation_subring K :=
{mem_or_inv_mem' :=

begin
rintro k,
simp only [subring.mem_carrier, subring.mem_comap, valuation_subring.mem_to_subring],
have h : e k ∈ A ∨ (e k)⁻¹ ∈ A,
exact valuation_subring.mem_or_inv_mem A (e k),
cases h with h hinv,
left,
exact h,
right,
exact hinv,
end
  ..(A.to_subring.comap e) }

[Michail Karatarakis]

I have been having some path related issues with the imports. The only project that seemed to work at that time was the tutorials project :) I 'll try reinstalling everything.

[Kevin Buzzard]

So now your code has no non-terminal simps and it rightly doesn't work, because (⇑e k)⁻¹ and ⇑e k⁻¹ are not definitionally equal.

[Kevin Buzzard]

So what is left of your question now?

[Kevin Buzzard]

One is inv (e k), the other is e (inv k).

[Michail Karatarakis]

Alright, so now the definition works with map_inv₀ ?

[Kevin Buzzard]

Yeah, that's the last piece of the puzzle.

[Kevin Buzzard]

I don't know why my simp found it and not yours.

squeeze_simp,
-- Try this: simp only [subring.mem_carrier, subring.mem_comap, valuation_subring.mem_to_subring, map_inv₀]

[Yaël Dillies]

because it just got changed: #15985

[Yaël Dillies]

You probably want to merge master.

[Kevin Buzzard]

or bump mathlib, depending on where this code is

[Michail Karatarakis]

Yes, thanks. I created a new project and it's fixed now.

import ring_theory.valuation.valuation_subring

variables {K L : Type*} [field K] [field L]

def valuation_subring.comap  (A : valuation_subring L) (e  : K →+* L) :
  valuation_subring K :=
{mem_or_inv_mem' :=

begin
rintro k,
simp only [subring.mem_carrier, subring.mem_comap, valuation_subring.mem_to_subring, map_inv₀],
have h : e k ∈ A ∨ (e k)⁻¹ ∈ A,
exact valuation_subring.mem_or_inv_mem A (e k),
cases h with h hinv,
left,
exact h,
right,
exact hinv,
end
  ..(A.to_subring.comap e) }

[Yaël Dillies]

Do not recreate projects :scream:

[Yaël Dillies]

Do leanproject up

[Michail Karatarakis]

Regarding the action of the Galois group on valuation_subring ring K, do I have to define it as a new class?

[Adam Topaz]

We should first golf a little bit...

import ring_theory.valuation.valuation_subring

variables {K L : Type*} [field K] [field L]

def valuation_subring.comap  (A : valuation_subring L) (e  : K →+* L) :
  valuation_subring K :=
{ mem_or_inv_mem' := λ k, by simp [valuation_subring.mem_or_inv_mem],
  ..(A.to_subring.comap e) }

[Adam Topaz]

The action of the Galois group would be an instance of the class docs#mul_action

[Adam Topaz]

BTW: Note that this is a right action

[Michail Karatarakis]

Right, so how do I define this action as a right action involving the comap?

import ring_theory.valuation.valuation_subring
import group_theory.group_action.defs

variables {K : Type*} {L: Type* } {M: Type*} [field K] [field L]
[algebra K L] [A : valuation_subring L]

instance pullback_action:  mul_action (L ≃ₐ[K] L)  M :=
{one_smul:= λσ, by refl,
 mul_smul:= λσ₁, λσ₂, λm, by refl }

[Michail Karatarakis]

Kevin Buzzard said:

The pullback of the pullback is the pullback and the pullback via the identity map is the identity, and from these facts you can deduce that the pullback along an isomorphism is a bijection.

I am not clear about how to customise this instance to involve these facts above. Would a right action suffice?

[Kevin Buzzard]

type.png

After the line refine {to_fun := _, map_one' := _, map_mul' := _},, one of your goals is a Type not a Prop. This is bad. You closed the goal with tauto, and what this did was generated a completely random endomorphism because tauto is not expecting to run on types. Judging by the other goals it looks like tauto chose the identity function, so right now what you seem to have is an action of the pulled back valuation (considered as a monoid), on the K-automorphisms of L, considered as a set (or more precisely a type), and the definition of the action is that everything acts trivially.

[Kevin Buzzard]

You want to give an action of the automorphisms on the valuation subrings.

[Kevin Buzzard]

instance : mul_action (L ≃ₐ[K] L) (valuation_subring L) :=
{ smul := λ e A, A.comap e, -- you cannot use tactic mode for this, it's data
  one_smul := begin sorry end,
  mul_smul := begin sorry end }

[Kevin Buzzard]

Michail Karatarakis said:

Kevin Buzzard said:

The pullback of the pullback is the pullback and the pullback via the identity map is the identity, and from these facts you can deduce that the pullback along an isomorphism is a bijection.

I am not clear about how to customise this instance to involve these facts above or if, they are implied. Would such a right action suffice?

The facts I flagged are precisely what you have to prove to create the mul_action.

[Kevin Buzzard]

You have defined valuation_subring.comap. Every definition comes with a cost. You might well find it tricky to fill in those two sorrys. Give them a go! But here's an interesting experiment (which you can try after): you can see that valuation_subring.comap is one proof and then everything else is subring.comap. You can jump to the definition of subring.comap in VS Code and observe that just after that definition is made, three theorems are proved:

@[simp] lemma coe_comap (s : subring S) (f : R →+* S) : (s.comap f : set R) = f ⁻¹' s := rfl

@[simp]
lemma mem_comap {s : subring S} {f : R →+* S} {x : R} : x ∈ s.comap f ↔ f x ∈ s := iff.rfl

lemma comap_comap (s : subring T) (g : S →+* T) (f : R →+* S) :
  (s.comap g).comap f = s.comap (g.comp f) :=
rfl

Two of those lemmas are tagged @[simp] and if you don't prove the analogous lemmas for valuation_subring.comap then the simplifier won't know even the most basic stuff about valuation_subring.comap. You want to train the simplifier to prove simple equalities (like your two sorries) and iffs for you. So see if you can prove the analogues of those statements, and then you might find that the two sorries needed to make the mul_action are much easier.

[Kevin Buzzard]

Here's the lemmas proved just after subgroup.comap:

@[simp, to_additive]
lemma coe_comap (K : subgroup N) (f : G →* N) : (K.comap f : set G) = f ⁻¹' K := rfl

@[simp, to_additive]
lemma mem_comap {K : subgroup N} {f : G →* N} {x : G} : x ∈ K.comap f ↔ f x ∈ K := iff.rfl

@[to_additive]
lemma comap_mono {f : G →* N} {K K' : subgroup N} : K ≤ K' → comap f K ≤ comap f K' :=
preimage_mono

@[to_additive]
lemma comap_comap (K : subgroup P) (g : N →* P) (f : G →* N) :
  (K.comap g).comap f = K.comap (g.comp f) :=
rfl

and here's what's proved after submonoid.comap:

@[simp, to_additive]
lemma coe_comap (S : submonoid N) (f : F) : (S.comap f : set M) = f ⁻¹' S := rfl

@[simp, to_additive]
lemma mem_comap {S : submonoid N} {f : F} {x : M} : x ∈ S.comap f ↔ f x ∈ S := iff.rfl
omit mc

@[to_additive]
lemma comap_comap (S : submonoid P) (g : N →* P) (f : M →* N) :
  (S.comap g).comap f = S.comap (g.comp f) :=
rfl

@[simp, to_additive]
lemma comap_id (S : submonoid P) : S.comap (monoid_hom.id P) = S :=
ext (by simp)

So those are some good suggestions for what kind of API you should make for valuation_subring.comap.

[Kevin Buzzard]

Wooah, the bare type comap (called preimage, it's a special case like an irregular verb) has all this:

def preimage {α : Type u} {β : Type v} (f : α → β) (s : set β) : set α := {x | f x ∈ s}

infix ` ⁻¹' `:80 := preimage

section preimage
variables {f : α → β} {g : β → γ}

@[simp] theorem preimage_empty : f ⁻¹' ∅ = ∅ := rfl

@[simp] theorem mem_preimage {s : set β} {a : α} : (a ∈ f ⁻¹' s) ↔ (f a ∈ s) := iff.rfl

lemma preimage_congr {f g : α → β} {s : set β} (h : ∀ (x : α), f x = g x) : f ⁻¹' s = g ⁻¹' s :=
by { congr' with x, apply_assumption }

theorem preimage_mono {s t : set β} (h : s ⊆ t) : f ⁻¹' s ⊆ f ⁻¹' t :=
assume x hx, h hx

@[simp] theorem preimage_univ : f ⁻¹' univ = univ := rfl

theorem subset_preimage_univ {s : set α} : s ⊆ f ⁻¹' univ := subset_univ _

@[simp] theorem preimage_inter {s t : set β} : f ⁻¹' (s ∩ t) = f ⁻¹' s ∩ f ⁻¹' t := rfl

@[simp] theorem preimage_union {s t : set β} : f ⁻¹' (s ∪ t) = f ⁻¹' s ∪ f ⁻¹' t := rfl

@[simp] theorem preimage_compl {s : set β} : f ⁻¹' sᶜ = (f ⁻¹' s)ᶜ := rfl

@[simp] theorem preimage_diff (f : α → β) (s t : set β) :
  f ⁻¹' (s \ t) = f ⁻¹' s \ f ⁻¹' t := rfl

[loads more omitted]

[Kevin Buzzard]

You could check that valuation_subring.comap plays well with the lattice structure on valuation subrings. Looking through the mathlib file where valuation_subring is defined, it appears to have instance : semilattice_sup (valuation_subring K) := ... which means that the valuation subrings of a field have some kind of lattice structure (infs or sups, like unions and intersections, maybe finite or infinite) and you could see if your construction preserved these things. That's what preimage_inter is doing above, for example (but using nonstandard ∩ instead of standard ⊓, called inf)

[Kevin Buzzard]

Finally, it's really important that you move [algebra K L] below the definition of valuation_subring.comap. I've just noticed that comap is picking it up, and we definitely don't need it at this point.

[Michail Karatarakis]

Great, thank you very much.

[Kevin Buzzard]

Adam Topaz said:

BTW: Note that this is a right action

Oh yeah! @Adam Topaz how do we do right actions in Lean? I think the code I've posted for the mul_action is not right.

[Kevin Buzzard]

smul := λ e A, A.comap e.symm, would work but is this the idiomatic way?

[Adam Topaz]

One option is to use docs#mul_opposite but @Eric Wieser will probably tell us the best way to do this

[Kevin Buzzard]

With my way, to get simp to do the job you need

@[simp] lemma alg_equiv.one_symm : (1 : L ≃ₐ[K] L).symm = 1 := rfl
@[simp] lemma alg_equiv.mul_symm {a b : L ≃ₐ[K] L} : (a * b).symm = b.symm * a.symm := rfl

Using

instance : mul_action (L ≃ₐ[K] L)ᵐᵒᵖ (valuation_subring L) :=
{ smul := λ e A, A.comap (unop e : L ≃ₐ[K] L),

I only have to make the basic API for valuation_subring.comap and I can get ext, simp to do everything.

[Kevin Buzzard]

@Michail Karatarakis I hadn't noticed it was a right action. Probably the ᵐᵒᵖ approach is best.

[Michail Karatarakis]

OK so, this is the definition we need for the right action?

instance : mul_action (L ≃ₐ[K] L)ᵐᵒᵖ (valuation_subring L) :=
{ smul := λ e A, A.comap (unop e : L ≃ₐ[K] L),
  one_smul := begin sorry end,
  mul_smul := begin sorry end }

[Yaël Dillies]

A good stress test for your definition is trying to show smul_comm_class (L ≃ₐ[K] L) (L ≃ₐ[K] L)ᵐᵒᵖ (valuation_subring L).

[Eric Wieser]

Mathlib only has right multiplication actions, not actions on the codomain

[Eric Wieser]

But certainly you can use mul_opposite to define this comap action; you're just at risk of hitting instance diamonds

[Eric Wieser]

Is docs#valuation_subring of the type I'd expect? (edit: no) If so, then I think there's already an action via map, docs#subring.pointwise_mul_action

[Kevin Buzzard]

Yaël Dillies said:

A good stress test for your definition is trying to show smul_comm_class (L ≃ₐ[K] L) (L ≃ₐ[K] L)ᵐᵒᵖ (valuation_subring L).

I can't make sense of this. What is the left action?

[Eric Wieser]

The one via map

[Eric Wieser]

That I link above for subring, but that we don't have yet for valuation_subring

[Kevin Buzzard]

I don't think there's map for valuation_subring. The image of a valuation subring under a ring homomorphism might not be a valuation subring.

[Kevin Buzzard]

Oh -- I see -- for equivs there is a map!

[Eric Wieser]

I would guess it generalizes to any group action, not just equivs

[Kevin Buzzard]

I'm confused. If you have a right action of a group on a thing, how are you getting a left action of the same group?

[Kevin Buzzard]

Just use the right action of the inverse?

[Kevin Buzzard]

I don't think these actions commute in general. I'm lost.

[Kevin Buzzard]

I can't make any sense of Yael's stress test.

[Eric Wieser]

I'll PR what I'm thinking of

[Kevin Buzzard]

I can't see any map other than A.map e = A.comap e.symm and these actions won't commute if the group isn't abelian.

[Eric Wieser]

#16080

[Eric Wieser]

Oh sorry, your point was that the actions might not commute, not that you can't think of what the left action is (which that PR provides)

[Eric Wieser]

I also now agree that @Yaël Dillies' stress test doesn't seem to make sense.

[Yaël Dillies]

Shouldn't my stress test boil down to associativity of composition?

[Eric Wieser]

What are you composing?

[Yaël Dillies]

I guess I was seeing valuation_subring as an alg_equiv :upside_down:

[Eric Wieser]

I think the true version of the statement is that "two actions on (valuation) subrings commute if they commute on the elements". Currently we are missing those instances for pointwise actions on subobjects

[Michail Karatarakis]

~Shall I just work on the API for the comap for now then, until the definition of the action can be stated or look at the PR first? I am bit confused.

[Kevin Buzzard]

I am about to go on holiday for a week so will be limited help during this time, but my honest opinion is that it would be good for you to fill in the sorries for the mop left action but in practice if you use it you'll just get a load of subgroups of the opposite group which will be really annoying, so I would just define the decomposition and inertia subgroups manually.

[Michail Karatarakis]

OK, just to conclude - here are the definitions we have so far:

import ring_theory.valuation.valuation_subring
import group_theory.group_action.basic

variables {K L : Type*} [field K] [field L] [algebra K L]

def valuation_subring.comap  (A : valuation_subring L) (e  : K →+* L) :
  valuation_subring K :=
{ mem_or_inv_mem' := λ k, by simp [valuation_subring.mem_or_inv_mem],
  ..(A.to_subring.comap e) }

instance : mul_action (L ≃ₐ[K] L)ᵐᵒᵖ (valuation_subring L) :=
{ smul := λ e A, A.comap (e.unop : L ≃ₐ[K] L),
  one_smul := begin sorry end,
  mul_smul := begin sorry end }

def decomposition_group (A : valuation_subring L) [mul_action (L ≃ₐ[K] L)ᵐᵒᵖ A] :
mul_action.stabilizer (L ≃ₐ[K] L)ᵐᵒᵖ A  := sorry

Is the definition of the decomposition group above what you meant?

[Michail Karatarakis]

Concerning the inertia group, do we define it as we 've discussed before ?:

1) $R_v$ is the valuation ring $\{ a ∈ L | v(a) \leq 1 \}$ ( prove that $R_v$ is a subring of $L$ ).

2) Define the maximal ideal of $m_v=\{ a ∈ K \mid v(a) < 1\}$ ( prove that $m_v$ is a subring of $L$).

3) Define the inertia group $I_v$ as the quotient $R_v/m_v.$

Is this the best way we can define it?

[Adam Topaz]

A few points

1. As Kevin mentioned, it could get annoying to work with the decomposition group if defined as a stabilizer, because this is a right action, and you use mop, meaning that the stabilizer is a subgroup of the mul-opposite of the Galois group instead of the Galois group itself. It's possible to translate to the Galois group with this approach, but it would be easier to define it as a subgroup of the Galois group directly.

2. Your second declaration doesn't make sense. You're trying to define the decomposition group as a stabilizer, not obtain some element of the stabilizer. When you write def decomposition_group (A : valuation_subring L) [mul_action (L ≃ₐ[K] L)ᵐᵒᵖ A] : mul_action.stabilizer (L ≃ₐ[K] L)ᵐᵒᵖ A := sorry, that means you're trying to obtain some element (aka "term") of the stabilizer.

3. The inertia group is not $R/\mathfrak{m}$. That's the residue field. you need to show that elements of the decomposition group preserve the maximal ideal and define the inertia group as those elements in the decomposition group which act trivially on the residue field.

[Adam Topaz]

We have a fairly robust API for valuation subrings in mathlib thanks to the work of @Jack McKoen . There is no need to define $R_v$ and/or $\mathfrak{m}_v$. Rather, it would be better to use (and extend) the existing API from mathlib.

[Michail Karatarakis]

1. & 2. OK, thank you for the clarification.

2. Oh, yes, you are right. I meant I should define the residue field first and then proceed - defining the inertia group would have been a fourth goal. Thus, do I define it as a subgroup of the decomposition group in this case?

[Adam Topaz]

Re 2: I would define the inertia group as a subgroup of the Galois group and prove that it's contained in the decomposition group, using the lattice structure on the type of subgroups of a group.

[Adam Topaz]

Also, mathlib knows that valuation rings are local, so there is no need to define the residue field as you can use the API for local rings.

[Michail Karatarakis]

OK, clear. I forgot to ask - the stabiliser subgroup is not in mathlib? (that's what confused me when I looked at docs#mul_action.stabilizer).

[Yaël Dillies]

What do you mean? mul_action.stabilizer is precisely the stabiliser subgroup.

[Michail Karatarakis]

Yeah, I was trying to understand Adam's point about the difference between obtaining a term of the stabiliser, and, the stabiliser. I thought that definition results in a subgroup and not a term. Of course my definition still doesn't make sense as it's been pointed out.

[Eric Wieser]

Your mistake is like writing def foo : 37 := sorry instead of def foo : nat := 37

[Kevin Buzzard]

The problem is that it's a right action so the stabiliser stuff doesn't work because that's set up for left actions

[Michail Karatarakis]

Right, I 'll try filling up the sorry s of the action regardless for practice. However, is there a set theoretic notation for the definition of the decomposition group that involves this action? Does the right action just play the rule of the composition ∘ as in the previous attempts ?

[Michail Karatarakis]

@Kevin Buzzard , could this be an alternative definition for the inertia group?

import ring_theory.valuation.valuation_subring

variables {K L: Type*} [field K] [field L][algebra K L] [A: valuation_subring L]

def inertia (x : A) : subgroup (L ≃ₐ[K] L):=
{ carrier := {σ : (L ≃ₐ[K] L)  |  A.valuation (σ x - x) <1 },
  mul_mem':=sorry,
  one_mem':=sorry,
  inv_mem':=sorry,
}

[Kevin Buzzard]

That's not the inertia subgroup because that function takes an input x and then returns a subgroup which depends on x. You probably want a "for all x" somewhere instead. I'm still in a field with no access to lean but I guess the forall goes after | in the carrier field

[Johan Commelin]

I don't think A : valuation_subring L should be in [typeclass brackets]. I guess (regular explicit) is how it's intended to be used.

[Yaël Dillies]

{A : valuation_subring L} is the correct thing here, actually, because of the(x : A). That's not the case anymore if you fix the definition as Kevin says.

[Michail Karatarakis]

Right, so it should be something like:

import ring_theory.valuation.valuation_subring

variables {K L: Type*} [field K] [field L][algebra K L]

def inertia (A: valuation_subring L): subgroup (L ≃ₐ[K] L):=
{ carrier := {σ : (L ≃ₐ[K] L)  | ∀ (x : A), A.valuation (σ (x) - x) < 1 },
  mul_mem':=sorry,
  one_mem':=sorry,
  inv_mem':=sorry,
}

[Michail Karatarakis]

1) Could an alternative definition for the inertia group be the following : " the elements of the Galois group (of the decomposition group)​ which fix the residue field pointwise" instead of saying "the elements that act trivially on the residue field" ? In this case, do the pointwise actions from docs#valuation_subring need to be modified for this goal?

2) Furthermore, understanding how actions are implemented would help me define the decomposition group too. Right now I am not clear about how to define it as a stabiliser from scratch. For example mul_action.stabiliser ( as it's been pointed out ) only works for left actions. It also seems that the definition is also based on other things that need to be defined from scratch for right actions too. So far, I can't see clearly where I have to start for that and how deep it gets- what we have, is this instance

instance : mul_action (L ≃ₐ[K] L)ᵐᵒᵖ (valuation_subring L) :=
{ smul := λ e A, A.comap (e.unop : L ≃ₐ[K] L),
  one_smul := begin sorry end,
  mul_smul := begin sorry end }

If I wish to define the decomposition group as

def decomposition_group : subgroup (L ≃ₐ[K] L)  := sorry

how could I involve this instance in the carrier?

[Kevin Buzzard]

Just define the stabiliser by hand as the elements of the group which fix something. As for fixing the residue field, sure you could define it like this. Did you define an action of the decomposition group on the residue field? That's an obvious prerequisite for this approach

[Michail Karatarakis]

"Just define the stabiliser by hand as the elements of the group which fix something" If I have a generic subgroup such as

variables {α β  : Type*} [group α ] [ group β ]

def stabilizer : subgroup α  :=
{ carrier := { a : α   |  ∀ (b : β), b • a  = b },
 mul_mem':=sorry,
 one_mem':=sorry,
 inv_mem':=sorry
  }

How do I to involve the mul_action instance from above - i. e. how do I equip this subgroup where • is that right action specifically?

[Eric Wieser]

That example seems to be missing mul_action α β

[Eric Wieser]

But the answer is "choose α and β and lean will find the appropriate instance"

[Eric Wieser]

You should be able to use stabilizer (L ≃ₐ[K] L)ᵐᵒᵖ (valuation_subring L)

[Eric Wieser]

(also note that the map action is now merged, docs#valuation_subring.pointwise_mul_action)

[Michail Karatarakis]

Eric Wieser said:

You should be able to use stabilizer (L ≃ₐ[K] L)ᵐᵒᵖ (valuation_subring L)

@Eric Wieser Yes sure, but what it's been pointed out is that this stabilizer is set up for left actions and we need a right action. Thus, it's better if I can define a stabilizer subgroup for an arbitrary mul_action . That's what I am not clear about, hence that example above. Any ideas of how I could implement a stabilizer subgroup for an arbitrary action?

[Eric Wieser]

docs#mul_action.stabilizer is already defined for an arbitrary mul_action (over a group), so I don't understand your question

[Michail Karatarakis]

Kevin Buzzard said:

The problem is that it's a right action so the stabiliser stuff doesn't work because that's set up for left actions

Right, I am referring to what @Kevin Buzzard and Adam pointed out.

[Kevin Buzzard]

We don't want a subgroup of G^mop, we want a subgroup of G.

Do you know what -- maybe we don't want the decomposition subgroup to be a subgroup? Maybe we just use the left action of mop but define D v to be the subtype rather than the subgroup? What do you think @Adam Topaz ? If v is a valuation not on the top field but on the bottom field, how are we going to define D v? I have always thought of it as a subgroup of the global Galois group but I'm wondering whether the object is sufficiently important to deserve its own decomposition_group v : Type rather than decomposition_subgroup v : subgroup (L K-alg_iso L).

@Michail Karatarakis there is a ton of stuff you could do here. Let's just have a one-on-one meeting at some point. I am on holiday right now unfortunately, but I will be back on Monday evening. I'll contact you offline and give you some concrete problems to think about. Right now, as sometimes happens, there seems to be several possibilities for the formalised definition of a decomposition group.

[Yaël Dillies]

Then you can use docs#subgroup.unopposite.

[Yaël Dillies]

Damn, it doesn't exist :sad: but docs#subgroup.opposite does, so it really should be there!

[Yaël Dillies]

I guess you're meant to use docs#subgroup.opposite_equiv:

def decomposition_subgroup : subgroup (L ≃ₐ[K] L) :=
subgroup.opposite_equiv.symm $ stabilizer (L ≃ₐ[K] L)ᵐᵒᵖ (valuation_subring L)

[Adam Topaz]

Well, there is no decomposition group if you only have a valuation of the base-field -- you need to choose a prolongation.
It's a theorem that the decomposition groups of two prolongations (which are conjugate) are conjugate in the group-theoretic sense, but that's a theorem. So you could define $D_v$ as a conjugacy class when $v$ is a valuation of the base.

[Adam Topaz]

I do think it should be defined as a sungroup because the behavior of this subgroup in the lattice of subgroups of the Galois groups reflects the decomposition behavior of the valuation on the base (and if you also include the inertia, you can relate ramification to this lattice structure as well)

[Kevin Buzzard]

Oh yes of course I'm a fool, it's only a conjugacy class of subgroups, I don't know what I was thinking.

[Adam Topaz]

It is confusing because we like to identify "the decomposition group of $p$" in $Gal_\mathbb{Q}$ with $Gal_{\mathbb{Q}_p}$ all the time ;)

[Kevin Buzzard]

OK so from now on I will try to be coherent. In the example you highlight above the following phenomena occur: We have an extension L of K (Galois, in this case), a valuation v on K, (uncountably) many extensions of this valuation to L, and for any two such extensions w1 and w2, there's a K-isomorphism from L to L sending w1 to w2. Furthermore if we choose an arbitrary w in L extending v on K, then the canonical map from D_w to the K_v-isomorphisms of L_w is an isomorphism. In what generality is all that true?

[Adam Topaz]

If you replace completion with Henselization, then this is true for arbitrary valuations. For completions, I don't know of the top of my head.

[Kevin Buzzard]

Do we have this in mathlib?

[Adam Topaz]

I don't think so.

[Kevin Buzzard]

Would it be worth Michail working on this, if his ultimate goal is to start talking about things like local conditions on deformations of global Galois representations? Is it the sort of thing which one actually needs in practice, or would be helpful to have? Is it _hard_? What's a reference?

[Kevin Buzzard]

I hadn't quite realised that things could be done in such generality.

[Adam Topaz]

Here is the page from the stacks project https://stacks.math.columbia.edu/tag/0BSK

[Adam Topaz]

What sorts of local conditions are you referring to?

[Kevin Buzzard]

deformations of representations of global Galois groups which are finite flat at p, or unramified at q, or something like that. FLT stuff. Michail is a student of Freek who's formalising the statements of some of the theorems of Wiles and Taylor-Wiles.

[Adam Topaz]

I think most things (e.g. unramified) can be phrased (and usually are phrased) entirely in terms of the structure of the decomposition group. Once you get to more analytic conditions, like being de Rham at p, that's when the identification with the Galois group of the completion seems to be required

[Kevin Buzzard]

A 2-dimensional representation being locally an extension of one-dimensional representations is perhaps a nice example. No completions needed there I guess.

[Adam Topaz]

I'm teaching a graduate NT course next term. It would be great if I can show off decomposition theory in mathlib by then ;)

[Kevin Buzzard]

@Adam Topaz what do you think of the following fix for the left/right thing: we can pull back valuations along arbitrary field maps, but we can push them forward along equivs. This would give us a left action, right?

[Adam Topaz]

Hmmmm I think that would be confusing. For example, is $\sigma D_v \sigma^{-1} = D_{v^\sigma}$ or $$D_{v^{\sigma^{-1}}$$? (I never remember and always have to write out the formula when I need to figure this out, but it's written down in books always using the right action, I suppose)

[Adam Topaz]

I'm a bit surprised that right actions are such a problem, given that we now have things like two-sided ideals.

[Adam Topaz]

Adam Topaz said:

I'm a bit surprised that right actions are such a problem, given that we now have things like two-sided ideals.

maybe I just made that up?

[Kevin Buzzard]

Do we want the decomposition subgroup to be a subgroup of G or of G^mop?

[Adam Topaz]

of G!

[Kevin Buzzard]

I guess we could pull it back along the isomorphism (do you know the name for the group iso G -> G^mop?) (op(g^{-1}) or whatever)

[Adam Topaz]

docs#mul_equiv.inv'

[Kevin Buzzard]

oh is this the point of division monoids??

[Adam Topaz]

That was my first encounter with division_monoid :rofl:

[Kevin Buzzard]

@Yaël Dillies that's pretty cool :-)

[Junyan Xu]

We have subbimodules, implemented via tensor product: https://github.com/leanprover-community/mathlib/commit/58cef51f7a819e7227224461e392dee423302f2d
Two-sided ideals would involve mop (sketch here)

[Yaël Dillies]

Kevin Buzzard said:

oh is this the point of division monoids??

One of them!

[Yaël Dillies]

@Kevin Buzzard said:

I guess we could pull it back along the isomorphism (do you know the name for the group iso G -> G^mop?) (op(g^{-1}) or whatever)

Did you read my snippet above? This is exactly what it does:

def decomposition_subgroup : subgroup (L ≃ₐ[K] L) :=
subgroup.opposite_equiv.symm $ stabilizer (L ≃ₐ[K] L)ᵐᵒᵖ (valuation_subring L)

[Junyan Xu]

This is exactly what it does:

I think they differ by ⁻¹

[Yaël Dillies]

Hmm... You're right. Why does that matter?

[Junyan Xu]

I think what they have in mind originally/mathematics-wise is your version, actually.

[Kevin Buzzard]

@Adam Topaz is there a general theory of higher ramification groups in this setting, indexed e.g. by elements of the value group in the range (0,1] or something?

[Kevin Buzzard]

Do you understand all that phi and psi conversion to upper numbering in the DVR setting, on a conceptual level?

[Michail Karatarakis]

Yaël Dillies said:

I guess you're meant to use docs#subgroup.opposite_equiv:

def decomposition_subgroup : subgroup (L ≃ₐ[K] L) :=
subgroup.opposite_equiv.symm $ stabilizer (L ≃ₐ[K] L)ᵐᵒᵖ (valuation_subring L)

@Yaël Dillies Could you please explain what your code does, and include the imports?

[Yaël Dillies]

The imports should be the same as yours.

[Yaël Dillies]

So stabilizer (L ≃ₐ[K] L)ᵐᵒᵖ (valuation_subring L) : subgroup (L ≃ₐ[K] L)ᵐᵒᵖ. But mathematically (L ≃ₐ[K] L)ᵐᵒᵖ is just L ≃ₐ[K] L again, so take the image of stabilizer (L ≃ₐ[K] L)ᵐᵒᵖ (valuation_subring L) under the mathematically irrelevant map (L ≃ₐ[K] L)ᵐᵒᵖ → L ≃ₐ[K] L.

[Michail Karatarakis]

It doesn't seem to compile. What's the issue here?

import ring_theory.valuation.valuation_subring
import group_theory.group_action.basic
import algebra.group.opposite

variables {K L: Type*} [field K] [field L] [algebra K L]

def decomposition_subgroup : subgroup (L ≃ₐ[K] L) :=
subgroup.opposite_equiv.symm $ mul_action.stabilizer (L ≃ₐ[K] L)ᵐᵒᵖ (valuation_subring L)

[Michail Karatarakis]

Yaël Dillies said:

So stabilizer (L ≃ₐ[K] L)ᵐᵒᵖ (valuation_subring L) : subgroup (L ≃ₐ[K] L)ᵐᵒᵖ. But mathematically (L ≃ₐ[K] L)ᵐᵒᵖ is just L ≃ₐ[K] L again, so take the image of stabilizer (L ≃ₐ[K] L)ᵐᵒᵖ (valuation_subring L) under the mathematically irrelevant map (L ≃ₐ[K] L)ᵐᵒᵖ → L ≃ₐ[K] L.

OK, thanks.

[Yaël Dillies]

Sorry, I wasn't done explaining!

[Yaël Dillies]

However docs#subgroup.opposite_equiv is not what I thought it was, so here's #16271 to define that "mathematically irrelevant map". If you use the code from that PR, then the definition becomes

def decomposition_subgroup : subgroup (L ≃ₐ[K] L) :=
subgroup.opposite.symm $ stabilizer (L ≃ₐ[K] L)ᵐᵒᵖ (valuation_subring L)

[Adam Topaz]

@Kevin Buzzard there is some work on this but as far as I know there is no established theory.

The one thing that comes to mind is work of Abrashkin on higher ramification in higher dimensional local fields -- he even constructs analogues of the field of norms!

[Adam Topaz]

The wild ramification group can always be defined for any valuation (it's the unique p-Sylow subgroup of the inertia group, where p is the residue characteristic)

[Adam Topaz]

And the theorem that the residue Galois group acts cyclotomically on the tame inertia still holds in general

[Kevin Buzzard]

but then wild inertia has some funny filtration on it indexed by the value group (which I just discovered isn't a group! #16272 that confused me for a bit).

[Kevin Buzzard]

I think Huber uses the phrase differently to mathlib :-(

[Adam Topaz]

I think even defining the filtration is subtle. There is no obvious choice. Do you take $\sigma x - x$ to have valuation $\le a$, or $< a$? Maybe you want to say that it acts trivially on the valuation ring modulo some power of the maximal ideal?

[Kevin Buzzard]

Each element x of the value group on the right side of 1 (I'm assuming <= 1) gives you two ideals of the valuation ring, J_{<=x} and J_x, and you can define I_{<=x} and I_{<x} to be the things fixing R / this ideal.

[Adam Topaz]

Yeah sure but not every ideal is of this form

[Adam Topaz]

Maybe one should index them by the ideals

[Kevin Buzzard]

Oh I see, you're saying that using ideals is even more general.

[Kevin Buzzard]

And then there's a map from nat into the ideals sending n to max^n and there's your higher ramification groups.

[Adam Topaz]

Now what about the upper numbering?

[Kevin Buzzard]

For me that's defined for finite extensions only, from the lower numbering, via this combinatorial voodoo, and then this miracle theorem that it's well-behaved under quotients (unlike the lower numbering, which is only well-behaved under subs), and then you can define it for arbitrary Galois extensions. OK completely dumb question: what's the relationship between the upper numbering higher ramification groups (indexed by Q) in the absolute Galois group of a p-adic field e.g. Q_p, and the filtration on inertia which we have, indexed by the ideals of Z_p-bar?

[Adam Topaz]

Kevin, these are the right questions, but I've exhausted what I can do on my phone while also making breakfast. I'll have to come back to this later ;)

[Michail Karatarakis]

Hi, I have defined the decomposition subgroup as the pullback along the map ( L ≃ₐ[K] L) →* ( L ≃ₐ[K] L)ᵐᵒᵖ(which should be an isomorphism..)

import ring_theory.valuation.valuation_subring
import group_theory.group_action.basic
import algebra.group.opposite

variables {K L: Type*} [field K] [field L] [algebra K L]

def valuation_subring.comap  (A : valuation_subring L) (e  : K →+* L) :
  valuation_subring K :=
{ mem_or_inv_mem' := λ k, by simp [valuation_subring.mem_or_inv_mem],
  ..(A.to_subring.comap e) }

instance : mul_action (L ≃ₐ[K] L)ᵐᵒᵖ (valuation_subring L) :=
{ smul := λ e A, A.comap (e.unop : L ≃ₐ[K] L),
  one_smul := begin rintro b, simp, ext1, split, rintro k, exact k, rintro h, exact h, end,
  mul_smul := λ x y b, by refl,}

open mul_opposite

def decomposition_group.comap (A : valuation_subring L) (d : ( L ≃ₐ[K] L) →* ( L ≃ₐ[K] L)ᵐᵒᵖ ):
subgroup (L ≃ₐ[K] L) := {
 .. ((mul_action.stabilizer  (L ≃ₐ[K] L)ᵐᵒᵖ A  ).comap d)
}

Does this work? This function might need to take a valuation on L as input. Any tricks for that?

[Yaël Dillies]

The pullback that you should use is docs#subgroup.opposite (once #16271 is in).

[Michail Karatarakis]

@Yaël Dillies Using #16271 we get what you wrote before (unless you have something else in mind) :

def decomposition_subgroup : subgroup (L ≃ₐ[K] L) :=
subgroup.opposite.symm ( mul_action.stabilizer (L ≃ₐ[K] L)ᵐᵒᵖ A)

It's using the map (L ≃ₐ[K] L)ᵐᵒᵖ → L ≃ₐ[K] L , whereas I am using (L ≃ₐ[K] L) →* (L ≃ₐ[K] L)ᵐᵒᵖ

Don't we need to have a valuation on L as input ? I am not clear about what's wrong with these two definitions.

[Michail Karatarakis]

Additionally, is there a correct way to promote the decomposition subgroup to a group?

[Kevin Buzzard]

The input is A. These definitions look fine to me. You can golf your proof of one_smul: the simp doesn't do anything so you can just remove it (and it is not good style anyway because it's not a terminal simp) and when you see rintro X, exact X you should be thinking "that's the identity map"; indeed instead of split, ... you can just finish the proof with refl because by this point your goal is of the form X <-> Y with X and Y definitionally equal.

The way to promote the subgroup to a group is just to start talking about it as if it were a type; when Lean is expecting a type and you provide it with a term it will look in the typeclass system to see if there are any coercions around which promote the term to a type, and it will find one and apply it; you know it's happened because you'll see one of those funny ↥ arrows, which in this case will indication an application of the function set_like.has_coe_to_sort.

[Michail Karatarakis]

OK, thank you. I golfed the proof above.

[Michail Karatarakis]

You mean that this coercion will happen automatically if I treat the decomposition subgroup as a group?

[Michail Karatarakis]

OK, then perhaps I could experiment by defining the inertia group ( subgroup for the Galois group, and, as the pointwise stabilizer of the decomposition group acting on the residue field ? ) There is docs#valuation_subring.pointwise_mul_action. Is this the action that we need?

[Michail Karatarakis]

Using this definition,

def decomposition_group : subgroup (L ≃ₐ[K] L) :=
subgroup.opposite.symm ( mul_action.stabilizer (L ≃ₐ[K] L)ᵐᵒᵖ A)

the definition:

instance {D:Type*} (D: decomposition_group) : mul_action D (local_ring.residue_field L):= sorry

yields a (deterministic) timeout error (if I try to remove the sorry)- Could someone explain what's this error about ?

Furthermore, why doesn't this definition

instance {D:Type*} (D: decomposition_group) :
pointwise_mul_action D (local_ring.residue_field L):= sorry

work? I am not clear about the syntax here; doesn't pointwise_mul_action behave like mul_action?

[Adam Topaz]

Can you provide a #mwe ?

[Michail Karatarakis]

Right,

import ring_theory.valuation.valuation_subring
import group_theory.group_action.basic
import algebra.group.opposite

variables {K L: Type*} [field K] [field L] [algebra K L] [A :valuation_subring L]

def valuation_subring.comap  (A : valuation_subring L) (e  : K →+* L) :
  valuation_subring K :=
{ mem_or_inv_mem' := λ k, by simp [valuation_subring.mem_or_inv_mem],
  ..(A.to_subring.comap e) }

instance : mul_action (L ≃ₐ[K] L)ᵐᵒᵖ (valuation_subring L) :=
{ smul := λ e A, A.comap (e.unop : L ≃ₐ[K] L),
  one_smul := λ b, by { ext1, refl},
  mul_smul := λ x y b, by refl,}

def decomposition_group : subgroup (L ≃ₐ[K] L) :=
subgroup.opposite.symm ( mul_action.stabilizer (L ≃ₐ[K] L)ᵐᵒᵖ A)


--The following gives the timeout error

instance {D:Type*} (D: decomposition_group) : mul_action D (local_ring.residue_field L):= sorry

--The following doesn't compile

instance {D:Type*} (D: decomposition_group) :
pointwise_mul_action D (local_ring.residue_field L):= sorry

[Adam Topaz]

The line

instance {D:Type*} (D: decomposition_group) : mul_action D (local_ring.residue_field L):= sorry

is not what you want.

[Adam Topaz]

It seems you're still confused about types vs terms.

[Adam Topaz]

What this line is saying, in words, is this: Let $D$ be a type, and let $D$ be an element of decomposition_group (which is a function, so that doesn't make sense). Then there is a multiplicative action of $D$ (but which one? there are two D's introduced) on the residue field of $L$.

[Adam Topaz]

Besides those issues, there is also no valuation mentioned whatsoever -- you're taking the residue field of the field $L$, which is a local ring since it has a unique maximal ideal (the trivial ideal). The residue field in this case is isomorphic to $L$ itself.

[Adam Topaz]

There is also an issue that your valuation ring variable is in square brackets. Those brackets are reserved for typeclass parameters whereas valuation_subring L is the type of (bundled) valuation subrings of the field L.

[Adam Topaz]

I don't know what this pointwise_mul_action is supposed to accomplish, but in any case, here is some code to get you started:

import ring_theory.valuation.valuation_subring
import group_theory.group_action.basic
import algebra.group.opposite

variables {K L: Type*} [field K] [field L] [algebra K L]

def valuation_subring.comap (A : valuation_subring L) (e  : K →+* L) :
  valuation_subring K :=
{ mem_or_inv_mem' := λ k, by simp [valuation_subring.mem_or_inv_mem],
  ..(A.to_subring.comap e) }

instance : mul_action (L ≃ₐ[K] L)ᵐᵒᵖ (valuation_subring L) :=
{ smul := λ e A, A.comap (e.unop : L ≃ₐ[K] L),
  one_smul := λ b, by { ext1, refl},
  mul_smul := λ x y b, by refl,}

variable (K)

def valuation_subring.decomposition_group
  (A : valuation_subring L) : subgroup (L ≃ₐ[K] L) :=
subgroup.opposite.symm ( mul_action.stabilizer (L ≃ₐ[K] L)ᵐᵒᵖ A)

variable {K}

instance (A : valuation_subring L):
  mul_action (A.decomposition_group K) (local_ring.residue_field A) := sorry

[Michail Karatarakis]

Adam Topaz said:

The line

instance {D:Type*} (D: decomposition_group) : mul_action D (local_ring.residue_field L):= sorry

is not what you want.

Sure, I just haven't encountered that timeout error before and I was wondering what it's about.

[Kevin Buzzard]

If Lean is expecting X and you give it Y, then it might put some effort into figuring out how Y's can be interpreted as X's. If you give it junk and Y can't be coerced into X then Lean might spend forever trying to do something impossible.

[Michail Karatarakis]

Hi, I have this MWE so far

import ring_theory.valuation.valuation_subring
import group_theory.group_action.basic
import algebra.group.opposite

variables {K L: Type*} [field K] [field L] [algebra K L]

def valuation_subring.comap (A : valuation_subring L) (e  : K →+* L) :
  valuation_subring K :=
{ mem_or_inv_mem' := λ k, by simp [valuation_subring.mem_or_inv_mem],
  ..(A.to_subring.comap e) }

instance : mul_action (L ≃ₐ[K] L)ᵐᵒᵖ (valuation_subring L) :=
{ smul := λ e A, A.comap (e.unop : L ≃ₐ[K] L),
  one_smul := λ b, by {ext1, refl},
  mul_smul := λ x y b, by refl,}

variable (K)

def valuation_subring.decomposition_group
  (A : valuation_subring L) : subgroup (L ≃ₐ[K] L) :=
subgroup.opposite.symm ( mul_action.stabilizer (L ≃ₐ[K] L)ᵐᵒᵖ A)

variable {K}

instance (A : valuation_subring L):
mul_action (A.decomposition_group K) (local_ring.residue_field A) :=
{ smul:= λ a k, k,
  one_smul:= λ a, by refl,
  mul_smul:= λ x y a, by refl,}

def valuation_subring.inertia_group (A : valuation_subring L) : subgroup (L ≃ₐ[K] L) :=
  {
   -- ..((mul_action.stabilizer (A.decomposition_group K) (local_ring.residue_field A) ) )
  }

The goal is to complete the definition of the inertia group as the stabilizer of the action of the decomposition group on the residue field.

Is this the correct way to define it ? - I am confused about how to complete this carrier. Removing the comment indicates that the carrier has type set ↥(valuation_subring.decomposition_group K A) but is expected to have type set (L ≃ₐ[K] L) What could be the right syntax, or, what could I use from the library to complete this coercion?

[Alex J. Best]

docs#mul_action.stabilizer is the stabilizer of a single point of a group acting on a Type, so you would really want the intersection of all the stabilizers of all points I guess, I don't know if we have this definition as a thing already in mathlib

[Alex J. Best]

Probably you could use the kernel of docs#mul_action.to_perm_hom for this

[Adam Topaz]

You defined the action on the residue field to be trivial. That's not the correct action.

[Kevin Buzzard]

And the whole point of doing it this way around is that the subgroup you'll get is a subgroup of the decomposition group, not of the full Galois group.

[Alex J. Best]

I think thats the type error above, even Lean wants to define a subgroup of the decomposition group! I couldn't work out how to get a subgroup of a subgroup into a subgroup the original group though, do we have that somewhere?

[Kevin Buzzard]

Just push it forward along the homomorphism with map.

[Alex J. Best]

Yeah idk why I was just expecting a name for that, but that makes total sense.

[Michail Karatarakis]

Alex J. Best said:

I think thats the type error above, even Lean wants to define a subgroup of the decomposition group! I couldn't work out how to get a subgroup of a subgroup into a subgroup the original group though, do we have that somewhere?

Yeah, that's what I got stuck on. The plan was to define the inertia as a subgroup of the Galois group and then to prove perhaps a theorem that says that it's a subgroup of the decomposition group. I thought there would be a coercion somewhere in that definition.

[Michail Karatarakis]

So what could I do to fix it?

[Michail Karatarakis]

What confused me was that, that theorem was being "asked for" in the definition.

[Michail Karatarakis]

Adam Topaz said:

You defined the action on the residue field to be trivial. That's not the correct action.

Right, what action do we need for this? All I know is that the decomposition group acts pointwise on the residue field.

[Junyan Xu]

You need to define a sub_mul_action (A.decomposition_group K) L with carrier := A (I'm not sure if the mul_action is already inferred by instance search). Then you sort of want to use docs#add_action.quotient_action with H := local_ring.maximal_ideal A, but we have a mul_action not add_action; the best way out of this is to consider the action on multiplicative L, I think. Another thing to beware of is that you should only be able to define a (left) mul_action of the mul_opposite (A.decomposition_group K)ᵐᵒᵖ.

[Michail Karatarakis]

Thanks for the clarification. But how can I combine this with what @Adam Topaz already defined below ? - This is a different action.

instance (A : valuation_subring L):
mul_action (A.decomposition_group K) (local_ring.residue_field A) := sorry

[Adam Topaz]

Right, you first need to define an action of the decomposition group by ring isomorphisms on $A$ itself, then use the fact that $A$ is local to descend this action to an action on the residue field.

[Junyan Xu]

Yeah I was just pointing out some intermediate defs you need to get to the end goal, and that the end goal should involve the mul_opposite of (A.decomposition_group K).

[Adam Topaz]

Well, the decomposition group should be a subgroup of the Galois group, so it should just be a regular left action on A.

[Adam Topaz]

Michail already converted from the stabilizer (which is a subgroup of the opposite group) to a subgroup of the Galois group using docs#subgroup.opposite

[Adam Topaz]

Note that we do have docs#distrib_mul_action which includes compatibility with addition. But the action on the ring is really by ring automorphisms, and as far as I know we don't have a way to speak nicely about actions by ring automorphisms.

[Junyan Xu]

Notice that if you use docs#mul_action.quotient_action with H := docs#add_subgroup.to_subgroup (local_ring.maximal_ideal A), then inv_mul_mem boils down to a' - a ∈ H → b • a' - b • a ∈ H, so you just need distrib_mul_action + a little bit.

[Junyan Xu]

docs#subgroup.opposite doesn't turn an action by mul_opposite (i.e. a right action) to an action by the original group (i.e. a left action) because it's simply the identity; docs#mul_equiv.inv' could do that because it inserts an inverse. So mul_action.stabilizer (L ≃ₐ[K] L)ᵐᵒᵖ A inherits the mul_action from (L ≃ₐ[K] L)ᵐᵒᵖ (probably by typeclass inference), but when you convert it to a subgroup of (L ≃ₐ[K] L) using subgroup.opposite.symm, it no longer has a mul_action. So I think it's better to consider the action of mul_action.stabilizer (L ≃ₐ[K] L)ᵐᵒᵖ A and get an the inertia subgroup as a subgroup of it instead of A.decomposition_group K, and only convert it to a subgroup of (L ≃ₐ[K] L) in the end if you really want to do that.

[Adam Topaz]

But there is no mul action of mul_action.stabilizer (L ≃ₐ[K] L)ᵐᵒᵖ A. It's a stabilizer! The action is trivial (on A as a set).

[Adam Topaz]

Since it stabilizes A as a set, the mul action induced by that of the Galois group on $L$ restricts to an action of $A$.

[Adam Topaz]

What we DO have is a mul_action of a subgroup of the Galois group of $L|K$ on $L$. That should be called docs#subgroup.mul_action maybe?

[Adam Topaz]

What Michail now needs to prove is that this mul_action of the decomposition group, when acting on $L$, restricts to an action of $A$.

[Adam Topaz]

Here's a bit more code... once those sorries are done, it would be a good exercise to obtain the action on the residue field by showing that the action on $A$ preserves the maximal ideal.

import ring_theory.valuation.valuation_subring
import group_theory.group_action.basic
import algebra.group.opposite

variables {K L: Type*} [field K] [field L] [algebra K L]

def valuation_subring.comap (A : valuation_subring L) (e  : K →+* L) :
  valuation_subring K :=
{ mem_or_inv_mem' := λ k, by simp [valuation_subring.mem_or_inv_mem],
  ..(A.to_subring.comap e) }

instance : mul_action (L ≃ₐ[K] L)ᵐᵒᵖ (valuation_subring L) :=
{ smul := λ e A, A.comap (e.unop : L ≃ₐ[K] L),
  one_smul := λ b, by { ext1, refl},
  mul_smul := λ x y b, by refl,}

variable (K)

def valuation_subring.decomposition_group
  (A : valuation_subring L) : subgroup (L ≃ₐ[K] L) :=
subgroup.opposite.symm (mul_action.stabilizer (L ≃ₐ[K] L)ᵐᵒᵖ A)

example (A : valuation_subring L) :
  mul_action (A.decomposition_group K) L :=
infer_instance

def valuation_subring.sub_mul_action (A : valuation_subring L) :
  sub_mul_action (A.decomposition_group K) L :=
{ carrier := A,
  smul_mem' := sorry }

instance decomposition_group.mul_action (A : valuation_subring L) :
  distrib_mul_action (A.decomposition_group K) A :=
{ smul_add := sorry,
  smul_zero := sorry,
  ..(sub_mul_action.mul_action (A.sub_mul_action K)) }

[Junyan Xu]

Oh yeah I was confused. I agree that you should be able to do sub_mul_action (A.decomposition_group K) L with carrier A. The reason is that the action on valuation subrings is via comap, which implicitly introduces an inverse relative to the action on elements: with the definition of mul_action (L ≃ₐ[K] L)ᵐᵒᵖ (valuation_subring L) it holds that a ∈ A → e⁻¹ • a ∈ e • A, i.e. to make the two actions compatible you need an inverse. Without using inverse, this can be written e • a ∈ A → a ∈ e • A, i.e. the two actions are not compatible but "adjoint".

[Eric Wieser]

Isn't docs#mul_semiring_action the tool to talk about actions by ring automorphisms, @Adam Topaz?

[Eric Wieser]

I think we're missing the instance for ring automorphisms because we're also missing the monoid structure (by composition) of ring automorphisms

[Eric Wieser]

But we have the version for alg_equiv

[Eric Wieser]

Also, can't you just define the decomposition group in terms of the existing docs#valuation_subring.pointwise_mul_action instead of making a new mul_action instance (defined via map instead of comap)? After all, comaping by e is just mapping by e⁻¹?

[Adam Topaz]

Ah! Great! I didn't know this pointwise mul action existed!

[Adam Topaz]

BTW the docstring for docs#subring.pointwise_mul_action sounds wrong to me (similarly for the valuation one).

[Adam Topaz]

It's not the action on a subring, but rather the action on the type of all subrings.

[Junyan Xu]

I guess we should add the following class/instances?

import group_theory.group_action.quotient
import ring_theory.ideal.quotient

universes u v

variables {α : Type u} (β : Type v) [monoid β]

class mul_action.add_quotient_action [add_group α] [mul_action β α] (H : add_subgroup α) : Prop :=
(neg_add_mem : ∀ (b : β) {a a' : α}, -a + a' ∈ H → -(b • a) + (b • a') ∈ H)
/- `inv_mul_mem` in docs#add_action.quotient_action should also be called `neg_add_mem`. -/

instance mul_action.add_quotient [add_group α] [mul_action β α] (H : add_subgroup α)
  [mul_action.add_quotient_action β H] : mul_action β (α ⧸ H) := sorry
/- The above are analogous to docs#mul_action.quotient_action, docs#mul_action.quotient -/

instance distrib_mul_action.add_quotient [add_group α] [distrib_mul_action β α] (H : add_subgroup α)
  [mul_action.add_quotient_action β H] [H.normal] : distrib_mul_action β (α ⧸ H) := sorry

instance mul_distrib_mul_action.add_quotient [comm_ring α] [mul_distrib_mul_action β α] (I : ideal α)
  [mul_action.add_quotient_action β I.to_add_subgroup] : mul_distrib_mul_action β (α ⧸ I) := sorry

instance mul_semiring_action.add_quotient [comm_ring α] [mul_semiring_action β α] (I : ideal α)
  [mul_action.add_quotient_action β I.to_add_subgroup] : mul_semiring_action β (α ⧸ I) := sorry

[Junyan Xu]

And we probably also want the following, but the current algebra hierarchy doesn't yet allow us to state them properly:

instance submodule.distrib_mul_action [add_monoid α] [distrib_mul_action β α]
  (p : submodule β α) : distrib_mul_action β p := sorry
/- Analogous to docs#sub_mul_action.mul_action.
  We want p to be both a sub_mul_action and a submonoid, i.e. a submodule, but the current
  typeclass requirement for submodule is too strong. Relax it? -/

instance submonoid'.mul_distrib_mul_action [monoid α] [mul_distrib_mul_action β α]
  (p : submonoid α /- + smul_mem -/) : mul_distrib_mul_action β p := sorry

instance subsemiring'.mul_semiring_action [semiring α] [mul_semiring_action β α]
  (p : subsemiring α /- + smul_mem -/) : mul_semiring_action β p := sorry

[Eric Wieser]

I already tried relaxing the typeclass requirements for submodule sometime last year, but ran into timeouts

[Michail Karatarakis]

Hi, I have the following MWE :

import ring_theory.valuation.valuation_subring
import group_theory.group_action.basic
import algebra.group.opposite

variables {K L: Type*} [field K] [field L] [algebra K L]

def valuation_subring.comap (A : valuation_subring L) (e  : K →+* L) :
  valuation_subring K :=
{ mem_or_inv_mem' := λ k, by simp [valuation_subring.mem_or_inv_mem],
  ..(A.to_subring.comap e) }

instance : mul_action (L ≃ₐ[K] L)ᵐᵒᵖ (valuation_subring L) :=
{ smul := λ e A, A.comap (e.unop : L ≃ₐ[K] L),
  one_smul := λ b, by { ext1, refl},
  mul_smul := λ x y b, by refl,}

variable (K)

def valuation_subring.decomposition_group
  (A : valuation_subring L) : subgroup (L ≃ₐ[K] L) :=
subgroup.opposite.symm (mul_action.stabilizer (L ≃ₐ[K] L)ᵐᵒᵖ A)

example (A : valuation_subring L) :
  mul_action (A.decomposition_group K) L := infer_instance

def valuation_subring.sub_mul_action (A : valuation_subring L) :
  sub_mul_action (A.decomposition_group K) L :=
{ carrier := A,
  smul_mem' := begin
  rintros d l h,
  sorry
  end
   }

It looks simple enough but I keep missing something. Is there anything in the library I could use, or any specific lemmata I shall define first?

However, concerning the previous conversation:

~Do we need to define the decomposition group in terms of that pointwise mul action instead?

[Kevin Buzzard]

So your d has type ↥(valuation_subring.decomposition_group K A), which means "subgroup (a term), promoted to a group (a type)". If you could get your hands on what was _actually_ going on, i.e. an element of the full Galois group L ≃ₐ[K] L and a proof that it's in the subgroup (and in particular if you could get rid of the ↥ coercion) then probably you could make more progress. The way to do this is literally to take d apart. To give a term of type ↥(valuation_subring.decomposition_group K A) is to give a pair consisting of an element of L ≃ₐ[K] L and a proof that it's in the subgroup. So you could continue with cases d with g hg for example. Or you could just do everything in one go with rintros ⟨g, hg⟩ l h,.

[Kevin Buzzard]

Do we need to define the decomposition group in terms of that pointwise mul action instead?

You don't _need_ to do anything. I don't quite understand the question.

[Michail Karatarakis]

Kevin Buzzard said:

Do we need to define the decomposition group in terms of that pointwise mul action instead?

You don't _need_ to do anything. I don't quite understand the question.

Right, I am referring to : https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Working.20on.20Frobenius.20elements/near/296946869

[Michail Karatarakis]

Thank you for the hint - Using cases with simp does remove the coercions, and I end up with the following:

import ring_theory.valuation.valuation_subring
import group_theory.group_action.basic
import algebra.group.opposite

variables {K L: Type*} [field K] [field L] [algebra K L]

def valuation_subring.comap (A : valuation_subring L) (e  : K →+* L) :
  valuation_subring K :=
{ mem_or_inv_mem' := λ k, by simp [valuation_subring.mem_or_inv_mem],
  ..(A.to_subring.comap e) }

instance : mul_action (L ≃ₐ[K] L)ᵐᵒᵖ (valuation_subring L) :=
{ smul := λ e A, A.comap (e.unop : L ≃ₐ[K] L),
  one_smul := λ b, by { ext1, refl},
  mul_smul := λ x y b, by refl,}

variable (K)

def valuation_subring.decomposition_group
  (A : valuation_subring L) : subgroup (L ≃ₐ[K] L) :=
subgroup.opposite.symm (mul_action.stabilizer (L ≃ₐ[K] L)ᵐᵒᵖ A)

example (A : valuation_subring L) :
  mul_action (A.decomposition_group K) L := infer_instance

def valuation_subring.sub_mul_action (A : valuation_subring L) :
  sub_mul_action (A.decomposition_group K) L :=
{ carrier := A,
  smul_mem' := begin
  rintros ⟨g, hg⟩ l h,
  simp at *,
  end }

which I find a bit confusing: I am looking for a proof involving an action of a tuple ⟨g, hg⟩ • l ∈ A instead, where g : L ≃ₐ[K] L and hg : g ∈ valuation_subring.decomposition_group K A . Is there anything more I could do from here?
Furthermore, library_search curiously gives several errors concerning the types instead of the usual timeout or indicating that it hasn't found something.

[Kevin Buzzard]

Are you claiming that simp at * closes the goal? It doesn't for me. If I do this:

  rintros ⟨g, hg⟩ l h,
  simp at *,
  change g • l ∈ A,

(this works because ⟨g, hg⟩ • l ∈ A is definitionally equal to g • l ∈ A) then we have

hg : g ∈ valuation_subring.decomposition_group K A
h : l ∈ A
⊢ g • l ∈ A

Mathematically this is trivial: it says "if g is in the subgroup which stabilises A, then it sends something in A to something in A". Well, if something is mathematically trivial like this but is causing problems in Lean then it should probably be a lemma! Indeed if I look at your code then I see a red flag: every definition in Lean comes with a cost, and the cost is that you need to make an API for that definition (i.e. a list of basic theorems about that definition). You define valuation_subring.decomposition_group and prove 0 theorems about it and then go on to make another definition, and now you're in the middle of a proof about this second definition but you find that you need a fact about the first definition. The thing to think now is not "how do I continue in this proof in the second definition", it's "let's go back and make the API for the first definition". It's important to make this API because all of this left action / right action nonsense means that it's not really as easy as one would like to close the goal from here (assuming that your code didn't clear it -- it didn't for me).

[Eric Wieser]

Arguably there is no point in having valuation_subring.decomposition_group at all, as it is a longer spelling and has less API than the equal mul_action.stabilizer (L ≃ₐ[K] L) A

[Eric Wieser]

Here's a proof of the above without any real definitions, which also follows my earlier suggestion to throw out all the mul_opposite stuff that isn't necessary

import ring_theory.valuation.valuation_subring
import group_theory.group_action.basic

variables {K L : Type*} [field K] [field L] [algebra K L]

variable (K)

open_locale pointwise

abbreviation valuation_subring.decomposition_group
  (A : valuation_subring L) : subgroup (L ≃ₐ[K] L) :=
mul_action.stabilizer (L ≃ₐ[K] L) A

def valuation_subring.sub_mul_action (A : valuation_subring L) :
  sub_mul_action (A.decomposition_group K) L :=
{ carrier := A,
  smul_mem' := λ g l h, begin
    convert set.smul_mem_smul_set h using 1,
    exact congr_arg coe g.prop.symm,
  end }

[Eric Wieser]

It also generalizes to

def valuation_subring.sub_mul_action {G : Type*}
  [group G] (A : valuation_subring L) [mul_semiring_action G L] :
  sub_mul_action (mul_action.stabilizer G A) L :=
{ carrier := A,
  smul_mem' := λ g l h, set.mem_of_mem_of_subset (set.smul_mem_smul_set h) g.prop.le }

[Eric Wieser]

Or even more generally

/-- Any set is stable under its stabilizer. -/
def set.to_stabilizer_sub_mul_action {G α : Type*} [group G] (A : set α) [mul_action G α] :
  sub_mul_action (mul_action.stabilizer G A) α :=
{ carrier := A,
  smul_mem' := λ g l h, set.mem_of_mem_of_subset (set.smul_mem_smul_set h) g.prop.le }

[Kevin Buzzard]

I think that decomposition_group needs a definition of some kind because it's a fundamental object in number theory. Here is my proposed development:

namespace valuation_subring

def decomposition_group
  (A : valuation_subring L) : subgroup (L ≃ₐ[K] L) :=
subgroup.opposite.symm (mul_action.stabilizer (L ≃ₐ[K] L)ᵐᵒᵖ A)

lemma mem_decomposition_group' (A : valuation_subring L)
  (g : L ≃ₐ[K] L) : g ∈ A.decomposition_group K ↔
    mul_opposite.op g ∈ mul_action.stabilizer (L ≃ₐ[K] L)ᵐᵒᵖ A :=
begin
  sorry
end

lemma mem_decomposition_group (A : valuation_subring L) (g : (L ≃ₐ[K] L)) :
  g ∈ A.decomposition_group K ↔ ∀ a : L, g • a ∈ A ↔ a ∈ A :=
begin
  sorry,
end

def sub_mul_action (A : valuation_subring L) :
  sub_mul_action (A.decomposition_group K) L :=
{ carrier := A,
  smul_mem' := begin
  rintros ⟨g, hg⟩ l h,
  simp at *,
  change g • l ∈ A,
  sorry,
  end }

end valuation_subring

Eric: Michail is my new PhD student and he's learning Lean right now. Don't give too many spoilers! He's supposed to be learning Lean this way! Michail: perhaps we should stop having these conversations in public, although I think Eric's idea of an abbreviation is probably better than mine.

[Eric Wieser]

Ah, if the goal is to learn lean, it might be a useful exercise to prove that mul_action.stabilizer (L ≃ₐ[K] L) A is equal to the more complicated subgroup.opposite.symm (mul_action.stabilizer (L ≃ₐ[K] L)ᵐᵒᵖ A), so that dropping the latter in favor of the former feels justified!

[Kevin Buzzard]

One thing I see in Eric's code is that we now have a left action of G on the valuation subrings?

[Eric Wieser]

Yes, that's mentioned higher up in this thread (here)