From 391746b1c7c5b3459a5f987d7d1d76093a669015 Mon Sep 17 00:00:00 2001
From: Chris Hughes <chrishughes24@gmail.com>
Date: Tue, 27 Jul 2021 08:42:11 +0000
Subject: [PATCH] feat(data/zmod/basic): chinese remainder theorem (#8356)

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
---
 src/algebra/char_p/basic.lean | 18 +++++++++++
 src/algebra/ring/prod.lean    | 20 ++++++++++++
 src/data/fintype/basic.lean   | 14 +++++++++
 src/data/int/cast.lean        | 13 ++++++++
 src/data/nat/cast.lean        | 13 ++++++++
 src/data/nat/gcd.lean         | 10 ++++++
 src/data/zmod/basic.lean      | 58 ++++++++++++++++++++++++++++++++++-
 7 files changed, 145 insertions(+), 1 deletion(-)

diff --git a/src/algebra/char_p/basic.lean b/src/algebra/char_p/basic.lean
index ee2355e8a8566..fc012e14d75fc 100644
--- a/src/algebra/char_p/basic.lean
+++ b/src/algebra/char_p/basic.lean
@@ -428,3 +428,21 @@ begin
 end
 
 end
+
+section prod
+
+variables (S : Type v) [semiring R] [semiring S] (p q : ℕ) [char_p R p]
+
+/-- The characteristic of the product of rings is the least common multiple of the
+characteristics of the two rings. -/
+instance [char_p S q] : char_p (R × S) (nat.lcm p q) :=
+{ cast_eq_zero_iff :=
+    by simp [prod.ext_iff, char_p.cast_eq_zero_iff R p,
+      char_p.cast_eq_zero_iff S q, nat.lcm_dvd_iff] }
+
+/-- The characteristic of the product of two rings of the same characteristic
+  is the same as the characteristic of the rings -/
+instance prod.char_p [char_p S p] : char_p (R × S) p :=
+by convert nat.lcm.char_p R S p p; simp
+
+end prod
diff --git a/src/algebra/ring/prod.lean b/src/algebra/ring/prod.lean
index 100b618e55be5..4829806640b10 100644
--- a/src/algebra/ring/prod.lean
+++ b/src/algebra/ring/prod.lean
@@ -141,4 +141,24 @@ ring_hom.ext $ λ _, rfl
   (ring_hom.snd S R).comp ↑(prod_comm : R × S ≃+* S × R) = ring_hom.fst R S :=
 ring_hom.ext $ λ _, rfl
 
+variables (R S) [subsingleton S]
+
+/-- A ring `R` is isomorphic to `R × S` when `S` is the zero ring -/
+@[simps] def prod_zero_ring : R ≃+* R × S :=
+{ to_fun := λ x, (x, 0),
+  inv_fun := prod.fst,
+  map_add' := by simp,
+  map_mul' := by simp,
+  left_inv := λ x, rfl,
+  right_inv := λ x, by cases x; simp }
+
+/-- A ring `R` is isomorphic to `S × R` when `S` is the zero ring -/
+@[simps] def zero_ring_prod : R ≃+* S × R :=
+{ to_fun := λ x, (0, x),
+  inv_fun := prod.snd,
+  map_add' := by simp,
+  map_mul' := by simp,
+  left_inv := λ x, rfl,
+  right_inv := λ x, by cases x; simp }
+
 end ring_equiv
diff --git a/src/data/fintype/basic.lean b/src/data/fintype/basic.lean
index bd49f62a895cd..694ce5523d0f1 100644
--- a/src/data/fintype/basic.lean
+++ b/src/data/fintype/basic.lean
@@ -980,6 +980,20 @@ begin
     rwa injective_iff_surjective_of_equiv (equiv_of_card_eq h) }
 end
 
+lemma right_inverse_of_left_inverse_of_card_le {f : α → β} {g : β → α}
+  (hfg : left_inverse f g) (hcard : card α ≤ card β) :
+  right_inverse f g :=
+have hsurj : surjective f, from surjective_iff_has_right_inverse.2 ⟨g, hfg⟩,
+right_inverse_of_injective_of_left_inverse
+  ((bijective_iff_surjective_and_card _).2
+    ⟨hsurj, le_antisymm hcard (card_le_of_surjective f hsurj)⟩ ).1
+  hfg
+
+lemma left_inverse_of_right_inverse_of_card_le {f : α → β} {g : β → α}
+  (hfg : right_inverse f g) (hcard : card β ≤ card α) :
+  left_inverse f g :=
+right_inverse_of_left_inverse_of_card_le hfg hcard
+
 end fintype
 
 lemma fintype.coe_image_univ [fintype α] [decidable_eq β] {f : α → β} :
