feat(zmod/basic)

src/data/zmod/basic.lean

@@ -751,6 +751,75 @@ end
 lemma val_cast_of_lt {n : ℕ} {a : ℕ} (h : a < n) : (a : zmod n).val = a :=
 by rw [val_nat_cast, nat.mod_eq_of_lt h]
 
+lemma val_le_self (a n : ℕ) : (a : zmod n).val ≤ a :=
+begin
+  cases n,
+  { refl, },
+  { by_cases a < n.succ,
+    { rw zmod.val_cast_of_lt h, },
+    { apply le_trans (zmod.val_le _) (le_of_not_gt h), }, },
+end
+
+lemma val_coe_val_le_val {n m : ℕ} [ne_zero m] (y : zmod n) : (y.val : zmod m).val ≤ y.val :=
+begin
+  by_cases y.val < m,
+  { rw zmod.val_cast_of_lt h, },
+  { apply le_of_lt (gt_of_ge_of_gt (not_lt.1 h) (zmod.val_lt (y.val : zmod m))), },
+end
+
+lemma val_coe_val_le_val' {n m : ℕ} [ne_zero m] [ne_zero n] (y : zmod n) :
+  (y : zmod m).val ≤ y.val := (@zmod.nat_cast_val _ (zmod m) _ _ y) ▸ val_coe_val_le_val y
+
+lemma coe_val_eq_val_of_lt {n m : ℕ} [ne_zero n] (h : n < m) (b : zmod n) :
+  (b.val : zmod m).val = b.val :=
+begin
+  have h2 : b.val = (b : zmod m).val,
+  { rw ←zmod.val_cast_of_lt (lt_trans (zmod.val_lt b) h),
+    refine congr_arg _ (zmod.nat_cast_val _), },
+  conv_rhs { rw h2, },
+  refine congr_arg _ _,
+  rwa zmod.nat_cast_val _,
+end
+
+lemma zero_le_div_and_div_lt_one {n : ℕ} [ne_zero n] (x : zmod n) :
+  0 ≤ (x.val : ℚ) / n ∧ (x.val : ℚ) / n < 1 :=
+⟨div_nonneg (nat.cast_le.2 (nat.zero_le _)) (nat.cast_le.2 (nat.zero_le _)), (div_lt_one
+  $ by {refine nat.cast_pos.2 (ne_zero.pos _)}).2 -- removing the by and refine does not work?
+    (nat.cast_lt.2 (zmod.val_lt _))⟩
+
+lemma nat_cast_zmod_cast_int {n a : ℕ} (h : a < n) : ((a : zmod n) : ℤ) = (a : ℤ) :=
+begin
+  by_cases h' : 0 < n,
+  { rw ←zmod.nat_cast_val _,
+    { apply congr rfl (zmod.val_cast_of_lt h), },
+    { apply ne_zero.of_pos h', }, },
+  simp only [not_lt, _root_.le_zero_iff] at h',
+  rw h',
+  simp only [zmod.cast_id', id.def],
+end
+
+lemma cast_int_one {n : ℕ} [fact (1 < n)] : ((1 : zmod n) : ℤ) = 1 :=
+begin
+  rwa [←zmod.nat_cast_val _, zmod.val_one _],
+  simp only [int.coe_nat_zero, int.coe_nat_succ, zero_add],
+  { assumption, },
+  { refine ⟨ne_zero_of_lt (fact.out (1 < n))⟩, },
+end
+
+lemma cast_nat_eq_zero_of_dvd {m n : ℕ} (h : m ∣ n) : (n : zmod m) = 0 :=
+begin
+  rw [←zmod.cast_nat_cast h, zmod.nat_cast_self, zmod.cast_zero],
+  refine zmod.char_p _,
+end
+
+lemma dvd_val_sub_cast_val {m : ℕ} (n : ℕ) [ne_zero m] [ne_zero n] (a : zmod m) :
+  n ∣ a.val - (a : zmod n).val :=
+begin
+  have : (a.val : zmod n) = ((a : zmod n).val : zmod n),
+  { rw [nat_cast_val, nat_cast_val], norm_cast, },
+  exact nat.dvd_iff_mod_eq_zero.2 (nat.sub_mod_eq_zero_of_mod_eq ((eq_iff_modeq_nat _).1 this)),
+end
+
 lemma neg_val' {n : ℕ} [ne_zero n] (a : zmod n) : (-a).val = (n - a.val) % n :=
 calc (-a).val = val (-a)    % n : by rw nat.mod_eq_of_lt ((-a).val_lt)
           ... = (n - val a) % n : nat.modeq.add_right_cancel' _ (by rw [nat.modeq, ←val_add,
@@ -1021,6 +1090,20 @@ instance subsingleton_ring_equiv [semiring R] : subsingleton (zmod n ≃+* R) :=
   f k = k :=
 by { cases n; simp }
 
+lemma cast_eq_of_dvd {m n : ℕ} (h : m ∣ n) (a : zmod m) : ((a : zmod n) : zmod m) = a :=
+begin
+  conv_rhs { rw ←zmod.ring_hom_map_cast (zmod.cast_hom h (zmod m)) a, },
+  rw zmod.cast_hom_apply,
+end
+
+@[simp]
+lemma cast_hom_self {n : ℕ} : zmod.cast_hom dvd_rfl (zmod n) = ring_hom.id (zmod n) := by simp
+
+@[simp]
+lemma cast_hom_comp {n m d : ℕ} (hm : n ∣ m) (hd : m ∣ d) :
+  (zmod.cast_hom hm (zmod n)).comp (zmod.cast_hom hd (zmod m)) = zmod.cast_hom (dvd_trans hm hd)
+  (zmod n) := ring_hom.ext_zmod _ _
+
 lemma ring_hom_right_inverse [ring R] (f : R →+* (zmod n)) :
   function.right_inverse (coe : zmod n → R) f :=
 ring_hom_map_cast f

src/data/zmod/crt_properties.lean

@@ -0,0 +1,98 @@
+/-
+Copyright (c) 2023 Ashvni Narayanan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ashvni Narayanan
+-/
+import data.zmod.basic
+import number_theory.padics.ring_homs
+
+/-!
+# Properties of ℤ/nℤ for the Chinese Remainder Theorem
+
+This file has some theorems regarding coercions with respect to the Chinese Remainder Theorem for
+`zmod n` for all `n`.
+
+## Main definitions and theorems
+ * `proj_fst`, `proj_snd`, `inv_fst`, `inv_snd` : lemmas regarding CRT
+
+## Tags
+zmod, CRT
+-/
+
+namespace zmod
+namespace chinese_remainder_theorem
+
+lemma proj_fst' {m n : ℕ} (h : m.coprime n) (a : zmod m) (b : zmod n) :
+  zmod.cast_hom (show m ∣ m * n, from dvd.intro n rfl) (zmod m)
+    ((zmod.chinese_remainder h).symm (a,b)) = a :=
+begin
+  change _ = prod.fst (a, b),
+  have h2 : zmod.cast_hom (show m.lcm n ∣ m * n,
+    by simp [nat.lcm_dvd_iff]) (zmod m × zmod n) _ = _,
+    exact (zmod.chinese_remainder h).right_inv (a,b),
+  conv_rhs { rw ←h2, },
+  convert_to _ = (ring_hom.comp (ring_hom.fst (zmod m) (zmod n))
+    (zmod.cast_hom _ (zmod m × zmod n))) ((zmod.chinese_remainder h).inv_fun (a, b)) using 1,
+  apply congr _ rfl, congr,
+  refine ring_hom.ext_zmod _ _,
+end
+
+lemma proj_snd' {m n : ℕ} (h : m.coprime n) (a : zmod m) (b : zmod n) :
+  zmod.cast_hom (show n ∣ m * n, from dvd.intro_left m rfl) (zmod n)
+    ((zmod.chinese_remainder h).symm (a,b)) = b :=
+begin
+  change _ = prod.snd (a, b),
+  have h2 : zmod.cast_hom (show m.lcm n ∣ m * n,
+    by simp [nat.lcm_dvd_iff]) (zmod m × zmod n) _ = _,
+    exact (zmod.chinese_remainder h).right_inv (a,b),
+  conv_rhs { rw ←h2, },
+  convert_to _ = (ring_hom.comp (ring_hom.snd (zmod m) (zmod n))
+    (zmod.cast_hom _ (zmod m × zmod n))) ((zmod.chinese_remainder h).inv_fun (a, b)) using 1,
+  apply congr _ rfl, congr,
+  refine ring_hom.ext_zmod _ _,
+end
+
+open zmod
+lemma inv_fst' {m n : ℕ} (x : zmod (m * n)) (cop : m.coprime n) :
+  (((zmod.chinese_remainder cop).to_equiv) x).fst = (x : zmod m) :=
+by { simp only [zmod.chinese_remainder, ring_equiv.to_equiv_eq_coe, ring_equiv.coe_to_equiv,
+  ring_equiv.coe_mk, cast_hom_apply, prod.fst_zmod_cast]}
+-- takes a long time to compile if not squeezed
+
+lemma inv_snd' {m n : ℕ} (x : zmod (m * n)) (cop : m.coprime n) :
+  (((zmod.chinese_remainder cop).to_equiv) x).snd = (x : zmod n) :=
+by { simp only [zmod.chinese_remainder, ring_equiv.to_equiv_eq_coe, ring_equiv.coe_to_equiv,
+  ring_equiv.coe_mk, zmod.cast_hom_apply, prod.snd_zmod_cast], }
+
+variables {p : ℕ} {d : ℕ}
+open padic_int
+
+lemma proj_fst [fact p.prime] {n : ℕ} (x : zmod d × ℤ_[p]) (cop : d.coprime (p^n)) :
+  ↑((zmod.chinese_remainder cop).symm (x.fst, (to_zmod_pow n) x.snd)) = x.fst := proj_fst' _ _ _
+
+lemma proj_snd [fact p.prime] {n : ℕ} (x : zmod d × ℤ_[p]) (cop : d.coprime (p^n)) :
+  ↑((zmod.chinese_remainder cop).symm (x.fst, (to_zmod_pow n) x.snd)) =
+  (to_zmod_pow n) x.snd :=
+proj_snd' _ _ _
+
+lemma inv_fst {n : ℕ} (x : zmod (d * p^n)) (cop : d.coprime (p^n)) :
+  (((zmod.chinese_remainder cop).to_equiv) x).fst = (x : zmod d) := inv_fst' x _
+
+lemma inv_snd {n : ℕ} (x : zmod (d * p^n)) (cop : d.coprime (p^n)) :
+  (((zmod.chinese_remainder cop).to_equiv) x).snd = (x : zmod (p^n)) := inv_snd' _ _
+
+variable (p)
+lemma proj_fst'' {n : ℕ} (hd : d.coprime p) (a : (zmod d)ˣ × (zmod (p^n))ˣ) :
+  ((zmod.chinese_remainder (nat.coprime.pow_right n hd)).inv_fun (↑(a.fst), ↑(a.snd)) : zmod d) =
+  a.fst :=
+by { rw ring_equiv.inv_fun_eq_symm, apply proj_fst', }
+
+lemma proj_snd'' [fact p.prime] {n : ℕ} (hd : d.coprime p) (a : (zmod d)ˣ × (zmod (p^n))ˣ) :
+  (padic_int.to_zmod_pow n) ((zmod.chinese_remainder (nat.coprime.pow_right n hd)).inv_fun
+  (↑(a.fst), ↑(a.snd)) : ℤ_[p]) = a.snd :=
+begin
+  rw [← zmod.int_cast_cast, map_int_cast, zmod.int_cast_cast, ring_equiv.inv_fun_eq_symm],
+  convert proj_snd' _ _ _,
+end
+end chinese_remainder_theorem
+end zmod

src/data/zmod/units.lean

@@ -0,0 +1,169 @@
+/-
+Copyright (c) 2023 Ashvni Narayanan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ashvni Narayanan
+-/
+import data.zmod.basic
+import topology.algebra.constructions
+
+/-!
+# Properties of units of ℤ/nℤ
+
+This file enlists some properties of units of `zmod n`. We then define a topological structure
+(the discrete topology) on `zmod n` for all `n` and consequently on the units.
+We also enlist several properties that are helpful with modular arithmetic.
+
+## Main definitions and theorems
+ * `zmod.topological_space`
+ * `cast_hom_apply'` : a version of `cast_hom_apply` where `R` is explicit
+ * `disc_top_units` : giving discrete topology to `units (zmod n)`
+
+## Tags
+zmod, units
+-/
+
+open zmod nat
+namespace zmod
+/-- Same as `zmod.cast_hom_apply` with some hypotheses being made explicit. -/
+lemma cast_hom_apply' {n : ℕ} (R : Type*) [ring R] {m : ℕ} [char_p R m]
+  (h : m ∣ n) (i : zmod n) : (cast_hom h R) i = ↑i := cast_hom_apply i
+
+lemma coe_map_of_dvd {a b : ℕ} (h : a ∣ b) {x : (zmod b)} (hx : is_unit x) :
+  is_unit (x : zmod a) := is_unit.map (cast_hom h (zmod a)).to_monoid_hom hx
+
+lemma is_unit_of_is_coprime_dvd {a b : ℕ} (h : a ∣ b) {x : ℕ} (hx : x.coprime b) :
+  is_unit (x : zmod a) :=
+begin
+  convert_to is_unit ((zmod.unit_of_coprime _ hx : zmod b) : zmod a),
+  { rw ←cast_nat_cast h x,
+    { congr, },
+    { refine zmod.char_p _, }, },
+  { apply coe_map_of_dvd h (units.is_unit _), },
+end
+
+lemma is_unit_mul {a b g : ℕ} (n : ℕ) (h1 : g.coprime a) (h2 : g.coprime b) :
+  is_unit (g : zmod (a * b^n)) :=
+is_unit_of_is_coprime_dvd dvd_rfl ((coprime.mul_right h1 (coprime.pow_right _ h2)))
+
+lemma cast_inv {a m n : ℕ} (ha : a.coprime n) (h : m ∣ n) :
+  (((a : zmod n)⁻¹ : zmod n) : zmod m) = ((a : zmod n) : zmod m)⁻¹ :=
+begin
+  change ((((zmod.unit_of_coprime a ha)⁻¹ : units (zmod n)) : zmod n) : zmod m) = _,
+  have h1 : ∀ c : (zmod m)ˣ, (c : zmod m)⁻¹ = ((c⁻¹ : units (zmod m)) : zmod m),
+  { intro c, simp only [inv_coe_unit], },
+  rw [← zmod.cast_hom_apply' (zmod m) h _, ← ring_hom.coe_monoid_hom,
+    ← units.coe_map_inv _ (zmod.unit_of_coprime a ha), ← h1],
+  congr,
+end
+
+lemma coprime_of_is_unit {m a : ℕ} (ha : is_unit (a : zmod m)) : a.coprime m :=
+begin
+  have f := zmod.val_coe_unit_coprime (is_unit.unit ha),
+  rw is_unit.unit_spec at f,
+  obtain ⟨y, hy⟩ : m ∣ (a - (a : zmod m).val),
+  { rw [← zmod.nat_coe_zmod_eq_zero_iff_dvd, nat.cast_sub (zmod.val_le_self _ _), sub_eq_zero],
+    cases m,
+    { simp only [int.coe_nat_inj'], refl, },
+    { rw zmod.nat_cast_val, simp only [zmod.cast_nat_cast'], }, },
+  rw nat.sub_eq_iff_eq_add (zmod.val_le_self _ _) at hy,
+  rw [hy, add_comm, ← nat.is_coprime_iff_coprime],
+  simp only [int.coe_nat_add, int.coe_nat_mul],
+  rw [is_coprime.add_mul_left_left_iff, nat.is_coprime_iff_coprime],
+  convert zmod.val_coe_unit_coprime (is_unit.unit ha),
+end
+
+instance units_fintype {n : ℕ} : fintype (zmod n)ˣ :=
+begin
+  by_cases n = 0,
+  { rw h, refine units_int.fintype, },
+  { haveI : ne_zero n := ⟨h⟩,
+    apply units.fintype, },
+end
+
+lemma is_unit_of_is_unit_mul {m n : ℕ} (x : ℕ) (hx : is_unit (x : zmod (m * n))) :
+  is_unit (x : zmod m) :=
+begin
+  rw is_unit_iff_dvd_one at *,
+  cases hx with k hk,
+  refine ⟨(k : zmod m), _⟩,
+  rw [← zmod.cast_nat_cast (dvd_mul_right m n), ← zmod.cast_mul (dvd_mul_right m n),
+   ← hk, zmod.cast_one (dvd_mul_right m n)],
+  any_goals { refine zmod.char_p _, },
+end
+
+lemma is_unit_of_is_unit_mul' {m n : ℕ} (x : ℕ) (hx : is_unit (x : zmod (m * n))) :
+  is_unit (x : zmod n) :=
+begin
+  rw mul_comm at hx,
+  apply is_unit_of_is_unit_mul x hx,
+end
+
+open zmod
+lemma is_unit_of_is_unit_mul_iff {m n : ℕ} (x : ℕ) : is_unit (x : zmod (m * n)) ↔
+  is_unit (x : zmod m) ∧ is_unit (x : zmod n) :=
+  ⟨λ h, ⟨is_unit_of_is_unit_mul x h, is_unit_of_is_unit_mul' x h⟩,
+   λ ⟨h1, h2⟩, units.is_unit (zmod.unit_of_coprime x (nat.coprime.mul_right
+      (coprime_of_is_unit h1) (coprime_of_is_unit h2))), ⟩
+
+lemma not_is_unit_of_not_is_unit_mul {m n x : ℕ} (hx : ¬ is_unit (x : zmod (m * n))) :
+  ¬ is_unit (x : zmod m) ∨ ¬ is_unit (x : zmod n) :=
+begin
+  rw ← not_and_distrib,
+  contrapose hx,
+  rw not_not at *,
+  rw is_unit_of_is_unit_mul_iff,
+  refine ⟨hx.1, hx.2⟩,
+end
+
+lemma not_is_unit_of_not_is_unit_mul' {m n : ℕ} [ne_zero (m * n)] (x : zmod (m * n))
+  (hx : ¬ is_unit x) : ¬ is_unit (x : zmod m) ∨ ¬ is_unit (x : zmod n) :=
+begin
+  rw [← zmod.cast_id _ x, ← zmod.nat_cast_val] at hx,
+  rw [← zmod.nat_cast_val, ← zmod.nat_cast_val],
+  apply not_is_unit_of_not_is_unit_mul hx,
+end
+
+lemma is_unit_val_of_unit {n k : ℕ} [ne_zero n] (hk : k ∣ n) (u : (zmod n)ˣ) :
+  is_unit ((u : zmod n).val : zmod k) :=
+by { apply zmod.is_unit_of_is_coprime_dvd hk (coprime_of_is_unit _),
+  rw [zmod.nat_cast_val, zmod.cast_id], apply units.is_unit _, }
+
+lemma unit_ne_zero {n : ℕ} [fact (1 < n)] (a : (zmod n)ˣ) : (a : zmod n).val ≠ 0 :=
+begin
+  intro h,
+  rw zmod.val_eq_zero at h,
+  have : is_unit (0 : zmod n),
+  { rw ← h, simp, },
+  rw is_unit_zero_iff at this,
+  apply @zero_ne_one _ _ _ _,
+  rw this,
+  apply_instance,
+end
+
+lemma inv_is_unit_of_is_unit {n : ℕ} {u : zmod n} (h : is_unit u) : is_unit u⁻¹ :=
+begin
+  have h' := is_unit_iff_dvd_one.1 h,
+  cases h' with k h',
+  rw is_unit_iff_dvd_one,
+  refine ⟨u, _⟩,
+  rw zmod.inv_mul_of_unit u h,
+end
+end zmod
+
+/-- Making `zmod` a discrete topological space. -/
+def zmod.topological_space (d : ℕ) : topological_space (zmod d) := ⊥
+
+local attribute [instance] zmod.topological_space
+instance {n : ℕ} : discrete_topology (zmod n) := ⟨rfl⟩
+
+namespace zmod
+@[continuity]
+lemma induced_top_cont_inv {n : ℕ} : @continuous _ _ (topological_space.induced
+  (units.coe_hom (zmod n)) infer_instance) _ (units.inv : (zmod n)ˣ → zmod n) :=
+units.induced_top_cont_inv
+
+instance {k : ℕ} : discrete_topology (zmod k)ˣ := units.discrete_topology_of_discrete
+
+instance discrete_prod_units {m n : ℕ} : discrete_topology (zmod m × zmod n)ˣ :=
+units.discrete_prod_units
+end zmod