feat(Algebra): SemimoduleCat, category of modules over semiring (#31023)

+ Introduce SemimoduleCat, the category of semimodules (mathlib's Module) over a Semiring. The new file ModuleCat/Semi.lean is copied from ModuleCat/Basic.lean. The additive/linear instances would require #28826.

Author: alreadydone

Mathlib.lean

@@ -175,6 +175,7 @@ import Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
 import Mathlib.Algebra.Category.ModuleCat.Products
 import Mathlib.Algebra.Category.ModuleCat.Projective
 import Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
+import Mathlib.Algebra.Category.ModuleCat.Semi
 import Mathlib.Algebra.Category.ModuleCat.Sheaf
 import Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian
 import Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings

Mathlib/Algebra/Category/ModuleCat/Basic.lean

@@ -3,10 +3,8 @@ Copyright (c) 2019 Robert A. Spencer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert A. Spencer, Markus Himmel
 -/
+import Mathlib.Algebra.Category.ModuleCat.Semi
 import Mathlib.Algebra.Category.Grp.Preadditive
-import Mathlib.Algebra.Module.Equiv.Basic
-import Mathlib.Algebra.Module.PUnit
-import Mathlib.CategoryTheory.Conj
 import Mathlib.CategoryTheory.Linear.Basic
 import Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
 
@@ -184,6 +182,20 @@ def homEquiv {M N : ModuleCat.{v} R} : (M ⟶ N) ≃ (M →ₗ[R] N) where
   toFun := Hom.hom
   invFun := ofHom
 
+/-- The categorical equivalence between `ModuleCat` and `SemimoduleCat`.
+
+In the inverse direction, data (such as the negation operation) is created which may lead to
+diamonds when applied to semi-modules that already have an existing additive group structure. -/
+def equivalenceSemimoduleCat : ModuleCat.{v} R ≌ SemimoduleCat.{v} R where
+  functor :=
+  { obj M := .of R M
+    map f := SemimoduleCat.ofHom f.hom' }
+  inverse := letI := Module.addCommMonoidToAddCommGroup
+  { obj M := of R M
+    map {M N} f := ofHom f.hom }
+  unitIso := NatIso.ofComponents fun _ ↦ { hom := ⟨.id⟩, inv := ⟨.id⟩ }
+  counitIso := NatIso.ofComponents fun _ ↦ { hom := ⟨.id⟩, inv := ⟨.id⟩ }
+
 end
 
 /- Not a `@[simp]` lemma since it will rewrite the (co)domain of maps and cause