Discriminant of p^n-th cyclotomic field

Stream: FLT-regular

[Riccardo Brasca]

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]

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]

Bonus question for p^0 :grinning:

[Kevin Buzzard]

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]

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]

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]

#13465

[Thomas Browning]

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]

Yes, I mean it is harder in Lean.

[Ruben Van de Velde]

Do we have any of that in mathlib yet?

[Riccardo Brasca]

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]

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

[Thomas Browning]

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]

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]

#13585
The ring of integers is finally PRed.

[Riccardo Brasca]

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

[Riccardo Brasca]

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]

Hope you're doing okay!

[Chris Birkbeck]

Oh man that sucks! Hope you're ok!

[Anne Baanen]

Hope you recover soon!

[Eric Rodriguez]

Oh my, get well soon!!

[Riccardo Brasca]

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]

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]

Bonus question for p^0 :grinning:

[Kevin Buzzard]

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]

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]

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]

#13465

[Thomas Browning]

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]

Yes, I mean it is harder in Lean.

[Ruben Van de Velde]

Do we have any of that in mathlib yet?

[Riccardo Brasca]

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]

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

[Thomas Browning]

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]

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]

#13585
The ring of integers is finally PRed.

[Riccardo Brasca]

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

[Riccardo Brasca]

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]

Hope you're doing okay!

[Chris Birkbeck]

Oh man that sucks! Hope you're ok!

[Anne Baanen]

Hope you recover soon!

[Eric Rodriguez]

Oh my, get well soon!!