chore(algebra/*): missing simp/inj lemmas (#2557)

Sometimes I have a specialized `ext` lemma for `A →+ B` that uses structure of `A` (e.g., `A = monoid_algebra α R`) and want to apply it to `A →+* B` or `A →ₐ[R] B`. These `coe_*_inj` lemmas make it easier.

Also add missing `simp` lemmas for bundled multiplication and rename `pow_of_add` and `gpow_of_add` to `of_add_smul` and `of_add_gsmul`, respectively.

Author: urkud

src/algebra/group/hom.lean

@@ -271,10 +271,15 @@ def mul_left {R : Type*} [semiring R] (r : R) : R →+ R :=
   map_zero' := mul_zero r,
   map_add' := mul_add r }
 
+@[simp] lemma coe_mul_left {R : Type*} [semiring R] (r : R) : ⇑(mul_left r) = (*) r := rfl
+
 /-- Right multiplication by an element of a (semi)ring is an `add_monoid_hom` -/
 def mul_right {R : Type*} [semiring R] (r : R) : R →+ R :=
 { to_fun := λ a, a * r,
   map_zero' := zero_mul r,
   map_add' := λ _ _, add_mul _ _ r }
 
+@[simp] lemma mul_right_apply {R : Type*} [semiring R] (a r : R) :
+  (mul_right r : R → R) a = a * r := rfl
+
 end add_monoid_hom

src/algebra/group_power.lean

@@ -671,10 +671,10 @@ end int
 @[simp] lemma neg_square {α} [ring α] (z : α) : (-z)^2 = z^2 :=
 by simp [pow, monoid.pow]
 
-@[simp] lemma pow_of_add [add_monoid A] (x : A) (n : ℕ) :
+lemma of_add_smul [add_monoid A] (x : A) (n : ℕ) :
   multiplicative.of_add (n • x) = (multiplicative.of_add x)^n := rfl
 
-@[simp] lemma gpow_of_add [add_group A] (x : A) (n : ℤ) :
+lemma of_add_gsmul [add_group A] (x : A) (n : ℤ) :
   multiplicative.of_add (n •ℤ x) = (multiplicative.of_add x)^n := rfl
 
 variables (M G A)
@@ -685,15 +685,15 @@ def powers_hom [monoid M] : M ≃ (multiplicative ℕ →* M) :=
 { to_fun := λ x, ⟨λ n, x ^ n.to_add, pow_zero x, λ m n, pow_add x m n⟩,
   inv_fun := λ f, f (multiplicative.of_add 1),
   left_inv := pow_one,
-  right_inv := λ f, monoid_hom.ext $ λ n, by { simp [← f.map_pow, ← pow_of_add] } }
+  right_inv := λ f, monoid_hom.ext $ λ n, by { simp [← f.map_pow, ← of_add_smul] } }
 
 /-- Monoid homomorphisms from `multiplicative ℤ` are defined by the image
 of `multiplicative.of_add 1`. -/
 def gpowers_hom [group G] : G ≃ (multiplicative ℤ →* G) :=
 { to_fun := λ x, ⟨λ n, x ^ n.to_add, gpow_zero x, λ m n, gpow_add x m n⟩,
   inv_fun := λ f, f (multiplicative.of_add 1),
   left_inv := gpow_one,
-  right_inv := λ f, monoid_hom.ext $ λ n, by { simp [← f.map_gpow, ← gpow_of_add] } }
+  right_inv := λ f, monoid_hom.ext $ λ n, by { simp [← f.map_gpow, ← of_add_gsmul ] } }
 
 /-- Additive homomorphisms from `ℕ` are defined by the image of `1`. -/
 def multiples_hom [add_monoid A] : A ≃ (ℕ →+ A) :=
@@ -708,3 +708,19 @@ def gmultiples_hom [add_group A] : A ≃ (ℤ →+ A) :=
   inv_fun := λ f, f 1,
   left_inv := one_gsmul,
   right_inv := λ f, add_monoid_hom.ext $ λ n, by simp [← f.map_gsmul] }
+
+variables {M G A}
+
+@[simp] lemma powers_hom_apply [monoid M] (x : M) (n : multiplicative ℕ) :
+  powers_hom M x n = x ^ n.to_add := rfl
+
+@[simp] lemma powers_hom_symm_apply [monoid M] (f : multiplicative ℕ →* M) :
+  (powers_hom M).symm f = f (multiplicative.of_add 1) := rfl
+
+lemma mnat_monoid_hom_eq [monoid M] (f : multiplicative ℕ →* M) (n : multiplicative ℕ) :
+  f n = (f (multiplicative.of_add 1)) ^ n.to_add :=
+by rw [← powers_hom_symm_apply, ← powers_hom_apply, equiv.apply_symm_apply]
+
+lemma mnat_monoid_hom_ext [monoid M] ⦃f g : multiplicative ℕ →* M⦄
+  (h : f (multiplicative.of_add 1) = g (multiplicative.of_add 1)) : f = g :=
+monoid_hom.ext $ λ n, by rw [mnat_monoid_hom_eq f, mnat_monoid_hom_eq g, h]

src/algebra/ring.lean

@@ -357,21 +357,13 @@ instance {α : Type*} {β : Type*} {rα : semiring α} {rβ : semiring β} : has
 instance {α : Type*} {β : Type*} {rα : semiring α} {rβ : semiring β} : has_coe (α →+* β) (α →+ β) :=
 ⟨ring_hom.to_add_monoid_hom⟩
 
-lemma coe_monoid_hom {α : Type*} {β : Type*} {rα : semiring α} {rβ : semiring β}
-  (f : α →+* β) (a : α) :
-  ((f : α →* β) : α → β) a = (f : α → β) a := rfl
-lemma coe_add_monoid_hom {α : Type*} {β : Type*} {rα : semiring α} {rβ : semiring β}
-  (f : α →+* β) (a : α) :
-  ((f : α →+ β) : α → β) a = (f : α → β) a := rfl
-
 @[simp, norm_cast]
-lemma coe_monoid_hom' {α : Type*} {β : Type*} {rα : semiring α} {rβ : semiring β} (f : α →+* β) :
-  ((f : α →* β) : α → β) = (f : α → β) := rfl
+lemma coe_monoid_hom {α : Type*} {β : Type*} {rα : semiring α} {rβ : semiring β} (f : α →+* β) :
+  ⇑(f : α →* β) = f := rfl
 
 @[simp, norm_cast]
-lemma coe_add_monoid_hom' {α : Type*} {β : Type*} {rα : semiring α} {rβ : semiring β}
-  (f : α →+* β) :
-  ((f : α →+ β) : α → β) = (f : α → β) := rfl
+lemma coe_add_monoid_hom {α : Type*} {β : Type*} {rα : semiring α} {rβ : semiring β} (f : α →+* β) :
+  ⇑(f : α →+ β) = f := rfl
 
 namespace ring_hom
 
@@ -400,6 +392,12 @@ coe_inj (funext h)
 theorem ext_iff {f g : α →+* β} : f = g ↔ ∀ x, f x = g x :=
 ⟨λ h x, h ▸ rfl, λ h, ext h⟩
 
+theorem coe_add_monoid_hom_inj : function.injective (coe : (α →+* β) → (α →+ β)) :=
+λ f g h, coe_inj $ show ((f : α →+ β) : α → β) = (g : α →+ β), from congr_arg coe_fn h
+
+theorem coe_monoid_hom_inj : function.injective (coe : (α →+* β) → (α →* β)) :=
+λ f g h, coe_inj $ show ((f : α →* β) : α → β) = (g : α →* β), from congr_arg coe_fn h
+
 /-- Ring homomorphisms map zero to zero. -/
 @[simp] lemma map_zero (f : α →+* β) : f 0 = 0 := f.map_zero'
 

src/ring_theory/algebra.lean

@@ -208,18 +208,35 @@ instance coe_ring_hom : has_coe (A →ₐ[R] B) (A →+* B) := ⟨alg_hom.to_rin
 
 instance coe_monoid_hom : has_coe (A →ₐ[R] B) (A →* B) := ⟨λ f, ↑(f : A →+* B)⟩
 
+instance coe_add_monoid_hom : has_coe (A →ₐ[R] B) (A →+ B) := ⟨λ f, ↑(f : A →+* B)⟩
+
 @[simp, norm_cast] lemma coe_mk {f : A → B} (h₁ h₂ h₃ h₄ h₅) :
   ⇑(⟨f, h₁, h₂, h₃, h₄, h₅⟩ : A →ₐ[R] B) = f := rfl
 
 @[simp, norm_cast] lemma coe_to_ring_hom (f : A →ₐ[R] B) : ⇑(f : A →+* B) = f := rfl
 
 @[simp, norm_cast] lemma coe_to_monoid_hom (f : A →ₐ[R] B) : ⇑(f : A →* B) = f := rfl
 
+@[simp, norm_cast] lemma coe_to_add_monoid_hom (f : A →ₐ[R] B) : ⇑(f : A →+ B) = f := rfl
+
 variables (φ : A →ₐ[R] B)
 
+theorem coe_fn_inj ⦃φ₁ φ₂ : A →ₐ[R] B⦄ (H : ⇑φ₁ = φ₂) : φ₁ = φ₂ :=
+by { cases φ₁, cases φ₂, congr, exact H }
+
+theorem coe_ring_hom_inj : function.injective (coe : (A →ₐ[R] B) → (A →+* B)) :=
+λ φ₁ φ₂ H, coe_fn_inj $ show ((φ₁ : (A →+* B)) : A → B) = ((φ₂ : (A →+* B)) : A → B),
+  from congr_arg _ H
+
+theorem coe_monoid_hom_inj : function.injective (coe : (A →ₐ[R] B)  → (A →* B)) :=
+function.injective_comp ring_hom.coe_monoid_hom_inj coe_ring_hom_inj
+
+theorem coe_add_monoid_hom_inj : function.injective (coe : (A →ₐ[R] B)  → (A →+ B)) :=
+function.injective_comp ring_hom.coe_add_monoid_hom_inj coe_ring_hom_inj
+
 @[ext]
 theorem ext ⦃φ₁ φ₂ : A →ₐ[R] B⦄ (H : ∀ x, φ₁ x = φ₂ x) : φ₁ = φ₂ :=
-by cases φ₁; cases φ₂; congr' 1; ext; apply H
+coe_fn_inj $ funext H
 
 theorem commutes (r : R) : φ (algebra_map R A r) = algebra_map R B r := φ.commutes' r