Remove `PNat` from cyclotomic fields

Stream: mathlib4

[Xavier Roblot]

At the moment, cyclotomic fields (and most of the API about roots of unity) is defined using PNat, see docs#IsCyclotomicExtension. Working with PNat is a bit of a pain, so I think it will be a good idea to switch to Nat instead. After thinking about it and doing some experiments, I think the best solution is to define cyclotomic extensions in the following way, for S : Set ℕ:

@[mk_iff]
class IsCyclotomicExtension : Prop where
  /-- For all nonzero `n ∈ S`, there exists a primitive `n`-th root of unity in `B`. -/
  exists_prim_root {n : ℕ} (hs : n ∈ S) (hs' : n ≠ 0): ∃ r : B, IsPrimitiveRoot r n
  /-- The `n`-th roots of unity, for `n ∈ S`, generate `B` as an `A`-algebra. -/
  adjoin_roots : ∀ x : B, x ∈ adjoin A {b : B | ∃ n : ℕ, n ∈ S ∧ n ≠ 0 ∧ b ^ (n : ℕ) = 1}

It is then easy to prove that

theorem diff_zero :
    IsCyclotomicExtension S A B = IsCyclotomicExtension (S \ {0}) A B := by
  simp [isCyclotomicExtension_iff, and_assoc]

and thus we can recover the fact that the elements of S are nonzero if it is necessary in the proofs.

Then, the API for extension generated by a single root of unity can be developed using a NeZero hypothesis.

I have used that idea to switch from PNat to Nat in the file Mathlib.NumberTheory.Cyclotomic.Basic. It was a bit tedious but there was no real difficulty. Still, there is a lot of work left to adapt other files. However, before going forward, I wanted to make sure that people agree that this is a good idea and that this is the way to proceed (and maybe also recruit some helping hands :slight_smile:)

[Eric Wieser]

Are the painpoints with PNat something we could write a tracking issue for and think about improving?

[Michael Stoll]

I did the first part of this, i.e., moving roots of unity from PNat to Nat(with NeZero), but stopped short of extending this to cyclotomic fields. So I appreciate @Xavier Roblot taking it upon him to continue with it!

[Michael Stoll]

(See #PR reviews > #18516: refactor roots of unity @ 💬 for the discussion thread on what I did.)

[Michael Stoll]

The main pain point is when you have n : Nat, but want to use it as input to something that eats a PNat. So it tends to make things easier if the API does not want to take PNats as input.

[Michael Stoll]

In my experience from what I did, replacing (n : PNat) with (n : Nat) [NeZero n] works very well.

[Alex Meiburg]

Would that be improved if more things returned a PNat, so that we (in general) had more PNats available to hand into things? Sort if in the vein that we desire ... \ne 0 as an argument if it suffices, but 0 < ... in the conclusion if possible

e.g. (as a totally random example) docs#Polynomial.Monic.eq_X_pow_char_pow_sub_C_pow_of_natSepDegree_eq_one could have m be a PNat instead of a Nat with the additional guarantee that it's nonzero.

[Michael Stoll]

There are way more things producing Nats than PNats. And when you have a PNat, there is a NeZero instance for it, so you can seamlessly use it in the Nat+NeZero setting.

[Alex Meiburg]

Right, I know, so I'm saying we could adjust the API to support that even better.
If docs#Polynomial.Monic.eq_X_pow_char_pow_sub_C_pow_of_natSepDegree_eq_one started with ∃ (m : PNat) ..., then when you obtain a witness from that, you get a PNat.

You can then use that PNat as a Nat in any theorems that require a Nat. If they require a Nat and a NeZero instance, that works too.

[Michael Stoll]

To get back to what I said earlier: I stopped short at looking at cyclotomic fields, because it was not clear to me how to best deal with zero. But I think just allowing it and ignoring it is likely a good approach; this is a bit similar to what I ended up doing in the context of L-series (allow the coefficient function to be defined on Nat and just throw away the value at zero).

[Eric Wieser]

Does adding this help?

instance {n} [NeZero n] : CoeDep ℕ n ℕ+ where coe := ⟨n, by have := NeZero.ne n; omega⟩

[Eric Wieser]

def i_take_a_pnat (n : ℕ+) := n

variable (n : ℕ) [NeZero n]
#check i_take_a_pnat n --works

[Michael Stoll]

Depending on the context, you may still have to provide the NeZero instance manually, e.g.,

import Mathlib

instance {n} [NeZero n] : CoeDep ℕ n ℕ+ where coe := ⟨n, by have := NeZero.ne n; omega⟩

def i_take_a_pnat (n : ℕ+) := n

variable (n : ℕ) [NeZero n]
#check i_take_a_pnat n --works

/-
type mismatch
  m + n - 1
has type
  ℕ : outParam Type
but is expected to have type
  ℕ+ : Type
-/
example {m n : ℕ} [NeZero m] [NeZero n] : i_take_a_pnat (m + n - 1) = m + n - 1 := sorry

example {m n : ℕ+} : i_take_a_pnat (m + n - 1) = m + n - 1 := rfl

[Michael Stoll]

You'd probably need something like

example {m n : ℕ} [NeZero m] [NeZero n] :
    letI : NeZero (m + n - 1) := ⟨by have := NeZero.ne n; have := NeZero.ne m; omega⟩
    i_take_a_pnat (m + n - 1) = m + n - 1 := rfl

[Michael Stoll]

(It would perhaps be nice if omega could use NeZero instances that are in the context.)

[Eric Wieser]

This works:

import Mathlib

/-- Needed to avoid `Subtype.mk`. -/
def PNat.mk (n : ℕ) (hn : 0 < n := by omega) : ℕ+ := ⟨n, hn⟩

instance {n} [NeZero n] : CoeDep ℕ n ℕ+ where coe := letI := NeZero.ne n; PNat.mk n

def i_take_a_pnat (n : ℕ+) := n

variable (n : ℕ) [NeZero n]

example {m n : ℕ} [NeZero m] [NeZero n] : i_take_a_pnat ((m + n : ℕ+) - 1) = m + n - 1 := sorry

example {m n : ℕ+} : i_take_a_pnat (m + n - 1) = m + n - 1 := rfl

[Riccardo Brasca]

Having worked a lot with cyclotomic stuff I 100% agree we made a mistake using PNat (sorry for that, my fault). Using NeZero seems to me the way to go: we write NeZero n at the beginning and then we forgot about it (is't more complicated with a set S, but currently most of the results concerns a single number).

[Riccardo Brasca]

There are probably results that hold in the case n=0, but I think we can safely ignore this.

[Kevin Buzzard]

I was aware of the PNat decision at the time (watching from afar) and I thought it was a great idea because I thought that the work on cyclo stuff would force people to develop a better PNat API. Remember that I was taught in Cambridge maths department that the naturals were PNat and I always felt it disappointing that in Lean they seemed to get far less love, because they were my favourite naturals. Can you describe in simple terms what went wrong? Was it the NeZero typeclass that spelt the end of PNat?

[Kevin Buzzard]

There are plenty of things in mathematics which literally make no sense for 0 (all the theory of multiplicative functions like $\sigma_k(n)$ is meaningless for 0, for example, and $\sigma_k(n)$ is everywhere in the early theory of modular forms); of course we can assign a junk value but then all of the theorems will say "if n isn't zero then..." as there is no sensible junk value.

[Riccardo Brasca]

If you want a very simple example of something annoying, if (a : ℕ) (b : ℕ+) you can not write a ^ b

[Riccardo Brasca]

It seems that NeZero a is much closer to the informal "Let's suppose once and forall that a is a positive natural number"

[Eric Wieser]

I think we need to develop a ppow API anyway for people using non-unital rings

[Riccardo Brasca]

Yes yes, I know. It was just an example of something currently not working well.

[Riccardo Brasca]

Similarly, I don't think we want PNat.Prime vs Nat.Prime vs Prime

[Ruben Van de Velde]

Move away from Nat.Prime entirely? :)

[Kevin Buzzard]

I'm surprised Yael is giving this a thumbs up, this will mean that anyone who wants to say "let p be a prime number" will suddenly have to import a bunch of ring theory and apparently importing ring theory is unfashionable right now...

[Kevin Buzzard]

It will also have the knock-on effect that people will be saying "I am a high school kid and I was looking at the definition of a prime number expecting it to be something I understand but what is a unique factorization monoid?" or whatever.

[Kevin Buzzard]

I should add that I'm also in favour of nuking Nat.Prime -- we have it already :-)

[Alex Meiburg]

I recently was using my own hacky version of a ppow in the quantumInfo repo, I needed a way to express "powers of a Hilbert space" in a context where we explicitly don't have a free copy of the zero-dimensional Hilbert space lying around. (This comes up a lot in quantum resource theories.)

[Alex Meiburg]

(this is a way of saying :+1:, I would like more PNat support!)

[Riccardo Brasca]

@Kevin Buzzard Note that Nat.Prime is already defined as Irreducible, so it has nothing specific to ℕ (and irreducibility can, and is, be defined in any monoid).

[Xavier Roblot]

I think this thread drifted a bit away from the original topic so I want to make sure that there is an agreement on the following: even though, it will be a go thing to get better API for PNat, if we can get rid of PNat for cyclomotic fields without too much pain, then we should do it.

[Riccardo Brasca]

But I have to admit that I read "Move away from PNat.Prime", not "from Nat.Prime" :sweat_smile:

[Riccardo Brasca]

Xavier Roblot said:

I think this thread drifted a bit away from the original topic so I want to make sure that there is an agreement on the following: even though, it will be a go thing to get better API for PNat, if we can get rid of PNat for cyclomotic fields without too much pain, then we should do it.

Yes please. What about opening a PR so anyone that has half an hour can work on that? Unless you want to do all the work of course!

[Xavier Roblot]

So far, I did not encounter too much difficulty, so I am making good progress. If I get bored at some point, I'll push my changes so that other people can work on it.

[Xavier Roblot]

I have a version that compiles here: #25114

There is probably still a lot of cleaning to be done. I am not going to work on it for quite some time, so anyone who wants to contribute is welcome to push their changes.

[Antoine Chambert-Loir]

Kevin Buzzard said:

There are plenty of things in mathematics which literally make no sense for 0 (all the theory of multiplicative functions like $\sigma_k(n)$ is meaningless for 0, for example, and $\sigma_k(n)$ is everywhere in the early theory of modular forms); of course we can assign a junk value but then all of the theorems will say "if n isn't zero then..." as there is no sensible junk value.

Looking at the Fourier expansion of the normalized Eisenstein series
$E_{2k}(\tau)= 1 - \frac{4k}{B_{2k}}\sum_{n=1}^\infty \sigma_{2k-1}(n) q^n$
one is lead to set $\sigma_{2k-1}(0)=-B_{2k}/4k$, which is off by a factor $2$, since
$-B_{2k}/2k=\zeta(1-2k)=\sum_{d=1}^\infty d^{2k-1}.$

[Antoine Chambert-Loir]

(Don't take this too seriously.)

[Kevin Buzzard]

Yes. One suggestion to fix this (also don't take it too seriously) is to imagine $E_{2k}(\tau)=\sum_{n\in\Z}\sigma_{2k-1}(n)q^{|n|}$ where $\sigma_k(n)$ for $n$ an integer means the sum of the positive divisors of $n$.

[Xavier Roblot]

The PR #25114 is ready for review