Surjection from Z into zmod

Stream: new members

[Hanting Zhang]

Try as I might, I cannot complete this proof.

import data.zmod.basic

open function

example (n : ℕ) : surjective (algebra_map ℤ (zmod n)) :=
begin
  unfold surjective,
  intro,
  use b.val,
  simp only [int.cast_coe_nat, ring_hom.eq_int_cast],
-- n: ℕ
-- b: zmod n
-- ⊢ ↑(b.val) = b
  sorry
end

How should I proceed?

[Eric Wieser]

Does ext help?

[Eric Wieser]

(deleted)

[Hanting Zhang]

No, zmod doesn't have ext. I guess what I'm really trying to do is identify zmod n with quotients of ℤ, but there seems to be no API for this.

[Hanting Zhang]

Maybe there is some sledgehammer to do this that I haven't found yet?

[Alex J. Best]

example (n : ℕ) : surjective (algebra_map ℤ (zmod n)) :=
begin
  intro x,
  use x,
  cases n;
  simp,
end

[Alex J. Best]

Its a bit weird because zmod n is defined quite differently for n=0 and n > 0, for n = 0 zmod n is just Z and for n positive it is fin n so sometimes you need to do cases on n for the proof to work.

[Alex J. Best]

I'd say the lemma

@[simp] lemma zmod.coe_coe_eq_self {n : ℕ} (a : zmod n) : ((a : ℤ) : zmod n) = a :=
by {cases n; simp}

should be added to mathlib

[Alex J. Best]

Maybe more useful is for me to describe my process for finding the proof:
First I had, intro x and then use x.val like you did. Then I tried simp and the goal was ↑(x.val) = x so I tried the tactic norm_cast as there were up arrows in the goal, but it didn't help, so I thought maybe using val was not the right format for cast to work, so switched it to use x so that lean would insert a cast itself, so the goal after simp was then, ↑↑x = x so I tried library search, nothing happened so I searched mathlib for the string coe_coe and found a bunch of things including docs#fin.coe_coe_eq_self which seemed very useful. And so I thought that this lemma would work, as zmod is basically the same as fin, so I looked up the definition of zmod in mathlib and saw it split into two cases, so at that point I knew if I did cases on n then docs#fin.coe_coe_eq_self should apply to one case, and the other case might also be doable with simp.

[Hanting Zhang]

I see. Thanks for the explanation.

[Hanting Zhang]

Seeing your lemma, I tried to also do lemma zmod.coe_nat_coe_eq_self {n : ℕ} (a : zmod n) : ((a.val : ℕ) : zmod n) = a := by sorry, but this somehow does work?

[Hanting Zhang]

I think it's because Z is a ring, which might play better with zmod. This lemma doesn't really matter... but it would be nice to try to understand what's happening here.

[Adam Topaz]

This is a good exercise! But if you want to use it for something else, I suggest simply using docs#zmod.int_cast_surjective

[Adam Topaz]

The API for this stuff is somewhat extensive. You can find it in data.zmod.basic

[Alex J. Best]

I think the documentation of docs#zmod.cast is wrong in that it says you can cast to a semiring, but actually you need somewhere for -1 in zmod 0 to go with the current definition.

[Adam Topaz]

Should we make a natmod n :)