Skip to content

Commit

Permalink
refactor(sum_two_square): extract lemmas about primes in Z[i] (#1643)
Browse files Browse the repository at this point in the history 
* refactor(sum_two_square): extract lemmas about primes in Z[i]

* forgot to save

* docztring

* module docstrings
  • Loading branch information
@ChrisHughes24 @mergify
ChrisHughes24 authored and mergify[bot] committed Nov 5, 2019
1 parent f3f1fd8 commit 986e58c
Show file tree
Hide file tree
Showing 2 changed files with 119 additions and 52 deletions.
112 changes: 110 additions & 2 deletions src/data/zsqrtd/gaussian_int.lean
View file
Expand Up @@ -2,11 +2,37 @@
Copyright (c) 2019 Chris Hughes. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Chris Hughes
-/
import data.zsqrtd.basic data.complex.basic ring_theory.principal_ideal_domain
import data.zmod.quadratic_reciprocity
/-!
# Gaussian integers
The Gaussian integers are complex integer, complex numbers whose real and imaginary parts are both
integers.
## Main definitions
The Euclidean domain structure on `ℤ[i]` is defined in this file.
The homomorphism `to_complex` into the complex numbers is also defined in this file.
## Main statements
The gaussian integers ℤ[i].
`prime_iff_mod_four_eq_three_of_nat_prime`
A prime natural number is prime in `ℤ[i]` if and only if it is `3` mod `4`
## Notations
This file uses the local notation `ℤ[i]` for `gaussian_int`
## Implementation notes
Gaussian integers are implemented using the more general definition `zsqrtd`, the type of integers
adjoined a square root of `d`, in this case `-1`. The definition is reducible, so that properties
and definitions about `zsqrtd` can easily be used.
-/

import data.zsqrtd.basic data.complex.basic algebra.euclidean_domain
open zsqrtd complex

@[reducible] def gaussian_int : Type := zsqrtd (-1)
Expand Down Expand Up @@ -161,4 +187,86 @@ instance : euclidean_domain ℤ[i] :=
remainder_lt := nat_abs_norm_mod_lt,
mul_left_not_lt := λ a b hb0, not_lt_of_ge $ norm_le_norm_mul_left a hb0 }

open principal_ideal_domain

lemma mod_four_eq_three_of_nat_prime_of_prime {p : ℕ} (hp : p.prime) (hpi : prime (p : ℤ[i])) :
p % 4 = 3 :=
hp.eq_two_or_odd.elim
(λ hp2, absurd hpi (mt irreducible_iff_prime.2 $
λ ⟨hu, h⟩, begin
have := h ⟨1, 1⟩ ⟨1, -1⟩ (hp2.symm ▸ rfl),
rw [← norm_eq_one_iff, ← norm_eq_one_iff] at this,
exact absurd this dec_trivial
end))
(λ hp1, by_contradiction $ λ hp3 : p % 4 ≠ 3,
have hp41 : p % 4 = 1,
begin
rw [← nat.mod_mul_left_mod p 2 2, show 2 * 2 = 4, from rfl] at hp1,
have := nat.mod_lt p (show 0 < 4, from dec_trivial),
revert this hp3 hp1,
generalize hm : p % 4 = m, clear hm, revert m,
exact dec_trivial,
end,
let ⟨k, hk⟩ := (zmodp.exists_pow_two_eq_neg_one_iff_mod_four_ne_three hp).2 $
by rw hp41; exact dec_trivial in
have hpk : p ∣ k.val ^ 2 + 1,
by rw [← zmodp.eq_zero_iff_dvd_nat hp]; simp *,
have hkmul : (k.val ^ 2 + 1 : ℤ[i]) = ⟨k.val, 1⟩ * ⟨k.val, -1⟩ :=
by simp [_root_.pow_two, zsqrtd.ext],
have hpne1 : p ≠ 1, from (ne_of_lt (hp.one_lt)).symm,
have hkltp : 1 + k.val * k.val < p * p,
from calc 1 + k.val * k.val ≤ k.val + k.val * k.val :
add_le_add_right (nat.pos_of_ne_zero
(λ hk0, by clear_aux_decl; simp [*, nat.pow_succ] at *)) _
... = k.val * (k.val + 1) : by simp [mul_add]
... < p * p : mul_lt_mul k.2 k.2 (nat.succ_pos _) (nat.zero_le _),
have hpk₁ : ¬ (p : ℤ[i]) ∣ ⟨k.val, -1⟩ :=
λ ⟨x, hx⟩, lt_irrefl (p * x : ℤ[i]).norm.nat_abs $
calc (norm (p * x : ℤ[i])).nat_abs = (norm ⟨k.val, -1⟩).nat_abs : by rw hx
... < (norm (p : ℤ[i])).nat_abs : by simpa [norm] using hkltp
... ≤ (norm (p * x : ℤ[i])).nat_abs : norm_le_norm_mul_left _
(λ hx0, (show (-1 : ℤ) ≠ 0, from dec_trivial) $
by simpa [hx0] using congr_arg zsqrtd.im hx),
have hpk₂ : ¬ (p : ℤ[i]) ∣ ⟨k.val, 1⟩ :=
λ ⟨x, hx⟩, lt_irrefl (p * x : ℤ[i]).norm.nat_abs $
calc (norm (p * x : ℤ[i])).nat_abs = (norm ⟨k.val, 1⟩).nat_abs : by rw hx
... < (norm (p : ℤ[i])).nat_abs : by simpa [norm] using hkltp
... ≤ (norm (p * x : ℤ[i])).nat_abs : norm_le_norm_mul_left _
(λ hx0, (show (1 : ℤ) ≠ 0, from dec_trivial) $
by simpa [hx0] using congr_arg zsqrtd.im hx),
have hpu : ¬ is_unit (p : ℤ[i]), from mt norm_eq_one_iff.2 $
by rw [norm_nat_cast, int.nat_abs_mul, nat.mul_eq_one_iff];
exact λ h, (ne_of_lt hp.one_lt).symm h.1,
let ⟨y, hy⟩ := hpk in
by have := hpi.2.2 ⟨k.val, 1⟩ ⟨k.val, -1⟩
⟨y, by rw [← hkmul, ← nat.cast_mul p, ← hy]; simp⟩;
clear_aux_decl; tauto)