diff --git a/src/data/int/cast.lean b/src/data/int/cast.lean
index 074add924bb87..bd7dee2ef7aab 100644
--- a/src/data/int/cast.lean
+++ b/src/data/int/cast.lean
@@ -202,6 +202,19 @@ end cast
 
 end int
 
+namespace prod
+
+variables {α : Type*} {β : Type*} [has_zero α] [has_one α] [has_add α] [has_neg α]
+  [has_zero β] [has_one β] [has_add β] [has_neg β]
+
+@[simp] lemma fst_int_cast (n : ℤ) : (n : α × β).fst = n :=
+by induction n; simp *
+
+@[simp] lemma snd_int_cast (n : ℤ) : (n : α × β).snd = n :=
+by induction n; simp *
+
+end prod
+
 open int
 
 namespace add_monoid_hom
diff --git a/src/data/nat/cast.lean b/src/data/nat/cast.lean
index 23af44230e9ab..4bec2a4e1a25d 100644
--- a/src/data/nat/cast.lean
+++ b/src/data/nat/cast.lean
@@ -239,6 +239,19 @@ end linear_ordered_field
 
 end nat
 
+namespace prod
+
+variables {α : Type*} {β : Type*} [has_zero α] [has_one α] [has_add α]
+  [has_zero β] [has_one β] [has_add β]
+
+@[simp] lemma fst_nat_cast (n : ℕ) : (n : α × β).fst = n :=
+by induction n; simp *
+
+@[simp] lemma snd_nat_cast (n : ℕ) : (n : α × β).snd = n :=
+by induction n; simp *
+
+end prod
+
 namespace add_monoid_hom
 
 variables {A B : Type*} [add_monoid A]
diff --git a/src/data/nat/gcd.lean b/src/data/nat/gcd.lean
index 9e91ec89b1b5d..807839231aca2 100644
--- a/src/data/nat/gcd.lean
+++ b/src/data/nat/gcd.lean
@@ -191,6 +191,10 @@ or.elim (eq_zero_or_pos k)
     by rw [gcd_mul_lcm, ←gcd_mul_right, mul_comm n k];
        exact dvd_gcd (mul_dvd_mul_left _ H2) (mul_dvd_mul_right H1 _))
 
