## Stream: new members

### Topic: Proving that 0 = 0 in zmod

#### Marc Masdeu (Aug 26 2020 at 13:55):

I am having trouble with this simple lemma.

lemma zero_eq_zero {n : ℕ} [0 < n] {x : zmod n} (h : (x : ℤ) = 0) : x = 0 :=
begin
sorry
end


In fact, I have been able to prove this, which I thought would already be in mathlib:

variables {n : ℕ}  [fact (0 < n)]

lemma zero_iff_n_divides (x : zmod n) : x = 0 ↔ n  ∣ x.val :=
begin
split,
{
intro h,
finish,
},
{
intro h,
cases h with w hw,
suffices : w = 0, by finish,
have H : x.val < n := @@zmod.val_lt _inst_1 x,
rw hw at H,
suffices : w < 1, by linarith,
exact (mul_lt_iff_lt_one_right _inst_1).mp H,
}
end


and I can't seem to prove the analogous one for integers:

variables {n : ℕ}  [fact (0 < n)]

lemma zero_iff_n_divides' (x : zmod n) : x = 0 ↔ (n : ℤ) ∣ (x : ℤ):=
begin
split,
{
intro h,
finish,
},
{
intro h,
cases h with w hw,
suffices : w = 0,
{
have hw0 : (x : ℤ) = 0, by nlinarith,
exact zero_eq_zero hw0,
},
sorry
}
end


Incidentally, I don't see with the typeclass inference system doesn't work in this case (hence the two occurrences of _inst_1 in the proof). Is there something that I am overlooking?

Thank you!

#### Kevin Buzzard (Aug 26 2020 at 13:57):

Can you post a #mwe? You're missing one or more of imports, variables, opens, universes

#### Kevin Buzzard (Aug 26 2020 at 13:58):

< is not a class, so [0 < n] won't work. Inputs to functions in [square brackets] are supposed to be filled in by the type class inference system, and the type class inference system only deals with classes, so it won't deal with <.

#### Kevin Buzzard (Aug 26 2020 at 14:00):

I feel like some people might think I'm just nagging when I ask for MWE's, but I genuinely don't know what to import to get zmod and I'm too lazy to find out.

#### Marc Masdeu (Aug 26 2020 at 14:00):

That compiles in my system.

import data.zmod.basic
import tactic

open_locale classical
noncomputable theory

variables {n : ℕ}  [fact (0 < n)]

lemma zero_eq_zero  {x : zmod n} (h : (x : ℤ) = 0) : x = 0 :=
begin
sorry
end


#### Marc Masdeu (Aug 26 2020 at 14:01):

Kevin Buzzard said:

I feel like some people might think I'm just nagging when I ask for MWE's, but I genuinely don't know what to import to get zmod and I'm too lazy to find out.

I am not one of those people.

#### Kevin Buzzard (Aug 26 2020 at 14:01):

You're using a coercion from zmod n to Z? Eew. I am surprised there is even a coercion :-)

#### Marc Masdeu (Aug 26 2020 at 14:03):

Well somewhere in Zulip I saw that it's best to work with int than with nat whenever possible.

#### Kevin Buzzard (Aug 26 2020 at 14:03):

h: ↑x = 0
⊢ x = 0


I don't know what the definition of that arrow is yet

#### Kenny Lau (Aug 26 2020 at 14:04):

Marc Masdeu said:

Well somewhere in Zulip I saw that it's best to work with int than with nat whenever possible.

that surely highly depends on context

#### Kenny Lau (Aug 26 2020 at 14:04):

I say that if you're in zmod you shouldn't coerce to int

or to nat

#### Kevin Buzzard (Aug 26 2020 at 14:04):