lemma sum_two_squares_of_nat_prime_of_not_irreducible {p : ℕ} (hp : p.prime)
(hpi : ¬irreducible (p : ℤ[i])) : ∃ a b, a^2 + b^2 = p :=
have hpu : ¬ is_unit (p : ℤ[i]), from mt norm_eq_one_iff.2 $
by rw [norm_nat_cast, int.nat_abs_mul, nat.mul_eq_one_iff];
exact λ h, (ne_of_lt hp.one_lt).symm h.1,
have hab : ∃ a b, (p : ℤ[i]) = a * b ∧ ¬ is_unit a ∧ ¬ is_unit b,
by simpa [irreducible, hpu, classical.not_forall, not_or_distrib] using hpi,
let ⟨a, b, hpab, hau, hbu⟩ := hab in
have hnap : (norm a).nat_abs = p, from ((hp.mul_eq_prime_pow_two_iff
(mt norm_eq_one_iff.1 hau) (mt norm_eq_one_iff.1 hbu)).1 $
by rw [← int.coe_nat_inj', int.coe_nat_pow, _root_.pow_two,
← @norm_nat_cast (-1), hpab];
simp).1,
⟨a.re.nat_abs, a.im.nat_abs, by simpa [nat_abs_norm_eq, nat.pow_two] using hnap⟩

lemma prime_of_nat_prime_of_mod_four_eq_three {p : ℕ} (hp : p.prime) (hp3 : p % 4 = 3) :
prime (p : ℤ[i]) :=
irreducible_iff_prime.1 $ classical.by_contradiction $ λ hpi,
let ⟨a, b, hab⟩ := sum_two_squares_of_nat_prime_of_not_irreducible hp hpi in
have ∀ a b : zmod 4, a^2 + b^2 ≠ p, by erw [← zmod.cast_mod_nat 4 p, hp3]; exact dec_trivial,
this a b (hab ▸ by simp)

/-- A prime natural number is prime in `ℤ[i]` if and only if it is `3` mod `4` -/
lemma prime_iff_mod_four_eq_three_of_nat_prime {p : ℕ} (hp : p.prime) :
prime (p : ℤ[i]) ↔ p % 4 = 3 :=
⟨mod_four_eq_three_of_nat_prime_of_prime hp, prime_of_nat_prime_of_mod_four_eq_three hp⟩

end gaussian_int
59 changes: 9 additions & 50 deletions src/number_theory/sum_two_squares.lean
View file
Expand Up @@ -2,67 +2,26 @@
Copyright (c) 2019 Chris Hughes. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Chris Hughes
-/
import data.zsqrtd.gaussian_int
/-!
# Sums of two squares
Proof of Fermat's theorem on the sum of two squares. Every prime congruent to 1 mod 4 is the sum
of two squares
-/

import data.zsqrtd.gaussian_int data.zmod.quadratic_reciprocity ring_theory.principal_ideal_domain

open gaussian_int principal_ideal_domain zsqrtd

