Decomposition group of ideal

Stream: mathlib4

[Suzuka Yu]

Greetings! I was thinking about using decomposition group,

$$D_{\mathfrak{p}} := \{ \sigma \in Gal(K/\mathbb{Q}) \mid \sigma(\mathfrak{p}) = \mathfrak{p}\}$$

and I found ValuationSubring.decompositionSubgroup, but it is defined with respect to valuation subring rather than ideal. So I wonder what's the connection between them? Thanks in advance!

[Johan Commelin]

I'm not entirely sure if the connection is built in mathlib. Pinging some people who will know: @María Inés de Frutos Fernández @Filippo A. E. Nuccio @Jiang Jiedong @Adam Topaz

[Notification Bot]

2 messages were moved here from #Is there code for X? > kronecker-weber by Kevin Buzzard.

[Jiang Jiedong]

Let $L/K$ be an extension of fields and $A$ be a valuation subring of $L$. As in mathlib, ValuationSubring.decompositionSubgroup is defined as the stabilizer of $A$. This is the same as the stabilizer of the maximal ideal $m$ of $A$.

So it is the same with $D_\frak{p}$ when $A$ is the localization of $\mathcal{O}_K$ with respect to $\frak{p}$.

[Johan Commelin]

@Jiang Jiedong But do we have a way of turning that localization into a bundled-up valuation subring?

[Jiang Jiedong]

As far as I know, there isn't such a direct function in mathlib...

[Suzuka Yu]

oh, I see, many thanks!

[Adam Topaz]

At the very least you can get a valuation from the prime ideal, then convert the valuation to a valuation sub ring.

[Filippo A. E. Nuccio]

The main steps to achieve this are

1. Create a term of the prime spectrum (see docs#IsDedekindDomain.HeightOneSpectrum) attached to your prime ideal.
2. Use docs#IsDedekindDomain.HeightOneSpectrum.valuation to get the valuation attached to the ideal seen as an element of the spectrum
3. The declaration docs#Valuation.valuationSubring provides the valuation subring associated to a Valuation.

[Suzuka Yu]

Filippo A. E. Nuccio 发言道：

The main steps to achieve this are

1. Create a term of the prime spectrum (see docs#IsDedekindDomain.HeightOneSpectrum) attached to your prime ideal.
2. Use docs#IsDedekindDomain.HeightOneSpectrum.valuation to get the valuation attached to the ideal seen as an element of the spectrum
3. The declaration docs#Valuation.valuationSubring provides the valuation subring associated to a Valuation.

Wow, thats very clear, thank you!

[Yongle Hu]

I have formalized the decomposition group in the case of Galois extensions of number fields, you can see the code here. I will try to submit PRs to incorporate them into the Mathlib library later.