Galois theory applied to prime decomposition

Stream: Is there code for X?

[Xavier Roblot]

Do we have the basic Galois theory of prime ideal decomposition? We have the decomposition group via docs#MulAction.stabilizer and the inertia group docs#AddSubgroup.inertia and some results relating them to prime ideal decomposition such as docs#Ideal.card_inertia_eq_ramificationIdxIn but I don't think there is anything about the decomposition field, inertia field, and so on. One application that I would need if the fact that the compositum with an unramfied extensions is unramified.

[Kevin Buzzard]

Are you asking about local or global fields? Can you formalise the statement of what you want?

[Thomas Browning]

I'm not aware of any theory of decomposition field or inertia field in mathlib.

[Xavier Roblot]

The application I have in mind is for the global fields but the basic theory should work the same for global and local fields. Anyway, since it seems it is missing, I'll work on that unless somebody else is already working on it.

[Thomas Browning]

Decomposition and inertia fields work for any Galois extension of Dedekind domains, and maybe even with less assumptions on the rings (I don't know).

[Antoine Chambert-Loir]

In Commutative Algebra, chapter 5 (Integers), §2 (Lifting prime ideals), §2 (Decomposition and inertia groups), Bourbaki defines decomposition and inertia groups for any group acting on a ring, relative to a prime ideal of that ring, as well as the inertia ring (elements invariant under the decomposition group).

[Antoine Chambert-Loir]

Their theorem 2 asserts that for an action of a finite group $G$ on a ring $A'$, with ring of invariants $A$,

• the ring $A'$ is integral over $A$;
• the group acts $G$ transitively on the set of prime ideals of $A'$ that restrict to a common prime ideal of $A$;
• for every $\mathfrak p'\in\operatorname{Spec}(A')$ lifting $\mathfrak p\in\operatorname{Spec}(A)$, the quotient group $D_{\mathfrak p'}/I_{\mathfrak p'}$ (decomposition modulo inertia) is naturally isomorphic with the Galois group of the normal extension $\operatorname{Frac}(A'/\mathfrak p')$ of $\operatorname{Frac}(A/\mathfrak p)$.

[Antoine Chambert-Loir]

In the next section, they apply this to the more standard situation, starting from an integrally closed ring $A$, with field of fractions $K$, a normal extension $K'$ of $K$ and the integral closure $A'$ of $A$ in $L$.

[Thomas Browning]

Those results I think we basically have in RingTheory/Invariant/Basic. I think it's just the theory of the fixed fields that's missing.

[Xavier Roblot]

Well, I think the last result:

• for every $\mathfrak p'\in\operatorname{Spec}(A')$ lifting $\mathfrak p\in\operatorname{Spec}(A)$, the quotient group $D_{\mathfrak p'}/I_{\mathfrak p'}$ (decomposition modulo inertia) is naturally isomorphic with the Galois group of the normal extension $\operatorname{Frac}(A'/\mathfrak p')$ of $\operatorname{Frac}(A/\mathfrak p)$.

is missing. I'll start with this one.

[Filippo A. E. Nuccio]

How are you going to frame the "naturally"... ? :smiling_devil:

[Xavier Roblot]

Fortunately, there is already docs#IsFractionRing.stabilizerHom :slight_smile:

[Thomas Browning]

I think we basically already have this. Surjectivity is in RingTheory/Invariant/Basic, and the fact that the kernel is the inertia subgroup seems to somehow be used in NumberTheory/RamificationInertia/Galois.

[Thomas Browning]

Yeah: docs#Ideal.Quotient.ker_stabilizerHom

[Thomas Browning]

and surjectivity is docs#Ideal.Quotient.stabilizerHom_surjective

[Xavier Roblot]

Well, that makes my life a lot easier

[Xavier Roblot]

#34730

[Xavier Roblot]