If you plan to do subtractions you shouldn't be using nat because it doesn't have a subtraction (it's a semiring, not a ring)

#### Patrick Massot (Aug 26 2020 at 14:05):

Kevin Buzzard said:

h: ↑x = 0
⊢ x = 0


I don't know what the definition of that arrow is yet

Kevin, we longer have this issue since Ed offered us magic widgets.

#### Patrick Massot (Aug 26 2020 at 14:05):

Just click on the arrow.

#### Marc Masdeu (Aug 26 2020 at 14:05):

What I want is an easy way to go from x=y (in zmod n) to n dividing x'-y', where x' and y' are lifts to integers. So here is where subtraction appears.

#### Kenny Lau (Aug 26 2020 at 14:05):

when we say "lift", we choose x' first

#### Kevin Buzzard (Aug 26 2020 at 14:06):

what are x' and y'? Are they arbitrary? Is this a theorem about x and y, or about x' and y'?

#### Kenny Lau (Aug 26 2020 at 14:06):

i.e. rather than using the standard lift that isn't canonical, instead let the integer be the variable

#### Kenny Lau (Aug 26 2020 at 14:06):

so the "correct" theorem should say that for x y : Z, (x : zmod n) = y <-> n | (x - y)

uparrow2.png

#### Kenny Lau (Aug 26 2020 at 14:06):

coercing from int to zmod is good; from zmod to int is bad

#### Kevin Buzzard (Aug 26 2020 at 14:06):

@Patrick Massot I said I didn't know the definition precisely because this trick told me nothing

#### Kevin Buzzard (Aug 26 2020 at 14:07):

#check (by apply_instance : has_lift (zmod n) ℤ)
/-
tactic.mk_instance failed to generate instance for
has_lift (zmod n) ℤ
-/


#### Kevin Buzzard (Aug 26 2020 at 14:07):

I've never understood the zoo of lifts and coercions properly

#### Patrick Massot (Aug 26 2020 at 14:07):

The trick tells you this is coercion from zmod n to int, that's infinitely more information than what you would have had before widgets.

#### Kevin Buzzard (Aug 26 2020 at 14:08):

#check (by apply_instance : has_coe (zmod n) ℤ)
/-
tactic.mk_instance failed to generate instance for
has_coe (zmod n) ℤ
-/


#### Kevin Buzzard (Aug 26 2020 at 14:08):

Patrick Massot said:

The trick tells you this is coercion from zmod n to int, that's infinitely more information than what you would have had before widgets.

I already knew that from the lemma statement lemma zero_eq_zero {x : zmod n} (h : (x : ℤ) = 0) : x = 0 :=

#### Kevin Buzzard (Aug 26 2020 at 14:08):

I genuinely don't know how to work out what the map is

#### Kevin Buzzard (Aug 26 2020 at 14:10):

oh -- I keep going with the widgets!

#### Kenny Lau (Aug 26 2020 at 14:11):

what is that cursed instance

#### Kevin Buzzard (Aug 26 2020 at 14:12):

/-- Cast an integer modulo n to another semiring.
This function is a morphism if the characteristic of R divides n.
See zmod.cast_hom for a bundled version. -/
def cast : Π {n : ℕ}, zmod n → R
| 0     := int.cast
| (n+1) := λ i, i.val

-- see Note [coercion into rings]
@[priority 900] instance (n : ℕ) : has_coe_t (zmod n) R := ⟨cast⟩

@[simp] lemma cast_zero : ((0 : zmod n) : R) = 0 :=
by { cases n; refl }


#### Kevin Buzzard (Aug 26 2020 at 14:14):

This coercion has no good ring-theoretic properties. @Rob Lewis the Teichmuller lift is at least a homomorphism of monoids with zero :-)

#### Marc Masdeu (Aug 26 2020 at 14:14):

OK I'll try to explain myself a bit better. I was trying to prove

variables {p r n m: ℕ} [fact p.prime] [fact (0 < n)] [fact (0 < m)] [1 ≤ r]

lemma basic_lemma (x : zmod (p^r)) (h : x * x = 1) : (x : zmod p) = 1 ∨ (x : zmod p) = -1 :=
begin
sorry
end


This is a statement about elements all in zmod (either p or p^r). It seems that it should be very easy, but I got this so far:

