Zulip Chat Archive

Stream: new members

Topic: Surjection from Z into zmod


view this post on Zulip Hanting Zhang (Jan 03 2021 at 03:07):

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?

view this post on Zulip Eric Wieser (Jan 03 2021 at 03:12):

Does ext help?

view this post on Zulip Eric Wieser (Jan 03 2021 at 03:12):

(deleted)

view this post on Zulip Hanting Zhang (Jan 03 2021 at 03:19):

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.

view this post on Zulip Hanting Zhang (Jan 03 2021 at 03:20):

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

view this post on Zulip Alex J. Best (Jan 03 2021 at 03:26):

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

view this post on Zulip Alex J. Best (Jan 03 2021 at 03:27):

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.

view this post on Zulip Alex J. Best (Jan 03 2021 at 03:29):

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

view this post on Zulip Alex J. Best (Jan 03 2021 at 03:37):

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.

view this post on Zulip Hanting Zhang (Jan 03 2021 at 03:41):

I see. Thanks for the explanation.

view this post on Zulip Hanting Zhang (Jan 03 2021 at 03:42):

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?

view this post on Zulip Hanting Zhang (Jan 03 2021 at 03:48):

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.

view this post on Zulip Adam Topaz (Jan 03 2021 at 03:52):

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

view this post on Zulip Adam Topaz (Jan 03 2021 at 03:54):

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

view this post on Zulip Alex J. Best (Jan 03 2021 at 03:54):

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.

view this post on Zulip Adam Topaz (Jan 03 2021 at 03:56):

Should we make a natmod n :)


Last updated: May 15 2021 at 02:11 UTC