chore(algebra/char_zero): rename vars, add with_top instance (#4523)

Motivated by #3135.

* Use `R` as a `Type*` variable;
* Add `add_monoid_hom.map_nat_cast` and `with_top.coe_add_hom`;
* Drop versions of `char_zero_of_inj_zero`, use `[add_left_cancel_monoid R]` instead.

src/algebra/char_p.lean

@@ -241,7 +241,7 @@ section
 variables (α : Type u) [ring α]
 
 lemma char_p_to_char_zero [char_p α 0] : char_zero α :=
-add_group.char_zero_of_inj_zero $
+char_zero_of_inj_zero $
   λ n h0, eq_zero_of_zero_dvd ((cast_eq_zero_iff α 0 n).mp h0)
 
 lemma cast_eq_mod (p : ℕ) [char_p α p] (k : ℕ) : (k : α) = (k % p : ℕ) :=

src/algebra/char_zero.lean

@@ -10,61 +10,47 @@ import tactic.wlog
 
 /-- Typeclass for monoids with characteristic zero.
   (This is usually stated on fields but it makes sense for any additive monoid with 1.) -/
-class char_zero (α : Type*) [add_monoid α] [has_one α] : Prop :=
-(cast_injective : function.injective (coe : ℕ → α))
+class char_zero (R : Type*) [add_monoid R] [has_one R] : Prop :=
+(cast_injective : function.injective (coe : ℕ → R))
 
-theorem char_zero_of_inj_zero {α : Type*} [add_monoid α] [has_one α]
-  (add_left_cancel : ∀ a b c : α, a + b = a + c → b = c)
-  (H : ∀ n:ℕ, (n:α) = 0 → n = 0) : char_zero α :=
+theorem char_zero_of_inj_zero {R : Type*} [add_left_cancel_monoid R] [has_one R]
+  (H : ∀ n:ℕ, (n:R) = 0 → n = 0) : char_zero R :=
 ⟨λ m n, begin
    assume h,
    wlog hle : m ≤ n,
    cases nat.le.dest hle with k e,
    suffices : k = 0, by rw [← e, this, add_zero],
-   apply H, apply add_left_cancel n,
+   apply H, apply @add_left_cancel R _ n,
    rw [← h, ← nat.cast_add, e, add_zero, h]
  end⟩
 
--- We have no `left_cancel_add_monoid`, so we restate it for `add_group`
--- and `ordered_cancel_comm_monoid`.
-
-theorem add_group.char_zero_of_inj_zero {α : Type*} [add_group α] [has_one α]
-  (H : ∀ n:ℕ, (n:α) = 0 → n = 0) : char_zero α :=
-char_zero_of_inj_zero (@add_left_cancel _ _) H
-
-theorem ordered_cancel_comm_monoid.char_zero_of_inj_zero {α : Type*}
-  [ordered_cancel_add_comm_monoid α] [has_one α]
-  (H : ∀ n:ℕ, (n:α) = 0 → n = 0) : char_zero α :=
-char_zero_of_inj_zero (@add_left_cancel _ _) H
-
 @[priority 100] -- see Note [lower instance priority]
-instance linear_ordered_semiring.to_char_zero {α : Type*}
-  [linear_ordered_semiring α] : char_zero α :=
-ordered_cancel_comm_monoid.char_zero_of_inj_zero $
-λ n h, nat.eq_zero_of_le_zero $
-  (@nat.cast_le α _ _ _).1 (le_of_eq h)
+instance linear_ordered_semiring.to_char_zero {R : Type*}
+  [linear_ordered_semiring R] : char_zero R :=
+char_zero_of_inj_zero $ λ n h, nat.eq_zero_of_le_zero $
+  (@nat.cast_le R _ _ _).1 (le_of_eq h)
 
 namespace nat
-variables {α : Type*} [add_monoid α] [has_one α] [char_zero α]
+variables {R : Type*} [add_monoid R] [has_one R] [char_zero R]
 
-theorem cast_injective : function.injective (coe : ℕ → α) :=
+theorem cast_injective : function.injective (coe : ℕ → R) :=
 char_zero.cast_injective
 
-@[simp, norm_cast] theorem cast_inj {m n : ℕ} : (m : α) = n ↔ m = n :=
+@[simp, norm_cast] theorem cast_inj {m n : ℕ} : (m : R) = n ↔ m = n :=
 cast_injective.eq_iff
 
-@[simp, norm_cast] theorem cast_eq_zero {n : ℕ} : (n : α) = 0 ↔ n = 0 :=
+@[simp, norm_cast] theorem cast_eq_zero {n : ℕ} : (n : R) = 0 ↔ n = 0 :=
 by rw [← cast_zero, cast_inj]
 
-@[norm_cast] theorem cast_ne_zero {n : ℕ} : (n : α) ≠ 0 ↔ n ≠ 0 :=
+@[norm_cast] theorem cast_ne_zero {n : ℕ} : (n : R) ≠ 0 ↔ n ≠ 0 :=
 not_congr cast_eq_zero
 
-lemma cast_add_one_ne_zero (n : ℕ) : (n + 1 : α) ≠ 0 :=
+lemma cast_add_one_ne_zero (n : ℕ) : (n + 1 : R) ≠ 0 :=
 by exact_mod_cast n.succ_ne_zero
 
 @[simp, norm_cast]
-theorem cast_dvd_char_zero {α : Type*} [field α] [char_zero α] {m n : ℕ}
-  (n_dvd : n ∣ m) : ((m / n : ℕ) : α) = m / n :=
+theorem cast_dvd_char_zero {k : Type*} [field k] [char_zero k] {m n : ℕ}
+  (n_dvd : n ∣ m) : ((m / n : ℕ) : k) = m / n :=
 begin
   by_cases hn : n = 0,
   { subst hn,
@@ -74,32 +60,39 @@ end
 
 end nat
 
-@[field_simps] lemma two_ne_zero' {α : Type*} [add_monoid α] [has_one α] [char_zero α] : (2:α) ≠ 0 :=
-have ((2:ℕ):α) ≠ 0, from nat.cast_ne_zero.2 dec_trivial,
+@[field_simps] lemma two_ne_zero' {R : Type*} [add_monoid R] [has_one R] [char_zero R] : (2:R) ≠ 0 :=
+have ((2:ℕ):R) ≠ 0, from nat.cast_ne_zero.2 dec_trivial,
 by rwa [nat.cast_succ, nat.cast_one] at this
 
 section
-variables {α : Type*} [semiring α] [no_zero_divisors α] [char_zero α]
+variables {R : Type*} [semiring R] [no_zero_divisors R] [char_zero R]
 
-lemma add_self_eq_zero {a : α} : a + a = 0 ↔ a = 0 :=
+lemma add_self_eq_zero {a : R} : a + a = 0 ↔ a = 0 :=
 by simp only [(two_mul a).symm, mul_eq_zero, two_ne_zero', false_or]
 
-lemma bit0_eq_zero {a : α} : bit0 a = 0 ↔ a = 0 := add_self_eq_zero
+lemma bit0_eq_zero {a : R} : bit0 a = 0 ↔ a = 0 := add_self_eq_zero
 end
 
 section
-variables {α : Type*} [division_ring α] [char_zero α]
+variables {R : Type*} [division_ring R] [char_zero R]
 
-@[simp] lemma half_add_self (a : α) : (a + a) / 2 = a :=
+@[simp] lemma half_add_self (a : R) : (a + a) / 2 = a :=
 by rw [← mul_two, mul_div_cancel a two_ne_zero']
 
-@[simp] lemma add_halves' (a : α) : a / 2 + a / 2 = a :=
+@[simp] lemma add_halves' (a : R) : a / 2 + a / 2 = a :=
 by rw [← add_div, half_add_self]
 
-lemma sub_half (a : α) : a - a / 2 = a / 2 :=
+lemma sub_half (a : R) : a - a / 2 = a / 2 :=
 by rw [sub_eq_iff_eq_add, add_halves']
 
-lemma half_sub (a : α) : a / 2 - a = - (a / 2) :=
+lemma half_sub (a : R) : a / 2 - a = - (a / 2) :=
 by rw [← neg_sub, sub_half]
 
 end
+
+namespace with_top
+
+instance {R : Type*} [add_monoid R] [has_one R] [char_zero R] : char_zero (with_top R) :=
+{ cast_injective := λ m n h, by rwa [← coe_nat, ← coe_nat n, coe_eq_coe, nat.cast_inj] at h }
+
+end with_top

src/algebra/ordered_group.lean

@@ -424,6 +424,12 @@ begin
     exact ⟨_, rfl, add_le_add_left h _⟩, }
 end
 
+/-- Coercion from `α` to `with_top α` as an `add_monoid_hom`. -/
+def coe_add_hom [add_monoid α] : α →+ with_top α :=
+⟨coe, rfl, λ _ _, rfl⟩
+
+@[simp] lemma coe_coe_add_hom [add_monoid α] : ⇑(coe_add_hom : α →+ with_top α) = coe := rfl
+
 @[simp] lemma zero_lt_top [ordered_add_comm_monoid α] : (0 : with_top α) < ⊤ :=
 coe_lt_top 0
 

src/data/complex/basic.lean

@@ -336,7 +336,7 @@ by rw [← of_real_rat_cast, of_real_im]
 /-! ### Characteristic zero -/
 
 instance char_zero_complex : char_zero ℂ :=
-add_group.char_zero_of_inj_zero $ λ n h,
+char_zero_of_inj_zero $ λ n h,
 by rwa [← of_real_nat_cast, of_real_eq_zero, nat.cast_eq_zero] at h
 
 theorem re_eq_add_conj (z : ℂ) : (z.re : ℂ) = (z + conj z) / 2 :=

src/data/complex/is_R_or_C.lean

@@ -368,7 +368,7 @@ by rw [← of_real_rat_cast, of_real_im]
 Note: This is not registered as an instance to avoid having multiple instances on ℝ and ℂ.
 -/
 lemma char_zero_R_or_C : char_zero K :=
-add_group.char_zero_of_inj_zero $ λ n h,
+char_zero_of_inj_zero $ λ n h,
 by rwa [← of_real_nat_cast, of_real_eq_zero, nat.cast_eq_zero] at h
 
 theorem re_eq_add_conj (z : K) : 𝓚 (re z) = (z + conj z) / 2 :=

src/data/nat/cast.lean

@@ -178,15 +178,20 @@ end nat
 
 namespace add_monoid_hom
 
-variables {A : Type*} [add_monoid A]
+variables {A B : Type*} [add_monoid A]
 
 @[ext] lemma ext_nat {f g : ℕ →+ A} (h : f 1 = g 1) : f = g :=
 ext $ λ n, nat.rec_on n (f.map_zero.trans g.map_zero.symm) $ λ n ihn,
 by simp only [nat.succ_eq_add_one, *, map_add]
 
-lemma eq_nat_cast {A} [add_monoid A] [has_one A] (f : ℕ →+ A) (h1 : f 1 = 1) :
+variables [has_one A] [add_monoid B] [has_one B]
+
+lemma eq_nat_cast (f : ℕ →+ A) (h1 : f 1 = 1) :
   ∀ n : ℕ, f n = n :=
-ext_iff.1 $ show f = nat.cast_add_monoid_hom A, from ext_nat (h1.trans nat.cast_one.symm)
+congr_fun $ show f = nat.cast_add_monoid_hom A, from ext_nat (h1.trans nat.cast_one.symm)
+
+lemma map_nat_cast (f : A →+ B) (h1 : f 1 = 1) (n : ℕ) : f n = n :=
+(f.comp (nat.cast_add_monoid_hom A)).eq_nat_cast (by simp [h1]) _
 
 end add_monoid_hom