feat(ring_theory/algebra, algebra/module): Add add_comm_monoid_to_add…

…_comm_group and semiring_to_ring (#4252)

src/algebra/module/basic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro
 -/
 import group_theory.group_action
+import tactic.nth_rewrite
 
 /-!
 # Modules over a ring
@@ -107,6 +108,19 @@ lemma finset.sum_smul {f : ι → R} {s : finset ι} {x : M} :
 
 end add_comm_monoid
 
+variables (R)
+
+/-- An `add_comm_monoid` that is a `semimodule` over a `ring` carries a natural `add_comm_group` structure. -/
+def semimodule.add_comm_monoid_to_add_comm_group [ring R] [add_comm_monoid M] [semimodule R M] :
+  add_comm_group M :=
+{ neg          := λ a, (-1 : R) • a,
+  add_left_neg := λ a, by {
+    nth_rewrite 1 ← one_smul _ a,
+    rw [← add_smul, add_left_neg, zero_smul], },
+  ..(infer_instance : add_comm_monoid M), }
+
+variables {R}
+
 section add_comm_group
 
 variables (R M) [semiring R] [add_comm_group M]

src/linear_algebra/tensor_product.lean

@@ -594,14 +594,7 @@ variables [module R M] [module R N] [module R P] [module R Q] [module R S]
 open_locale tensor_product
 open linear_map
 
-instance : add_comm_group (M ⊗[R] N) :=
-{ neg := tensor_product.lift $ (mk R M N).comp $ (-1 : R) • linear_map.id,
-  add_left_neg := λ x,
-    suffices (tensor_product.lift $ (mk R M N).comp $ (-1 : R) • linear_map.id) + linear_map.id = 0,
-      from linear_map.ext_iff.1 this x,
-    ext $ λ m n, by rw [add_apply, lift.tmul, comp_apply, mk_apply, smul_apply, neg_one_smul,
-        id_apply, id_apply, ← add_tmul, neg_add_self, zero_tmul, zero_apply],
-  .. tensor_product.add_comm_monoid M N }
+instance : add_comm_group (M ⊗[R] N) := semimodule.add_comm_monoid_to_add_comm_group R
 
 lemma neg_tmul (m : M) (n : N) : (-m) ⊗ₜ n = -(m ⊗ₜ[R] n) := (mk R M N).map_neg₂ _ _
 lemma tmul_neg (m : M) (n : N) : m ⊗ₜ (-n) = -(m ⊗ₜ[R] n) := (mk R M N _).map_neg _

src/ring_theory/algebra.lean

@@ -286,13 +286,22 @@ instance linear_map.semimodule' (R : Type u) [comm_semiring R]
 end semiring
 
 section ring
-variables [comm_ring R] [comm_ring S] [ring A] [algebra R A]
+variables [comm_ring R]
 
-lemma mul_sub_algebra_map_commutes (x : A) (r : R) :
+variables (R)
+
+/-- A `semiring` that is an `algebra` over a commutative ring carries a natural `ring` structure. -/
+def semiring_to_ring [semiring A] [algebra R A] : ring A := {
+  ..semimodule.add_comm_monoid_to_add_comm_group R,
+  ..(infer_instance : semiring A) }
+
+variables {R}
+
+lemma mul_sub_algebra_map_commutes [ring A] [algebra R A] (x : A) (r : R) :
   x * (x - algebra_map R A r) = (x - algebra_map R A r) * x :=
 by rw [mul_sub, ←commutes, sub_mul]
 
-lemma mul_sub_algebra_map_pow_commutes (x : A) (r : R) (n : ℕ) :
+lemma mul_sub_algebra_map_pow_commutes [ring A] [algebra R A] (x : A) (r : R) (n : ℕ) :
   x * (x - algebra_map R A r) ^ n = (x - algebra_map R A r) ^ n * x :=
 begin
   induction n with n ih,