crazy coercion

Stream: mathlib4

[Kevin Buzzard]

You'll know the question if you look at the output to this:

import Mathlib

def foo (q : ℕ) (a : ZMod q) : ℂ := a
#print foo

Why?? And should I worry about this?

[Anne Baanen]

Does this return a whole real number between 0 and q because we get a composition along the lines of ZMod q → Fin q → ℕ → ℂ?

[Anne Baanen]

(Substituting ℤ if q = 0 of course.)

[Oliver Nash]

@Kevin Buzzard Do I understand correctly that the point you're making is that this fails:

example (q : ℕ) (a : ZMod q) : foo q a = @ZMod.cast ℂ _ q a := rfl -- fails

because Lean has instead decided on:

example (q : ℕ) (a : ZMod q) : foo q a = Complex.ofReal (@ZMod.cast ℝ _ q a) := rfl -- succeeds

It seems wrong to me that the real numbers should be involved.

[Jireh Loreaux]

This strikes me as maybe being a CoeHead vs. CoeTail vs. CoeTC problem, but I'm not sure exactly where.

[Kevin Buzzard]

For me the coercion was going through the Gaussian integers! Is that not the case for other people??

[Oliver Nash]

If I use your import Mathlib then it does indeed go through the Gaussian integers. However when I wrote my comment above, I just pasted the definition into a file I was working on with some other imports and it went through the reals. So unfortunately it seems to depend on imports.

[Kyle Miller]

For reference (using set_option pp.coercions false):

def foo : (q : ℕ) → ZMod q → ℂ :=
fun q a ↦ FunLike.coe GaussianInt.toComplex (ZMod.cast a)

[Yury G. Kudryashov]

Did we have a diamond in Lean 3?

[Kevin Buzzard]

I don't know, but right now in mathlib4 we have this (and this is blocking some work of a student):

import Mathlib -- to import some awful coercion

variable (q : ℕ)

example (a : ZMod q) : (a : ℂ) = GaussianInt.toComplex a := by
  rfl -- a syntactic equality

example (a : ZMod q) : (a : ℂ) = ZMod.cast a := by
  sorry -- I'm stuck on this. Can assume 0 < q if necessary

[Johan Commelin]

Pretty terrible indeed!

[Johan Commelin]

We really need to remove the automated coercion from ZMod to random rings.

[Johan Commelin]

It should be conditional on some [Fact _]s, or be a local instance, or both

[Kevin Buzzard]

But we're doing Kloosterman sums and there it's really handy to be able to go from ZMod q to $\R$ so I am going to have to eat my words :-)

[Kevin Buzzard]

Actually maybe not -- perhaps we should just be using val really.

[Johan Commelin]

I don't know Kloosterman sums. But that sounds like a pretty non-canonical thing that Kloosterman was doing...

[Kevin Buzzard]

it's all about things like $\sum_{x\in \Z/q\Z}e(x^2/q)$ where $e(x):=e^{2\pi i x}$ so everything is well-defined.

[Johan Commelin]

But then you want to factor e(_/q) through ZMod q, right?

[Kevin Buzzard]

Right.

[Kevin Buzzard]

Yeah I think that for all of our sanity I'm just going to build the function $\Z/q\Z\to\mathbb{C}^\times$ sending $n$ to $r^{2\pi in/q}$ and make the API for it. But I guess there are still two questions left, namely (1) why does Lean want to go through Z[i] and (2) how do we prove that Z/n -> Z[i] -> C is the cast. Alternatively we could burninate the cast. I'm now back to agreeing with you that it's a completely evil function.

[Alex Kontorovich]

This must've been dealt with in the Bloom-Mehta formalization, no? Do I recall they dealt with Kloosterman sums (or perhaps more general exponential sums)? How did they do it?

[Alex Kontorovich]

Sorry, theirs was Lean3 and this is presumably a new Lean4 issue. Nevermind.

[Eric Wieser]

Don't we already have that map as docs3#real.angle.exp_map_circle?

[Kevin Buzzard]

I want the source to be $\Z/q\Z$, so I think that's different?

[Eric Wieser]

I assume you don't mean AddCircle (q : ℤ), even though that's defined as what you wrote?

[Kevin Buzzard]

The Lean 3 thing you linked to is eating a real.angle.

[Kevin Buzzard]

Just to be clear: the thing I want is def eZMod (q : ℕ) (x : ZMod q) : ℂ := Complex.exp (2 * Real.pi * Complex.I * x.val / q). Do you think we have it? (and the proof that it sends x+y to e(x)*e(y)?)

[Eric Wieser]

Don't you want the result to live in docs#Circle ?

[Kevin Buzzard]

No, because I immediately want to add them up.

[Eric Wieser]

What I'm suggesting is:

import Mathlib.Analysis.SpecialFunctions.Complex.Circle
import Mathlib.Analysis.Fourier.AddCircle

@[simps!]
def ZMod.toQuotient (A) [AddCommGroupWithOne A] (q : ℕ) :
    ZMod q →+ A ⧸ AddSubgroup.zmultiples (q : A) :=
  ZMod.lift _ ⟨(QuotientAddGroup.mk' _).comp (Int.castAddHom A), by simp⟩

/-- A bundled version of `AddCircle.toCircle` -/
@[simps!]
noncomputable def AddCircle.toCircleHom (r : ℝ) : AddCircle r →+ Additive circle :=
  AddMonoidHom.mk' AddCircle.toCircle AddCircle.toCircle_add

-- note that we need to introduce `K` and all the extra assumptions since `AddCircle` isn't allowed on `ℤ`.
noncomputable abbrev ZMod.toAddCircle (K) [LinearOrderedRing K] [TopologicalSpace K] [OrderTopology K] (q : ℕ) :
    ZMod q →+ AddCircle (q : K) :=
  ZMod.toQuotient K q

noncomputable abbrev ZMod.toCircle {q : ℕ} (z : ZMod q) : circle :=
  (ZMod.toAddCircle _ _ z).toCircle

noncomputable abbrev ZMod.toCircleHom (q : ℕ) : ZMod q →+ Additive circle :=
  (AddCircle.toCircleHom _).comp (ZMod.toAddCircle _ _)

[Kevin Buzzard]

But where's the map I actually want, sending x to $e^{2\pi i x/q}$?

[Kevin Buzzard]

oh is circle some subtype of C?

[Eric Wieser]

circle : SubGroup C

[Eric Wieser]

docs#circle

[Eric Wieser]

docs#AddCircle.toCircle is _almost_ the map you asked for, but we have two different spellings of ZMod and it's the wrong one

[Eric Wieser]

In particular we seem to be missing

@[simps!]
def ZMod.toIntQuotient (q : ℕ) :
    ZMod q ≃+ ℤ ⧸ AddSubgroup.zmultiples (q : ℤ) :=
  AddMonoidHom.toAddEquiv
    (ZMod.lift _ ⟨QuotientAddGroup.mk' _, by simp⟩)
    ({ toFun := (sorry : Function.Periodic (Int.cast : ℤ → ZMod q) q).lift
       map_zero' := sorry
       map_add' := sorry })
    sorry
    sorry

[Anne Baanen]

Is this not docs#Int.quotientZmultiplesEquivZMod ?

[Anne Baanen]

Or is the Periodic part important?

[Eric Wieser]

It's the neighbouring docs#Int.quotientZmultiplesNatEquivZMod