# Zulip Chat Archive

## Stream: FLT-regular

### Topic: Discriminant of p^n-th cyclotomic field

#### Riccardo Brasca (Feb 23 2022 at 17:19):

We now have docs#is_cyclotomic_extension.discr_odd_prime: the discriminant of the `p`

-th cyclotomic field. If someone is interested, we are also almost done with the discriminant of the `p^n`

-th cyclotomic field (although we don't need it for the project). I think the only missing prerequisite for the main calculation is that if `ζ`

is a `k`

-primitive roof of unity in a `k`

-th cyclotomic extension `K/L`

, than both `K(ζ^h)/L`

and `K/K(ζ^h)`

are cyclotomic of certain order (we maybe only need one of the two, I don't remember the details).

#### Riccardo Brasca (Apr 14 2022 at 22:17):

Does someone have a nice formula for the discriminant of the `p ^ (k+1)`

-th cyclotomic field? I mean, that holds in as much cases as possible. Note that:

- if
`p`

is odd the discriminant is`(-1) ^ ((p - 1) / 2) * p ^ (p ^ k * ((p - 1) * (k + 1) - 1))`

. - if
`p = 2`

then it is:`2 ^ (k * 2 ^ k)`

if`2 ≤ k`

.`-4`

if`k = 1`

.`-1`

if`k = 0`

.

#### Riccardo Brasca (Apr 14 2022 at 22:18):

Bonus question for `p^0`

:grinning:

#### Kevin Buzzard (Apr 15 2022 at 00:35):

The conductor-discriminant formula gives a formula for this (up to sign) which is independent of everything but involves a finite product so is probably no better. For example the reason the disc of Q(zeta_p) is p^(p-2) is that p-2 of the level p Dirichlet chars have conductor p and the other one has conductor 1

#### Junyan Xu (Apr 15 2022 at 01:37):

When p=2, k=0 it's 1 right?

Wikipedia has one that works for all n > 2 (not necessarily prime power!)

image.png

#### Riccardo Brasca (Apr 15 2022 at 06:23):

Let me see if I can end up with a uniform proof. Unfortunately the non prime-power case is really more difficult and I am not going to prove it (in any case one has to prove the prime-power case to prove the general case, so it is not a waste of time).

#### Riccardo Brasca (Apr 15 2022 at 15:40):

#### Thomas Browning (Apr 16 2022 at 11:36):

Riccardo Brasca said:

Let me see if I can end up with a uniform proof. Unfortunately the non prime-power case is really more difficult and I am not going to prove it (in any case one has to prove the prime-power case to prove the general case, so it is not a waste of time).

Isn't there a general theorem that you can use: If $K$ and $L$ are number fields with coprime discriminants, then:

(a) $K$ and $L$ are linearly disjoint over $\mathbb{Q}$.

(b) $\mathcal O_{KL}=\mathcal O_K\mathcal O_L$.

(c) $\Delta_{KL}=\Delta_K^{[L:\mathbb{Q}]}\Delta_L^{[K:\mathbb{Q}]}$.

I think this should follow from relative discriminants. In particular, the divisibility $\Delta_K^{[L:\mathbb{Q}]}\Delta_L^{[K:\mathbb{Q}]}\mid\Delta_{KL}$ should follow from relative discriminants and the coprimality assumption, and the other direction is given by the inclusion $\mathcal O_K\mathcal O_L\leq\mathcal O_{KL}$.

#### Riccardo Brasca (Apr 16 2022 at 12:16):

Yes, I mean it is harder in Lean.

#### Ruben Van de Velde (Apr 16 2022 at 12:45):

Do we have any of that in mathlib yet?

#### Riccardo Brasca (Apr 16 2022 at 18:46):

The discriminant was introduced for this project, so the answer is probably no. I don't think we have a reasonable way of saying "linearly disjoints"

#### Kevin Buzzard (Apr 16 2022 at 19:40):

We have all this stuff in lattice theory and subfields are a lattice, right?

#### Thomas Browning (Apr 16 2022 at 21:17):

Linearly disjoint means something stronger than disjoint, I think. But I think it's parts (b) and (c) of the theorem that are more relevant here.

#### Riccardo Brasca (Apr 21 2022 at 15:26):

I just realized that, since `1 / 2 = 0`

, the formula

```
Δ = (-1) ^ ((p ^ (k + 1).totient) / 2) * p ^ (p ^ k * ((p - 1) * (k + 1) - 1))
```

where `Δ`

is the discriminant of a `p ^ (k + 1)`

-th cyclotomic extension, holds also if `p = 2`

and `k = 0`

:rolling_on_the_floor_laughing:

#### Riccardo Brasca (Apr 21 2022 at 19:34):

#13585

The ring of integers is finally PRed.

#### Riccardo Brasca (Apr 21 2022 at 19:42):

This was the first milestone. I will try next week to make a reasonable plan for the near future.

#### Riccardo Brasca (Apr 25 2022 at 11:34):

I had a bike accident and I still have to find out a confortable position to work, so I am not thinking about this at the moment, but I hope I will be able to use a computer soon

#### Yaël Dillies (Apr 25 2022 at 11:35):

Hope you're doing okay!

#### Chris Birkbeck (Apr 25 2022 at 11:39):

Oh man that sucks! Hope you're ok!

#### Anne Baanen (Apr 25 2022 at 11:41):

Hope you recover soon!

#### Eric Rodriguez (Apr 25 2022 at 11:42):

Oh my, get well soon!!

#### Riccardo Brasca (Feb 23 2022 at 17:19):

We now have docs#is_cyclotomic_extension.discr_odd_prime: the discriminant of the `p`

-th cyclotomic field. If someone is interested, we are also almost done with the discriminant of the `p^n`

-th cyclotomic field (although we don't need it for the project). I think the only missing prerequisite for the main calculation is that if `ζ`

is a `k`

-primitive roof of unity in a `k`

-th cyclotomic extension `K/L`

, than both `K(ζ^h)/L`

and `K/K(ζ^h)`

are cyclotomic of certain order (we maybe only need one of the two, I don't remember the details).

#### Riccardo Brasca (Apr 14 2022 at 22:17):

Does someone have a nice formula for the discriminant of the `p ^ (k+1)`

-th cyclotomic field? I mean, that holds in as much cases as possible. Note that:

- if
`p`

is odd the discriminant is`(-1) ^ ((p - 1) / 2) * p ^ (p ^ k * ((p - 1) * (k + 1) - 1))`

. - if
`p = 2`

then it is:`2 ^ (k * 2 ^ k)`

if`2 ≤ k`

.`-4`

if`k = 1`

.`-1`

if`k = 0`

.

#### Riccardo Brasca (Apr 14 2022 at 22:18):

Bonus question for `p^0`

:grinning:

#### Kevin Buzzard (Apr 15 2022 at 00:35):

The conductor-discriminant formula gives a formula for this (up to sign) which is independent of everything but involves a finite product so is probably no better. For example the reason the disc of Q(zeta_p) is p^(p-2) is that p-2 of the level p Dirichlet chars have conductor p and the other one has conductor 1

#### Junyan Xu (Apr 15 2022 at 01:37):

When p=2, k=0 it's 1 right?

Wikipedia has one that works for all n > 2 (not necessarily prime power!)

image.png

#### Riccardo Brasca (Apr 15 2022 at 06:23):

Let me see if I can end up with a uniform proof. Unfortunately the non prime-power case is really more difficult and I am not going to prove it (in any case one has to prove the prime-power case to prove the general case, so it is not a waste of time).

#### Riccardo Brasca (Apr 15 2022 at 15:40):

#### Thomas Browning (Apr 16 2022 at 11:36):

Riccardo Brasca said:

Isn't there a general theorem that you can use: If $K$ and $L$ are number fields with coprime discriminants, then:

(a) $K$ and $L$ are linearly disjoint over $\mathbb{Q}$.

(b) $\mathcal O_{KL}=\mathcal O_K\mathcal O_L$.

(c) $\Delta_{KL}=\Delta_K^{[L:\mathbb{Q}]}\Delta_L^{[K:\mathbb{Q}]}$.

I think this should follow from relative discriminants. In particular, the divisibility $\Delta_K^{[L:\mathbb{Q}]}\Delta_L^{[K:\mathbb{Q}]}\mid\Delta_{KL}$ should follow from relative discriminants and the coprimality assumption, and the other direction is given by the inclusion $\mathcal O_K\mathcal O_L\leq\mathcal O_{KL}$.

#### Riccardo Brasca (Apr 16 2022 at 12:16):

Yes, I mean it is harder in Lean.

#### Ruben Van de Velde (Apr 16 2022 at 12:45):

Do we have any of that in mathlib yet?

#### Riccardo Brasca (Apr 16 2022 at 18:46):

The discriminant was introduced for this project, so the answer is probably no. I don't think we have a reasonable way of saying "linearly disjoints"

#### Kevin Buzzard (Apr 16 2022 at 19:40):

We have all this stuff in lattice theory and subfields are a lattice, right?

#### Thomas Browning (Apr 16 2022 at 21:17):

Linearly disjoint means something stronger than disjoint, I think. But I think it's parts (b) and (c) of the theorem that are more relevant here.

#### Riccardo Brasca (Apr 21 2022 at 15:26):

I just realized that, since `1 / 2 = 0`

, the formula

```
Δ = (-1) ^ ((p ^ (k + 1).totient) / 2) * p ^ (p ^ k * ((p - 1) * (k + 1) - 1))
```

where `Δ`

is the discriminant of a `p ^ (k + 1)`

-th cyclotomic extension, holds also if `p = 2`

and `k = 0`

:rolling_on_the_floor_laughing:

#### Riccardo Brasca (Apr 21 2022 at 19:34):

#13585

The ring of integers is finally PRed.

#### Riccardo Brasca (Apr 21 2022 at 19:42):

This was the first milestone. I will try next week to make a reasonable plan for the near future.

#### Riccardo Brasca (Apr 25 2022 at 11:34):

I had a bike accident and I still have to find out a confortable position to work, so I am not thinking about this at the moment, but I hope I will be able to use a computer soon

#### Yaël Dillies (Apr 25 2022 at 11:35):

Hope you're doing okay!

#### Chris Birkbeck (Apr 25 2022 at 11:39):

Oh man that sucks! Hope you're ok!

#### Anne Baanen (Apr 25 2022 at 11:41):

Hope you recover soon!

#### Eric Rodriguez (Apr 25 2022 at 11:42):

Oh my, get well soon!!

Last updated: Dec 20 2023 at 11:08 UTC