feat(algebra/group/hom): cancel injective/surjective monoid_homs (#…

…2112)

* feat(algebra/group/hom): cancel injective/surjective `monoid_hom`s

* Add a `ring_hom` version

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

src/algebra/group/hom.lean

@@ -134,6 +134,16 @@ lemma exists_inv_of_comp_exists_inv {S : set M} {f : M →* N}
   ∃ x : P, g.comp f s * x = 1 :=
 let ⟨c, hc⟩ := hf s H in ⟨g c, show g _ * _ = _, by rw [←g.map_mul, hc, g.map_one]⟩
 
+@[to_additive]
+lemma cancel_right {g₁ g₂ : N →* P} {f : M →* N} (hf : function.surjective f) :
+  g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=
+⟨λ h, monoid_hom.ext $ (forall_iff_forall_surj hf).1 (ext_iff.1 h), λ h, h ▸ rfl⟩
+
+@[to_additive]
+lemma cancel_left {g : N →* P} {f₁ f₂ : M →* N} (hg : function.injective g) :
+  g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
+⟨λ h, monoid_hom.ext $ λ x, hg $ by rw [← comp_apply, h, comp_apply], λ h, h ▸ rfl⟩
+
 omit mP
 variables [mM] [mN]
 

src/algebra/ring.lean

@@ -421,6 +421,14 @@ lemma comp_assoc {δ} {rδ: semiring δ} (f : α →+* β) (g : β →+* γ) (h
 lemma comp_apply (hnp : β →+* γ) (hmn : α →+* β) (x : α) : (hnp.comp hmn : α → γ) x =
   (hnp (hmn x)) := rfl
 
+lemma cancel_right {g₁ g₂ : β →+* γ} {f : α →+* β} (hf : function.surjective f) :
+  g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=
+⟨λ h, ring_hom.ext $ (forall_iff_forall_surj hf).1 (ext_iff.1 h), λ h, h ▸ rfl⟩
+
+lemma cancel_left {g : β →+* γ} {f₁ f₂ : α →+* β} (hg : function.injective g) :
+  g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
+⟨λ h, ring_hom.ext $ λ x, hg $ by rw [← comp_apply, h, comp_apply], λ h, h ▸ rfl⟩
+
 omit rα rβ rγ
 
 /-- Ring homomorphisms preserve additive inverse. -/