lemma basic_lemma (x : zmod (p^r)) (h : x * x = 1) : (x : zmod p) = 1 ∨ (x : zmod p) = -1 :=
begin
have hp : nat.prime p, by assumption,
have  h1 : (p : ℤ)^r ∣ ((x.val : ℤ) * (x.val : ℤ) - 1),
{
have h' :  x * x -1 = 0 := sub_eq_zero.mpr h,
--rw_mod_cast zmod.int_coe_zmod_eq_zero_iff_dvd at h',
sorry
},
have h2 : (p : ℤ) ∣ ((x.val : ℤ) * (x.val : ℤ) - 1),
{
cases h1 with w h1w,
rw h1w,
ring,
fconstructor,
use (p^(r-1)) * w,
rw ← int.mul_assoc,
have hp : (p : ℤ)^r = p * p^(r-1),
{
induction r with d hd,
{
linarith,
},
{
ring,
ring,
}
},
rw ←hp,
rw int.mul_comm,
},
have h3 : (p : ℤ) ∣ ((x.val : ℤ) - 1) ∨ (p : ℤ) ∣ (x.val : ℤ) + 1,
{
have hfac : (x.val : ℤ) * (x.val : ℤ) - 1
= ((x.val:ℤ) - 1) * ((x.val:ℤ) + 1) := by ring,
rw hfac at h2,
apply int.prime.dvd_mul' hp h2,
},
cases h3 with h3l h3r,
{
left,
suffices : (x : zmod p) - 1 = 0, by exact sub_eq_zero.mp this,
rw← zmod.int_coe_zmod_eq_zero_iff_dvd (((x.val):ℤ)-1) p at h3l,
push_cast at *,
rw @@x_val_trans _inst_1 _inst_4 at h3l,
exact h3l,
},
{
right,
suffices : (x : zmod p) + 1 = 0, by exact eq_neg_of_add_eq_zero this,
rw← zmod.int_coe_zmod_eq_zero_iff_dvd (((x.val):ℤ) + 1) p at h3r,
push_cast at *,
rw @@x_val_trans _inst_1 _inst_4 at h3r,
exact h3r,
}
end


So I find myself trying to prove

↑p ^ r ∣ ↑(x.val) * ↑(x.val) - 1


in the realm of int...

#### Kevin Buzzard (Aug 26 2020 at 14:16):

To prove the basic lemma, let xbar be x mod p and deduce that xbar^2=1 and then you're done because zmod p is a field, right?

#### Marc Masdeu (Aug 26 2020 at 14:17):

This was my math proof, but I had a bit more trouble writing it in Lean!

#### Kenny Lau (Aug 26 2020 at 14:17):

@Kevin Buzzard right, so the problem is how to coerce from zmod (p^r) to zmod p

#### Kenny Lau (Aug 26 2020 at 14:17):

now that cursed instance seems like a good candidate

#### Kenny Lau (Aug 26 2020 at 14:18):

because zmod p does have characteristic dividing p^r

#### Marc Masdeu (Aug 26 2020 at 14:18):

But @Kenny Lau this coercion should be simple, right?

#### Kenny Lau (Aug 26 2020 at 14:18):

so maybe zmod.cast_hom would help

#### Kevin Buzzard (Aug 26 2020 at 14:20):

In the situation where the coercion is ring-theoretically reasonable one should use the ring-theoretic coercion I guess

#### Kenny Lau (Aug 26 2020 at 14:20):

I feel like this is still #xy

#### Kenny Lau (Aug 26 2020 at 14:21):

the "basic lemma" has a coercion from zmod (p^r) to zmod p

#### Kenny Lau (Aug 26 2020 at 14:21):

what demanded this coercion to start with?

#### Kevin Buzzard (Aug 26 2020 at 14:21):

There is no API for it and it's a horrible function, so it's horrible to use.

#### Marc Masdeu (Aug 26 2020 at 14:22):

OK the feeling I had throughout is that zmod's API is not quite working yet. It is very hard to work with it, since it has references to %, to MOD, ...

#### Marc Masdeu (Aug 26 2020 at 14:25):

Kenny Lau said:

I feel like this is still #xy

You got me. I want to prove that in Z/p^r (p odd) the only solutions to x^2-1=0 are 1 and -1. The way I can prove this is to lift x to x'=+-1 + e, with e being a multiple of p (hence the basic lemma). Then I prove that p^r divides e, here is where I use that p is odd.

#### Kevin Buzzard (Aug 26 2020 at 14:26):

right, that looks like the standard proof.

#### Marc Masdeu (Aug 26 2020 at 14:30):

I might start from scratch...

#### Kevin Buzzard (Aug 26 2020 at 14:39):

rofl cast uses nat.cast_coe because it's coercing to a general ring, as opposed to the standard coercion from nat to int.

#### Kevin Buzzard (Aug 26 2020 at 14:40):

so the issue is to prove that nat.cast_coe is injective when going from nat to int.

#### Kevin Buzzard (Aug 26 2020 at 14:49):

import data.zmod.basic
import tactic

open_locale classical
noncomputable theory

variables {n : ℕ} [fact (0 < n)]

lemma zero_eq_zero  {x : zmod n} (h : (x : ℤ) = 0) : x = 0 :=
begin
-- this workaround is because you're using fact
tactic.unfreeze_local_instances,
-- deal with n = 0 case
cases n with d, cases _inst_1,
-- now n = d + 1
-- now take x apart
cases x with a ha,
-- now a is a natural
ext, dsimp,
-- and it suffices to prove a = 0,
unfold_coes at h,
-- zmod.cast has no API because nobody uses it
rw zmod.cast.equations._eqn_2 at h,
-- We know the usual map ℕ → ℤ is injective
rw ←int.coe_nat_eq_zero,
-- so we would be done by h
convert h,
-- except we now have to prove that the two coercions ℕ → ℤ are equal.
apply congr_arg has_coe_t.mk,
ext n,
-- we prove it by induction
induction n with d hd,
{ refl },
{ unfold nat.cast,
rw ←hd,
refl }
end


You're really fighting the system here because the casts don't have too much API

#### Johan Commelin (Aug 26 2020 at 14:53):

My apologies for the awful coercion. I don't know how to improve it.

#### Marc Masdeu (Aug 26 2020 at 14:53):

Wow! That is incredibly hard!! Thanks @Kevin Buzzard, this is the kind of thing that throw some people off...

#### Kevin Buzzard (Aug 26 2020 at 14:53):

Because it's so general it's hard to find lemmas about it.

#### Kevin Buzzard (Aug 26 2020 at 14:54):

What's going on here Marc is that there is a map from Z/nZ to any ring given by literally sending 0,1,2,...,n-1 to 0,1,2,...,n-1. There aren't really any lemmas you can prove about it.

#### Kevin Buzzard (Aug 26 2020 at 14:54):

However, for a given ring like the integers, there are lemmas you can prove (for example injectivity)

#### Kevin Buzzard (Aug 26 2020 at 14:55):

but these lemmas are not proved, as far as I can see.

#### Kevin Buzzard (Aug 26 2020 at 14:55):

because probably there are a million such lemmas. We know that "if x is in Z/nZ then lift x to Z" is a reasonable thing to do

#### Kevin Buzzard (Aug 26 2020 at 14:56):

but "if x is in Z/nZ then randomly map it to Z/mZ" is perhaps not so common

#### Marc Masdeu (Aug 26 2020 at 14:56):

I see. Yes, the general map is a bit dumb, but it's very common as you know in arithmetic to lift elements in Z/n to Z and then prove things about those lifts, so it'd be useful to have some lemmas about this.

#### Kevin Buzzard (Aug 26 2020 at 14:57):

It might be interesting @Johan Commelin to see how many times in the library this map is used when the target ring is not nat or int. If people are only using it to lift from Z/n to Z (this is Marc's use case and also yours in the PR) then perhaps it's worth restricting to that case and then writing the API which Marc needed here.

#### Marc Masdeu (Aug 26 2020 at 14:57):

Maybe it'd be best to do as in mathlib, start with integers and prove things about their images in various zmods

#### Kevin Buzzard (Aug 26 2020 at 14:58):

right, that's another way of thinking about it.

#### Kevin Buzzard (Aug 26 2020 at 14:58):

There is congruence mod n in mathlib, and it's an equivalence relation on integers

#### Kevin Buzzard (Aug 26 2020 at 14:58):

and that has a whole file of API, a very solid one.

#### Marc Masdeu (Aug 26 2020 at 14:59):

Yes, I will want to work with the ring (and its units) zmod n, so I'd rather not think in terms of equivalence relations...

#### Kevin Buzzard (Aug 26 2020 at 14:59):

I feel like lifting from Z/p^n to Z/p^(n+1) is still a useful thing though

#### Marc Masdeu (Aug 26 2020 at 14:59):

Ideally, it would be easy to go back and forth between all these objects.

#### Kevin Buzzard (Aug 26 2020 at 15:00):

but I would be strongly tempted here not to use the cast. It is easy to go back and forth between these objects, because you can do it directly without using the coercion.

I'll try...

#### Kevin Buzzard (Aug 26 2020 at 15:01):

If n>0 then a term of type zmod n is just a pair (a,h) with a a natural and h a proof that it's less than n. So you can just use (a,h') to move from Z/n to Z/(pn) where h' is a proof that a<pn manufactured from the proof that it's less than n

#### Kevin Buzzard (Aug 26 2020 at 15:02):

It would be very easy to prove things about that map because it's defined concretely on the level of integers without using nat.cast or zmod.cast

#### Kevin Buzzard (Aug 26 2020 at 15:10):

I can't find x^2=1 -> x=+-1 in a field

#### Bryan Gin-ge Chen (Aug 26 2020 at 15:13):

There's docs#mul_self_eq_one_iff

#### Kevin Buzzard (Aug 26 2020 at 15:16):

import data.zmod.basic
import tactic

open_locale classical
noncomputable theory

#check zmod.cast_hom

variables {p r n m: ℕ} (hp : p.prime) (hn : 0 < n) (hm : 0 < m) (hr : 0 < r)

lemma div_pow (p : ℕ) {r : ℕ} (hr : 0 < r) : p ∣ p^r :=
begin
-- do a case split on r=0 or r=s+1
cases r with s,
{ -- r=0 can't happen
cases hr },
{ -- r = s + 1 so we can use nat.pow_succ
rw nat.pow_succ,
-- library_search found the next line
apply dvd_mul_left,
}
end

include hp hn hm hr

lemma basic_lemma (x : zmod (p^r)) (h : x * x = 1) :
(x : zmod p) = 1 ∨ (x : zmod p) = -1 :=
begin
let f := zmod.cast_hom (div_pow p hr) (zmod p), -- the ring hom
set xp := f x with hxp,
have hxpsquared : xp * xp = 1,
{ rw hxp,
rw ←f.map_mul,
rw h,
exact f.map_one,
},
haveI : fact p.prime := hp,
convert mul_self_eq_one_iff.1 hxpsquared,
end


#### Johan Commelin (Aug 26 2020 at 15:52):

Note that mathlib knows that coe : int → zmod n is surjective. In fact it knows that arbitrary ring homs to zmod n are surjective.

#### Johan Commelin (Aug 26 2020 at 15:52):

I guess that might be helpful...

#### Johan Commelin (Aug 26 2020 at 15:52):

But I haven't thought about the details of what's going on here.

#### Mario Carneiro (Aug 26 2020 at 17:30):

import data.zmod.basic

theorem cast_inj : ∀ {i}, function.injective (coe : zmod i → int)
| 0 := λ a b, by simp
| (n+1) := λ a b h, fin.val_injective (nat.cast_inj.1 h)

lemma zero_eq_zero {n} {x : zmod n} (h : (x : ℤ) = 0) : x = 0 :=
cast_inj (h.trans \$ by simp)


#### Kevin Buzzard (Aug 26 2020 at 17:31):

Right! And now if we want to prove it for rationals, you have to prove a whole new cast_inj :-(

#### Mario Carneiro (Aug 26 2020 at 17:32):

I tried to generalize it but char_p wasn't built to handle this

#### Mario Carneiro (Aug 26 2020 at 17:32):

I don't know how to say "R is a ring with the first n elements distinct"

#### Mario Carneiro (Aug 26 2020 at 17:34):

Anyway this proof doesn't really generalize because the zero case uses int.cast_id

#### Mario Carneiro (Aug 26 2020 at 17:34):

so a different ring would actually be substantively different

#### Marc Masdeu (Aug 26 2020 at 18:25):

Thanks for the discussion. I am slowly understanding how this is working...

Last updated: May 15 2021 at 22:14 UTC