## 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).

#13465

#### 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).

#13465

#### 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!!

Last updated: Dec 20 2023 at 11:08 UTC