equation in ℕ to equation in zmod n

Stream: Is there code for X?

[Stuart Presnell]

I feel like I'm missing something obvious here. If I'm trying to prove, for example,

example (n : ℕ) (x : zmod n) : x ^ 2 - 1 = (x + 1) * (x - 1) := sorry

and I have the corresponding statement that holds for all x : ℕ (in this case, nat.sq_sub_sq x 1), can I use the equation in ℕ to prove the equation in zmod n?

[Stuart Presnell]

I suspect the answer is either going to be "No, of course not, because ..." or "Of course, it's just ...". Either way, I have the :face_palm: ready!

[Mario Carneiro]

No, not really, but it is an equation in the language of rings and zmod n is a ring so by ring should work

[Mario Carneiro]

in fact this theorem is considreably harder over nat because - doesn't mean the usual thing

[Kevin Buzzard]

Yeah the canonical map (call it f) from nat to zmod n is surjective which is one of the ingredients you'd need for this, but it does not satisfy f(a-b) = f(a) - f(b) which would be another.

[Kevin Buzzard]

eg x-(x+1)=0 can be proved for nat but can't be deduced for zmod n

[Stuart Presnell]

Yes, I'd once again forgotten about the problem of subtraction.

[Damiano Testa]

For instance, when x=0 the statement over ℕ and over zmod n are both true but represent "different" identities.

[Stuart Presnell]

Yeah, I realise now that if I want to get a result for zmod n from something more generic, the natural generalisation is something like comm_ring R, not ℕ.

[Stuart Presnell]

And indeed the example I gave above has _root_.sq_sub_sq x 1 for x : R.

[Ruben Van de Velde]

How about from \Z?

[Kevin Buzzard]

Then it becomes the statement "evaluation of a polynomial commutes with ring homomorphisms" which presumably is there somewhere...

[Filippo A. E. Nuccio]

Is it this result? BTW: How can I paste docs links if there is a subscript? The usual way did not work...

[Eric Wieser]

You can't, we need to fix the Zulip linkifiers (if they can be fixed)

[Stuart Presnell]

Related to my previous question, do we have this?

example {p α : ℕ} (hα0 : 0 < α) (pp : p.prime) (hp_odd : odd p) {x : zmod (p^α)}
  (root : x^2 = 1) :
  x = 1 ∨ x = -1 := sorry

[Stuart Presnell]