So I started working on this project and made some progress but I would like to get some feedback before moving further. I am showing a bit of code in the next message (note that you need #34730 for this code to compile). The code below is still very much WIP and many things can be improved but I'd like to know if people agree with the choice for the definitions for the decomposition fields (and related objects) that I made) The short version is the following: given a setup with K fraction field of A, L fraction field of B and L/K a finite Galois extension of group G. The decomposition field of a ideal P of B is defined by

def decompField : IntermediateField K L := FixedPoints.intermediateField (stabilizer G P)

I also define

abbrev decompRing : Subalgebra A (decompField K L G P) := integralClosure A (decompField K L G P)

and

abbrev decompPrime : Ideal (decompRing A K L G P) :=
     comap (algebraMap (decompRing A K L G P) B) P

I need to add quite a number of instances for things to work but I could prove the first results about the decomposition field, for example the fact the prime p of A below P is totally split in it.

[Xavier Roblot]

Here is the code (note that this is still WIP with non optimized proofs or hypothesis):

import Mathlib.NumberTheory.RamificationInertia.Galois

theorem Nat.eq_eq_of_mul_le_mul {a b c d : ℕ} (ha : a ≤ c) (hb : b ≤ d) (hc : 0 < c) (hd : 0 < d)
    (h : c * d ≤ a * b) : a = c ∧ b = d :=
  ⟨le_antisymm ha <| Nat.le_of_mul_le_mul_right (h.trans <| Nat.mul_le_mul_left a hb) hd,
    le_antisymm hb <| Nat.le_of_mul_le_mul_left (h.trans <| Nat.mul_le_mul_right b ha) hc⟩

theorem Ideal.inertiaDeg_le_inertiaDeg {R S T : Type*} [CommRing R] [CommRing S] [CommRing T]
    [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [Module.Finite R T]
    (p : Ideal R) (P : Ideal S) (Q : Ideal T) [P.LiesOver p] [Q.LiesOver P] [p.IsMaximal] :
    Ideal.inertiaDeg P Q ≤ Ideal.inertiaDeg p Q := by
  have : Q.LiesOver p := Ideal.LiesOver.trans Q P p
  unfold Ideal.inertiaDeg
  rw [dif_pos (by rwa [← Ideal.under_def, eq_comm, ← Ideal.liesOver_iff]),
    dif_pos (by rwa [← Ideal.under_def, eq_comm, ← Ideal.liesOver_iff])]
  have : IsScalarTower (R ⧸ p) (S ⧸ P) (T ⧸ Q) := IsScalarTower.of_algebraMap_eq <| by
    rintro ⟨x⟩; exact congr_arg _ (IsScalarTower.algebraMap_apply R S T x)
  exact Module.finrank_top_le_finrank_of_isScalarTower _ _ _

theorem Ideal.ramificationIdx_le_ramificationIdx {R S T : Type*} [CommRing R] [CommRing S]
    [CommRing T] (p : Ideal R) (P : Ideal S) (Q : Ideal T) (f : R →+* S) (g : S →+* T)
    (hp : p = Ideal.comap f P) (h : BddAbove {n | map (g.comp f) p ≤ Q ^ n}) :
    Ideal.ramificationIdx g P Q ≤ Ideal.ramificationIdx (g.comp f) p Q := by
  unfold Ideal.ramificationIdx
  refine csSup_le_csSup' h fun n hn ↦ ?_
  rw [Set.mem_setOf_eq, ← map_map, map_le_iff_le_comap, map_le_iff_le_comap, hp]
  apply Ideal.comap_mono
  rwa [← Ideal.map_le_iff_le_comap]

theorem Ideal.IsDedekindDomain.ramificationIdx_le_ramificationIdx {R S T : Type*} [CommRing R]
    [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T]
    [Module.IsTorsionFree R T] [IsDomain R] [IsDedekindDomain T]
    (p : Ideal R) (P : Ideal S) (Q : Ideal T) [Q.LiesOver p] [P.LiesOver p] [Q.IsPrime]
    (hp : p ≠ ⊥) :
    Ideal.ramificationIdx (algebraMap S T) P Q ≤ Ideal.ramificationIdx (algebraMap R T) p Q := by
  rw [IsScalarTower.algebraMap_eq R S T]
  refine Ideal.ramificationIdx_le_ramificationIdx p P Q (algebraMap R S) (algebraMap S T) ?_ ?_
  · rwa [← under_def, ← liesOver_iff]
  · rw [← IsScalarTower.algebraMap_eq R S T]
    suffices ramificationIdx (algebraMap R T) p Q ≠ 0 by
      contrapose! this
      exact ramificationIdx_eq_zero (by rwa [not_bddAbove_iff] at this)
    exact ramificationIdx_ne_zero_of_liesOver _ hp

noncomputable section

open MulAction Pointwise Ideal

set_option linter.unusedSectionVars false

variable (A K L : Type*) {B : Type*} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K]
  [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L]
  [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsFractionRing B L]

variable (G : Type*) [Group G] [Finite G] [MulSemiringAction G L] [IsGaloisGroup G K L]
  [MulSemiringAction G B] [SMulDistribClass G B L] [IsIntegrallyClosed A] [Algebra.IsIntegral A B]
  [IsGaloisGroup G A B]

variable (p : Ideal A) (P : Ideal B) [P.LiesOver p]

/-- Def. -/
def decompField : IntermediateField K L := FixedPoints.intermediateField (stabilizer G P)

/-- Def. -/
abbrev decompRing : Subalgebra A (decompField K L G P) := integralClosure A (decompField K L G P)

local notation3 "LD" => decompField K L G P
local notation3 "𝓞D" => decompRing A K L G P

variable [IsIntegralClosure B A L]

instance : IsScalarTower A 𝓞D L :=
  IsScalarTower.of_algebraMap_eq' rfl

instance : Algebra 𝓞D B := (IsIntegralClosure.lift A (S := 𝓞D) B L).toRingHom.toAlgebra

/-- Def. -/
abbrev decompPrime : Ideal 𝓞D := comap (algebraMap (decompRing A K L G P) B) P

local notation3 "𝓟D" => decompPrime A K L G P

variable [FiniteDimensional K L] [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B]
  [Module.IsTorsionFree A B] [p.IsMaximal] [P.IsMaximal] [Algebra.IsSeparable (A ⧸ p) (B ⧸ P)]

theorem rank_decompField_left (hp : p ≠ ⊥) :
    Module.finrank LD L = p.ramificationIdxIn B * p.inertiaDegIn B := by
  rw [← card_stabilizer_eq (G := G) p hp P]
  exact IsGaloisGroup.finrank_fixedPoints_eq_card_subgroup G K L (stabilizer G P)

theorem rank_decompField_right (hp : p ≠ ⊥) :
    Module.finrank K LD = (p.primesOver B).ncard := by
  refine mul_left_injective₀ (b := Module.finrank (decompField K L G P) L) ?_ ?_
  · exact Nat.pos_iff_ne_zero.mp <| Module.finrank_pos
  · dsimp only
    rw [Module.finrank_mul_finrank, rank_decompField_left A K L G p P hp,
      ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn hp B G,
      IsGaloisGroup.card_eq_finrank G K L]

instance : IsFractionRing 𝓞D LD :=
  integralClosure.isFractionRing_of_finite_extension K _

variable [Algebra.IsSeparable K L]

instance : IsDedekindDomain 𝓞D :=
  integralClosure.isDedekindDomain A K LD

instance : Module.IsTorsionFree A LD :=
  Module.IsTorsionFree.trans_faithfulSMul A K LD

instance : IsScalarTower 𝓞D B L := by
  refine IsScalarTower.of_algebraMap_eq fun x ↦ ?_
  change _ = algebraMap B L (IsIntegralClosure.lift A (S := 𝓞D) B L x)
  simp only [IsIntegralClosure.algebraMap_lift]

instance : SMulDistribClass (stabilizer G P) B L := ⟨by simp [subgroup_smul_def, smul_distrib_smul]⟩

instance : IsIntegralClosure B 𝓞D L :=
  IsIntegralClosure.tower_top (R := A)

instance : Algebra.IsIntegral 𝓞D B :=
  IsIntegralClosure.isIntegral_algebra 𝓞D L

instance : IsGaloisGroup (stabilizer G P) LD L :=
  IsGaloisGroup.subgroup G K L (stabilizer G P)

instance : IsGaloisGroup (stabilizer G P) 𝓞D B :=
  IsGaloisGroup.of_isFractionRing (stabilizer G P) _ B LD L

instance : Module.Finite A 𝓞D :=
  IsIntegralClosure.finite A K LD _

instance : Module.Finite 𝓞D B :=
  IsIntegralClosure.finite _ LD L _

instance : Module.IsTorsionFree 𝓞D B :=
  IsIntegralClosure.isTorsionFree _ L

theorem primesOver_decompPrime : primesOver 𝓟D B = {P} := by
  refine Set.eq_singleton_iff_unique_mem.mpr ⟨⟨IsMaximal.isPrime' P, over_under P⟩, ?_⟩
  rintro Q ⟨_, _⟩
  obtain ⟨σ, rfl⟩ := exists_smul_eq_of_isGaloisGroup 𝓟D P Q (stabilizer G P)
  exact σ.prop

theorem decompPrime_ne_bot (hp : p ≠ ⊥) :
    decompPrime A K L G P ≠ ⊥ :=
  under_ne_bot (decompRing A K L G P) <| ne_bot_of_liesOver_of_ne_bot hp P

theorem decompPrime_ramficationIdxIn_mul_inertiaDegIn (hp : p ≠ ⊥) :
    ramificationIdxIn 𝓟D B * inertiaDegIn 𝓟D B = p.ramificationIdxIn B * p.inertiaDegIn B := by
  have := ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn
    (decompPrime_ne_bot A K L G p P hp) B (stabilizer G P)
  rw [primesOver_decompPrime, Set.ncard_singleton, one_mul] at this
  rw [this, IsGaloisGroup.card_eq_finrank (stabilizer G P) LD L,
    rank_decompField_left A K L G p P hp]

theorem ramificationIdxIn_decompPrime (hp : p ≠ ⊥) :
    ramificationIdxIn 𝓟D B = p.ramificationIdxIn B := by
  refine (Nat.eq_eq_of_mul_le_mul ?_ ?_ ?_ ?_
    (decompPrime_ramficationIdxIn_mul_inertiaDegIn A K L G p P hp).symm.le).1
  · rw [ramificationIdxIn_eq_ramificationIdx p P G,
      ramificationIdxIn_eq_ramificationIdx _ P (stabilizer G P)]
    exact IsDedekindDomain.ramificationIdx_le_ramificationIdx _ _ _ hp
  · rw [inertiaDegIn_eq_inertiaDeg p P G, inertiaDegIn_eq_inertiaDeg _ P (stabilizer G P)]
    exact inertiaDeg_le_inertiaDeg p 𝓟D P
  · exact Nat.pos_of_ne_zero <| ramificationIdxIn_ne_zero G hp
  · exact Nat.pos_of_ne_zero <| inertiaDegIn_ne_zero G

theorem inertiaDegIn_decompPrime (hp : p ≠ ⊥) :
    inertiaDegIn 𝓟D B = p.inertiaDegIn B := by
  refine (Nat.eq_eq_of_mul_le_mul ?_ ?_ ?_ ?_
    (decompPrime_ramficationIdxIn_mul_inertiaDegIn A K L G p P hp).symm.le).2
  · rw [ramificationIdxIn_eq_ramificationIdx p P G,
      ramificationIdxIn_eq_ramificationIdx _ P (stabilizer G P)]
    exact IsDedekindDomain.ramificationIdx_le_ramificationIdx _ _ _ hp
  · rw [inertiaDegIn_eq_inertiaDeg p P G, inertiaDegIn_eq_inertiaDeg _ P (stabilizer G P)]
    exact inertiaDeg_le_inertiaDeg p (decompPrime A K L G P) P
  · exact Nat.pos_of_ne_zero <| ramificationIdxIn_ne_zero G hp
  · exact Nat.pos_of_ne_zero <| inertiaDegIn_ne_zero G

theorem ramificationIdx_decompPrime (hp : p ≠ ⊥) :
    ramificationIdx (algebraMap A 𝓞D) p 𝓟D = 1 := by
  have := ramificationIdx_algebra_tower (p := p) (P := 𝓟D) (Q := P) ?_ ?_ map_comap_le
  · rwa [← ramificationIdxIn_eq_ramificationIdx 𝓟D P (stabilizer G P),
    ramificationIdxIn_decompPrime A K L G p P hp, ramificationIdxIn_eq_ramificationIdx p P G,
    right_eq_mul₀] at this
    exact IsDedekindDomain.ramificationIdx_ne_zero_of_liesOver P hp
  · exact map_ne_bot_of_ne_bot <| decompPrime_ne_bot A K L G p P hp
  · exact map_ne_bot_of_ne_bot hp

[Thomas Browning]

Should these be predicated? I.e., IsDecompositionField or IsDecompPrime? I'm just worried that at some point you might want to apply this theory to an extension which is not defeq to what's in mathlib.

[Thomas Browning]

(Although IsDecompPrime would just be LiesOver, I guess?)

[Andrew Yang]

I agree it makes sense to have IsDecompositionField.

[Xavier Roblot]

I agree that it would be nice to have a predicate IsDecompositionField but I don't know how to define it. For the definition of the decomposition field I can think about, it is either the field fixed by stabilizer G P, that's the definition I used, or the maximal extension of L/K in which P is totally split, or the minimal extension of L/K such that P is the only prime above the prime below it. In this two last cases, it is then also of type IntermediateField K L and so we end up essentially with the same object

[Andrew Yang]

I was thinking of something like

class IsDecompositionField {OE} (D F) (P : Ideal OE) [P.IsPrime] extends
    Algebra.IsInvariant D F (stabilizer Gal(F/E) P)

[Antoine Chambert-Loir]

I may be wrong, but I'm worried with the hypotheses that rings are domains.

[Antoine Chambert-Loir]

Also, #34730 has some new lemmas under IsMaximal P, for P : Ideal A, while a similar result holds for IsPrime P, replacing quotient rings with their fraction fields (the residue field of the scheme Spec (A)).

[Xavier Roblot]

Antoine Chambert-Loir said:

Also, #34730 has some new lemmas under IsMaximal P, for P : Ideal A, while a similar result holds for IsPrime P, replacing quotient rings with their fraction fields (the residue field of the scheme Spec (A)).

@Antoine Chambert-Loir , could you please review the PR #34730 to pinpoint which results you are referring to.

[Xavier Roblot]

Andrew Yang said:

I was thinking of something like

class IsDecompositionField {OE} (D F) (P : Ideal OE) [P.IsPrime] extends
    Algebra.IsInvariant D F (stabilizer Gal(F/E) P)

I see, and I guess you mean a version where Gal(F/E) is replaced by some group G acting on F.

[Thomas Browning]

Or perhaps it should just be IsGaloisGroup (stabilizer G P) D F (which includes faithful and commutes)?

[Andrew Yang]

Xavier Roblot said:

I guess you mean a version where Gal(F/E) is replaced by some group G acting on F.

Not really, because the concept is independent of which "galois group" is chosen. So it should not take an extra G but rather have a lemma saying this imply Algebra.IsInvariant D F (stabilizer G P) for an arbitrary G.

[Thomas Browning]

Ah, define it as IsGaloisGroup (stabilizer Gal(F/E) P) D F but have API that says IsDecompositionField iff IsGaloisGroup (stabilizer G P) D F for any IsGaloisGroup G F E?

[Xavier Roblot]

Ok, thanks for the suggestion. I'll try that.

[Antoine Chambert-Loir]

Naïve question (should be moved elsewhere): if I wish to play with the PR of somebody else, say #34730, what should I do to have it on my computer?

[Etienne Marion]

If things are correctly setup (as instructed here: https://leanprover-community.github.io/contribute/git.html), gh pr checkout 34730 should work.

[Antoine Chambert-Loir]

For @Xavier Roblot , the issue is the primesOver_finite is proved under the too stringent hypothesis that one has an extension of Dedekind rings. Using the theory of Artin rings, it works in much greater generality.

[Xavier Roblot]

Antoine Chambert-Loir said:

For Xavier Roblot , the issue is the primesOver_finite is proved under the too stringent hypothesis that one has an extension of Dedekind rings. Using the theory of Artin rings, it works in much greater generality.

I quite agree but that's definitely over my pay grade. I suspect there are lot of similar results that use IsDedekindDomain as hypothesis since it is true in applications that people had in mind even though more general hypothesis could be used, but this is not a domain of math I am confortable with so I do not want to open this can of worms.

[Andrew Yang]

primesOver_finite could be generalized to docs#Algebra.QuasiFinite now that we have this typeclass.

[Antoine Chambert-Loir]

That would be a good idea to do so: that would immediately remove the docs#IsDedekindRing hypothesis from the applications and allowing for generalization while releasing the urgency of proving the appropriate instance of docs#Algebra.QuasiFinite.

[Antoine Chambert-Loir]

And this is even better than what I thought, since there is docs#Algebra.QuasiFinite.instOfFinite.

[Antoine Chambert-Loir]

Update. Adding Mathlib.RingTheory.QuasiFinite.Basic to Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas creates a cycle. Some nasty work in view.

[Andrew Yang]

Yeah Mathlib.RingTheory.QuasiFinite.Basic is quite import heavy (since one needs a bit more commutative algebra to make things work) and we should probably be careful about where to import it. That said, it should definitely not need dedekind domains to work and #34946 splits the stuff about polynomials (which needs RatFunc which is an adicCompletion which uses dedekind domains) into a separate file.

[Riccardo Brasca]

Splitting is almost always a good idea, let's merge it.

[Xavier Roblot]

@Antoine Chambert-Loir , now that #34946 has been merged, are you still working on replacing IsDedekindRing by Algebra.QuasiFinite wherever it's appropriate or should I take a look at it?

[Antoine Chambert-Loir]

I'm not working presently on it (too many other duties); if you wish to have a look at it, that's perfectly fine for me.

[Xavier Roblot]

Wait, Algebra.QuasiFinite is not a perfect replacement for IsDedekindDomain, right? If S is a Dedekind domain that is also an R-algebra, there is no reason that Algebra.QuasiFinite R S holds in general (at least, I don't see why that would be true). So I cannot just replace [IsDedekindDomain B] by [Algebra.QuasiFinite A B] in docs#primesOver_finite without breaking things further down...

[Antoine Chambert-Loir]

IIUTC Algebra.QuasiFinite will allow to replace many proofs in IsDedekindDomain.Something.Lemmas by the more general result that a finite algebra is quasi-finite, hence that there are finitely many prime ideals over a given one.

[Antoine Chambert-Loir]

Now, docs#primesOver_finite has a strange hypothesis: B is integral over A, but not necessarily finite, and the quasi-finiteness only holds because B is assumed to be a Dedekind domain. I would guess that in all of your applications, B is obviously finite over A.

[Antoine Chambert-Loir]

There are cases where finiteness does not hold, but quasi-finiteness still holds, eg, in localizations, but I find it strange to assume the Dedekind domain property upside.

[Xavier Roblot]

Is it true that B integral over A and B Dedekind domain implies QuasiFinite A B? Is so, then maybe we just need to add this instance.

[Andrew Yang]

Yes. Basically you can take the current proof of docs#primesOver_finite and plug it into docs#Algebra.QuasiFinite.iff_finite_primesOver

[Andrew Yang]

Hmmm wait it might get more tricky if you only assume integral.

[Antoine Chambert-Loir]

What I mean is that the applications, for example to the number of prime ideals, finiteness holds by assumption, so all this issue becomes easier.

[Xavier Roblot]

Sorry but I am getting a bit confused. Are you saying that the hypotheses of docs#primesOver_finite, that is CommRing A, CommRing B, IsDedekindDomain B, Algebra A B, IsDomain A, Module.IsTorsionFree A B and Algebra.IsIntegral A B implies Algebra.QuasiFinite A B? If yes, then we should definitely add the corresponding instance. But, all the ways to prove Algebra.QuasiFinite A B that I can find need some kind of finiteness assumption that I don't know how to prove with only these hypotheses.

[Xavier Roblot]

After spending some time looking for a proof, I do not believe that the above assertion is true so my proposal is the following:

1. Leave docs#primesOver_finite as it is
2. Everywhere docs#primesOver_finite is used, see if an additional finiteness assertion is present. If so, try to replace docs#primesOver_finite by docs#Algebra.QuasiFinite.finite_primesOver and get rid of the IsDedekindDomain hypothesis.

[Xavier Roblot]

Well, I didn't find any place where it made sense to do this change...

[Xavier Roblot]

#35303

[Jz Pan]

Interestingly, I'm also working on decomposition subgroup and inertia subgroup, but for places (docs#AbsoluteValue). The content is not ready for mathlib yet (but the code quality is ... sort of?), but only used in the Lean Iwasawa project, see https://github.com/acmepjz/lean-iwasawa/blob/master/Iwasawalib/NumberTheory/RamificationInertia/AbsoluteValue.lean. The advantage is that it can also be defined for infinite places, unlike mathlib one which is only defined for prime ideals (= finite places).

[Jz Pan]

I've proved that my definition of decomposition and inertia are the same as the mathlib ones for finite places.

[Xavier Roblot]

Indeed, your construction is indeed more general than the one that we have. It will be probably be useful to have both eventually. It is certainly nice that your definitions agree with the ones for ideals :slight_smile: