feat(algebra/*): injective hom into kernel map_eq_*_iff (#11275)

src/algebra/free_algebra.lean

@@ -337,10 +337,10 @@ lemma algebra_map_left_inverse :
 algebra_map_left_inverse.injective.eq_iff
 
 @[simp] lemma algebra_map_eq_zero_iff (x : R) : algebra_map R (free_algebra R X) x = 0 ↔ x = 0 :=
-algebra_map_inj x 0
+map_eq_zero_iff (algebra_map _ _) algebra_map_left_inverse.injective
 
 @[simp] lemma algebra_map_eq_one_iff (x : R) : algebra_map R (free_algebra R X) x = 1 ↔ x = 1 :=
-algebra_map_inj x 1
+map_eq_one_iff (algebra_map _ _) algebra_map_left_inverse.injective
 
 -- this proof is copied from the approach in `free_abelian_group.of_injective`
 lemma ι_injective [nontrivial R] : function.injective (ι R : X → free_algebra R X) :=

src/algebra/group/hom.lean

@@ -181,6 +181,10 @@ instance one_hom.one_hom_class : one_hom_class (one_hom M N) M N :=
 @[simp, to_additive] lemma map_one [one_hom_class F M N] (f : F) : f 1 = 1 :=
 one_hom_class.map_one f
 
+@[to_additive] lemma map_eq_one_iff [one_hom_class F M N] (f : F)
+  (hf : function.injective f) {x : M} : f x = 1 ↔ x = 1 :=
+hf.eq_iff' (map_one f)
+
 end one
 
 section mul
@@ -967,7 +971,7 @@ its kernel is trivial. For the iff statement on the triviality of the kernel,
 see `add_monoid_hom.injective_iff'`. "-/]
 lemma injective_iff {G H} [group G] [mul_one_class H] (f : G →* H) :
   function.injective f ↔ (∀ a, f a = 1 → a = 1) :=
-⟨λ h x hfx, h $ hfx.trans f.map_one.symm,
+⟨λ h x, (map_eq_one_iff f h).mp,
  λ h x y hxy, mul_inv_eq_one.1 $ h _ $ by rw [f.map_mul, hxy, ← f.map_mul, mul_inv_self, f.map_one]⟩
 
 /-- A homomorphism from a group to a monoid is injective iff its kernel is trivial,

src/linear_algebra/exterior_algebra.lean

@@ -209,10 +209,10 @@ lemma algebra_map_left_inverse :
 
 @[simp] lemma algebra_map_eq_zero_iff (x : R) :
   algebra_map R (exterior_algebra R M) x = 0 ↔ x = 0 :=
-by rw [←algebra_map_inj M x 0, ring_hom.map_zero]
+map_eq_zero_iff (algebra_map _ _) (algebra_map_left_inverse _).injective
 
 @[simp] lemma algebra_map_eq_one_iff (x : R) : algebra_map R (exterior_algebra R M) x = 1 ↔ x = 1 :=
-by rw [←algebra_map_inj M x 1, ring_hom.map_one]
+map_eq_one_iff (algebra_map _ _) (algebra_map_left_inverse _).injective
 
 variables {M}
 

src/linear_algebra/tensor_algebra.lean

@@ -166,10 +166,10 @@ lemma algebra_map_left_inverse :
 (algebra_map_left_inverse M).injective.eq_iff
 
 @[simp] lemma algebra_map_eq_zero_iff (x : R) : algebra_map R (tensor_algebra R M) x = 0 ↔ x = 0 :=
-by rw [←algebra_map_inj M x 0, ring_hom.map_zero]
+map_eq_zero_iff (algebra_map _ _) (algebra_map_left_inverse _).injective
 
 @[simp] lemma algebra_map_eq_one_iff (x : R) : algebra_map R (tensor_algebra R M) x = 1 ↔ x = 1 :=
-by rw [←algebra_map_inj M x 1, ring_hom.map_one]
+map_eq_one_iff (algebra_map _ _) (algebra_map_left_inverse _).injective
 
 variables {M}