The proof for x : zmod p is more straightforward, because we have [no_zero_divisors (zmod p)]`.

[Stuart Presnell]

And I can prove this (without any issues with subtraction)

example {p α x : ℕ} (pp : p.prime) (hp_odd : odd p) (root : p^α ∣ x^2 - 1) :
  (p^α ∣ x - 1) ∨ (p^α ∣ x + 1) := sorry

but I can't see how to use this to get a proof of the above.

[Eric Wieser]

No need for hα0 : 0 < α, it's true for α = 0

[Kevin Buzzard]

Why not x : int instead of x : nat for the intermediate result?

[Kevin Buzzard]

Then the result would be easier to use.

[Stuart Presnell]

I've started an attempt on that, but I've run into difficulties proving it and other difficulties in using it for the zmod (p^α) result — I get tangled up in coercions.

[Stuart Presnell]

The outline of the proof for x : nat is:

example {p α x : ℕ} (pp : p.prime) (hp_odd : odd p) (root : p^α ∣ x^2 - 1) :
  (p^α ∣ x - 1) ∨ (p^α ∣ x + 1) :=
begin
  have h1 : p^α ∣ (x + 1) * (x - 1), { rw ←nat.sq_sub_sq, simpa },
  have h2 : ¬ p ∣ (x + 1) ∨ ¬ p ∣ (x - 1), { sorry },  -- because if p divides both then p ∣ 2
  cases h2 with h_plus h_minus,
  { left, sorry },
  { right, sorry },
end

where the last two sorrys are taken care of with docs#prime.pow_dvd_of_dvd_mul_left and docs#prime.pow_dvd_of_dvd_mul_right.

[Stuart Presnell]

But I can't see how to write the counterpart of ¬ p ∣ (x + 1) and ¬ p ∣ (x - 1) in the zmod (p^α) case.

[Notification Bot]

Stuart Presnell has marked this topic as unresolved.

[Stuart Presnell]

Sorry, I didn't check back into the thread after I marked it as resolved. Thanks @Kevin Buzzard for writing up a solution!

[Stuart Presnell]

Here's the version I figured out:

import data.nat.parity
import data.zmod.algebra
import ring_theory.int.basic

open nat zmod

/-- If an odd prime power `p^α` divides `x^2 - 1` then it divides `x-1` or `x+1`. -/
lemma square_roots_of_one_int {p α : ℕ} {x : ℤ} (pp : p.prime) (hp_odd : odd p)
  (root : ↑p^α ∣ x^2 - 1) :
  (↑p^α ∣ x - 1) ∨ (↑p^α ∣ x + 1) :=
begin
  have pp' := prime_iff_prime_int.1 pp,
  have diffsquare : ↑(p^α) ∣ (x-1) * (x+1), { ring_nf, simp [root] },
  have h2 : ¬ ↑p ∣ (x + 1) ∨ ¬ ↑p ∣ (x - 1),
  { rw ←not_and_distrib,
    rintro ⟨hp1, hp2⟩,
    have h3 : ↑p ∣ (x+1) - (x-1), { exact dvd_sub hp1 hp2 },
    have h4 : (x+1) - (x-1) = 2, { ring },
    rw h4 at h3,
    rw (show (2:ℤ) = 2*1^2, by linarith) at h3,
    have := prime_two_or_dvd_of_dvd_two_mul_pow_self_two pp h3,
    simp [pp.ne_one] at this,
    rw [this, odd_iff_not_even] at hp_odd,
    exact hp_odd even_two },
  cases h2 with h_plus h_minus,
  { left, apply prime.pow_dvd_of_dvd_mul_left pp' α h_plus, simpa [mul_comm] using diffsquare },
  { right, apply prime.pow_dvd_of_dvd_mul_right pp' α h_minus, simpa [mul_comm] using diffsquare },
end

/-- If `x : zmod (p^α)` (for odd prime `p`) satisfies `x^2 = 1` then `x = 1 ∨ x = -1` -/
lemma square_roots_of_one_zmod {p α : ℕ} (pp : p.prime) (hp_odd : odd p) {x : zmod (p^α)}
  (root : x^2 = 1) :
  x = 1 ∨ x = -1 :=
begin
  refine or.imp (λ h, _) (λ h, _) (@square_roots_of_one_int p α ↑x pp hp_odd _ ),
  { have := int_coe_eq_int_coe_iff_dvd_sub 1 (↑x) (↑p^α),
    simp at this,
    rwa [eq_comm, this] },
  { have := int_coe_eq_int_coe_iff_dvd_sub (-1) (↑x) (↑p^α),
    simp at this,
    rwa [eq_comm, this] },
  { have := int_coe_eq_int_coe_iff_dvd_sub 1 (↑x^2) (↑p^α),
    simp at this,
    rw [←this, root] },
end

[Stuart Presnell]

Of course I was cheating in the latter proof by leaving the simps unsqueezed. Here's a better version with tem changed to {norm,push}_cast

import data.nat.parity
import data.zmod.algebra
import ring_theory.int.basic

open nat zmod

/-- If `x : zmod (p^α)` (for odd prime `p`) satisfies `x^2 = 1` then `x = 1 ∨ x = -1` -/
lemma square_roots_of_one_zmod {p α : ℕ} (pp : p.prime) (hp_odd : odd p) {x : zmod (p^α)}
  (root : x^2 = 1) :
  x = 1 ∨ x = -1 :=
begin
  refine or.imp (λ h, _) (λ h, _) (@square_roots_of_one_int p α ↑x pp hp_odd _ ),
  { have := int_coe_eq_int_coe_iff_dvd_sub 1 (↑x) (↑p^α),
    norm_cast at this,
    rwa [eq_comm, this, nat.cast_pow] },
  { have := int_coe_eq_int_coe_iff_dvd_sub (-1) (↑x) (↑p^α),
    push_cast at this,
    rw [eq_comm, this],
    simpa using h },
  { have := int_coe_eq_int_coe_iff_dvd_sub 1 (↑x^2) (↑p^α),
    push_cast at this,
    rw [←this, root] },
end