local notation `ℤ[i]` := gaussian_int
open gaussian_int principal_ideal_domain

namespace nat
namespace prime

/-- Fermat's theorem on the sum of two squares. Every prime congruent to 1 mod 4 is the sum
of two squares -/
lemma sum_two_squares {p : ℕ} (hp : p.prime) (hp1 : p % 4 = 1) :
∃ a b : ℕ, a ^ 2 + b ^ 2 = p :=
let ⟨k, hk⟩ := (zmodp.exists_pow_two_eq_neg_one_iff_mod_four_ne_three hp).2 $
by rw hp1; exact dec_trivial in
have hpk : p ∣ k.val ^ 2 + 1,
by rw [← zmodp.eq_zero_iff_dvd_nat hp]; simp *,
have hkmul : (k.val ^ 2 + 1 : ℤ[i]) = ⟨k.val, 1⟩ * ⟨k.val, -1⟩ :=
by simp [_root_.pow_two, zsqrtd.ext],
have hpne1 : p ≠ 1, from (ne_of_lt (hp.one_lt)).symm,
have hkltp : 1 + k.val * k.val < p * p,
from calc 1 + k.val * k.val ≤ k.val + k.val * k.val :
add_le_add_right (nat.pos_of_ne_zero
(λ hk0, by clear_aux_decl; simp [*, nat.pow_succ] at *)) _
... = k.val * (k.val + 1) : by simp [mul_add]
... < p * p : mul_lt_mul k.2 k.2 (nat.succ_pos _) (nat.zero_le _),
have hpk₁ : ¬ (p : ℤ[i]) ∣ ⟨k.val, -1⟩ :=
λ ⟨x, hx⟩, lt_irrefl (p * x : ℤ[i]).norm.nat_abs $
calc (norm (p * x : ℤ[i])).nat_abs = (norm ⟨k.val, -1⟩).nat_abs : by rw hx
... < (norm (p : ℤ[i])).nat_abs : by simpa [norm] using hkltp
... ≤ (norm (p * x : ℤ[i])).nat_abs : norm_le_norm_mul_left _
(λ hx0, (show (-1 : ℤ) ≠ 0, from dec_trivial) $
by simpa [hx0] using congr_arg zsqrtd.im hx),
have hpk₂ : ¬ (p : ℤ[i]) ∣ ⟨k.val, 1⟩ :=
λ ⟨x, hx⟩, lt_irrefl (p * x : ℤ[i]).norm.nat_abs $
calc (norm (p * x : ℤ[i])).nat_abs = (norm ⟨k.val, 1⟩).nat_abs : by rw hx
... < (norm (p : ℤ[i])).nat_abs : by simpa [norm] using hkltp
... ≤ (norm (p * x : ℤ[i])).nat_abs : norm_le_norm_mul_left _
(λ hx0, (show (1 : ℤ) ≠ 0, from dec_trivial) $
by simpa [hx0] using congr_arg zsqrtd.im hx),
have hpu : ¬ is_unit (p : ℤ[i]), from mt norm_eq_one_iff.2 $
by rw [norm_nat_cast, int.nat_abs_mul, nat.mul_eq_one_iff];
exact λ h, (ne_of_lt hp.one_lt).symm h.1,
let ⟨y, hy⟩ := hpk in
have hpi : ¬ irreducible (p : ℤ[i]),
from mt irreducible_iff_prime.1
(λ hp, by have := hp.2.2 ⟨k.val, 1⟩ ⟨k.val, -1⟩
⟨y, by rw [← hkmul, ← nat.cast_mul p, ← hy]; simp⟩;
clear_aux_decl; tauto),
have hab : ∃ a b, (p : ℤ[i]) = a * b ∧ ¬ is_unit a ∧ ¬ is_unit b,
by simpa [irreducible, hpu, classical.not_forall, not_or_distrib] using hpi,
let ⟨a, b, hpab, hau, hbu⟩ := hab in
have hnap : (norm a).nat_abs = p, from ((hp.mul_eq_prime_pow_two_iff
(mt norm_eq_one_iff.1 hau) (mt norm_eq_one_iff.1 hbu)).1 $
by rw [← int.coe_nat_inj', int.coe_nat_pow, _root_.pow_two,
← @norm_nat_cast (-1), hpab];
simp).1,
⟨a.re.nat_abs, a.im.nat_abs, by simpa [nat_abs_norm_eq, pow_two] using hnap⟩
sum_two_squares_of_nat_prime_of_not_irreducible hp
(by rw [irreducible_iff_prime, prime_iff_mod_four_eq_three_of_nat_prime hp, hp1]; norm_num)

end prime
end nat

0 comments on commit 986e58c

Please sign in to comment.