+lemma lcm_dvd_iff {m n k : ℕ} : lcm m n ∣ k ↔ m ∣ k ∧ n ∣ k :=
+⟨λ h, ⟨dvd_trans (dvd_lcm_left _ _) h, dvd_trans (dvd_lcm_right _ _) h⟩,
+  and_imp.2 lcm_dvd⟩
+
 theorem lcm_assoc (m n k : ℕ) : lcm (lcm m n) k = lcm m (lcm n k) :=
 dvd_antisymm
   (lcm_dvd
@@ -358,6 +362,12 @@ by simp [coprime]
 @[simp] theorem coprime_self (n : ℕ) : coprime n n ↔ n = 1 :=
 by simp [coprime]
 
+lemma coprime.eq_of_mul_eq_zero {m n : ℕ} (h : m.coprime n) (hmn : m * n = 0) :
+  m = 0 ∧ n = 1 ∨ m = 1 ∧ n = 0 :=
+(nat.eq_zero_of_mul_eq_zero hmn).imp
+  (λ hm, ⟨hm, n.coprime_zero_left.mp $ hm ▸ h⟩)
+  (λ hn, ⟨m.coprime_zero_left.mp $ hn ▸ h.symm, hn⟩)
+
 /-- Represent a divisor of `m * n` as a product of a divisor of `m` and a divisor of `n`. -/
 def prod_dvd_and_dvd_of_dvd_prod {m n k : ℕ} (H : k ∣ m * n) :
   { d : {m' // m' ∣ m} × {n' // n' ∣ n} // k = d.1 * d.2 } :=
diff --git a/src/data/zmod/basic.lean b/src/data/zmod/basic.lean
index d65b32ca40226..8903c732550ce 100644
--- a/src/data/zmod/basic.lean
+++ b/src/data/zmod/basic.lean
@@ -83,7 +83,7 @@ instance fintype : Π (n : ℕ) [fact (0 < n)], fintype (zmod n)
 | 0     h := false.elim $ nat.not_lt_zero 0 h.1
 | (n+1) _ := fin.fintype (n+1)
 
-lemma card (n : ℕ) [fact (0 < n)] : fintype.card (zmod n) = n :=
+@[simp] lemma card (n : ℕ) [fact (0 < n)] : fintype.card (zmod n) = n :=
 begin
   casesI n,
   { exfalso, exact nat.not_lt_zero 0 (fact.out _) },
@@ -176,6 +176,14 @@ def cast : Π {n : ℕ}, zmod n → R
 @[simp] lemma cast_zero : ((0 : zmod n) : R) = 0 :=
 by { cases n; refl }
 
+variables {S : Type*} [has_zero S] [has_one S] [has_add S] [has_neg S]
+
+@[simp] lemma _root_.prod.fst_zmod_cast (a : zmod n) : (a : R × S).fst = a :=
+by cases n; simp
+
+@[simp] lemma _root_.prod.snd_zmod_cast (a : zmod n) : (a : R × S).snd = a :=
+by cases n; simp
+
 end
 
 /-- So-named because the coercion is `nat.cast` into `zmod`. For `nat.cast` into an arbitrary ring,
@@ -577,6 +585,54 @@ def units_equiv_coprime {n : ℕ} [fact (0 < n)] :
   left_inv := λ ⟨_, _, _, _⟩, units.ext (nat_cast_zmod_val _),
   right_inv := λ ⟨_, _⟩, by simp }
 
+/-- The **Chinese remainder theorem**. For a pair of coprime natural numbers, `m` and `n`,
+  the rings `zmod (m * n)` and `zmod m × zmod n` are isomorphic. 
+
+See `ideal.quotient_inf_ring_equiv_pi_quotient` for the Chinese remainder theorem for ideals in any
+ring.
+-/
+def chinese_remainder {m n : ℕ} (h : m.coprime n) :
+  zmod (m * n) ≃+* zmod m × zmod n :=
+let to_fun : zmod (m * n) → zmod m × zmod n :=
+  zmod.cast_hom (show m.lcm n ∣ m * n, by simp [nat.lcm_dvd_iff]) (zmod m × zmod n) in
+let inv_fun : zmod m × zmod n → zmod (m * n) :=
+  λ x, if m * n = 0
+    then if m = 1
+      then ring_hom.snd _ _ x
+      else ring_hom.fst _ _ x
+    else nat.modeq.chinese_remainder h x.1.val x.2.val in
+have inv : function.left_inverse inv_fun to_fun ∧ function.right_inverse inv_fun to_fun :=
+  if hmn0 : m * n = 0
+    then begin
+      rcases h.eq_of_mul_eq_zero hmn0 with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩;
+      simp [inv_fun, to_fun, function.left_inverse, function.right_inverse,
+        ring_hom.eq_int_cast, prod.ext_iff]
+    end
+    else
+      begin
+        haveI : fact (0 < (m * n)) := ⟨nat.pos_of_ne_zero hmn0⟩,
+        haveI : fact (0 < m) := ⟨nat.pos_of_ne_zero $ left_ne_zero_of_mul hmn0⟩,
+        haveI : fact (0 < n) := ⟨nat.pos_of_ne_zero $ right_ne_zero_of_mul hmn0⟩,
+        have left_inv : function.left_inverse inv_fun to_fun,
+        { intro x,
+          dsimp only [dvd_mul_left, dvd_mul_right, zmod.cast_hom_apply, coe_coe, inv_fun, to_fun],
+          conv_rhs { rw ← zmod.nat_cast_zmod_val x },
+          rw [if_neg hmn0, zmod.eq_iff_modeq_nat, ← nat.modeq.modeq_and_modeq_iff_modeq_mul h,
+            prod.fst_zmod_cast, prod.snd_zmod_cast],
+          refine
+            ⟨(nat.modeq.chinese_remainder h (x : zmod m).val (x : zmod n).val).2.left.trans _,
+            (nat.modeq.chinese_remainder h (x : zmod m).val (x : zmod n).val).2.right.trans _⟩,
+          { rw [← zmod.eq_iff_modeq_nat, zmod.nat_cast_zmod_val, zmod.nat_cast_val] },
+          { rw [← zmod.eq_iff_modeq_nat, zmod.nat_cast_zmod_val, zmod.nat_cast_val] } },
+        exact ⟨left_inv, fintype.right_inverse_of_left_inverse_of_card_le left_inv (by simp)⟩,
+      end,
+{ to_fun := to_fun,
+  inv_fun := inv_fun,
+  map_mul' := ring_hom.map_mul _,
+  map_add' := ring_hom.map_add _,
+  left_inv := inv.1,
+  right_inv := inv.2 }
+
 section totient
 open_locale nat