feat: API about Small modules (#5769)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: kim-em

Mathlib.lean

@@ -2237,6 +2237,7 @@ import Mathlib.Logic.Relator
 import Mathlib.Logic.Small.Basic
 import Mathlib.Logic.Small.Group
 import Mathlib.Logic.Small.List
+import Mathlib.Logic.Small.Module
 import Mathlib.Logic.Small.Ring
 import Mathlib.Logic.Unique
 import Mathlib.Logic.UnivLE

Mathlib/Logic/Small/Module.lean

@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2021 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import Mathlib.Logic.Small.Group
+import Mathlib.Logic.Small.Ring
+
+/-!
+# Transfer module and algebra structures from `α` to `Shrink α`.
+-/
+
+noncomputable section
+
+instance [Semiring α] [AddCommMonoid β] [Module α β] [Small β] : Module α (Shrink β) :=
+  (equivShrink _).symm.module α
+
+/-- A small module is linearly equivalent to its small model. -/
+def linearEquivShrink (α β) [Semiring α] [AddCommMonoid β] [Module α β] [Small β] :
+    β ≃ₗ[α] Shrink β :=
+  ((equivShrink β).symm.linearEquiv α).symm
+
+instance [CommSemiring α] [Semiring β] [Algebra α β] [Small β] : Algebra α (Shrink β) :=
+  (equivShrink _).symm.algebra α
+
+/-- A small algebra is algebra equivalent to its small model. -/
+def algEquivShrink (α β) [CommSemiring α] [Semiring β] [Algebra α β] [Small β] :
+    β ≃ₐ[α] Shrink β :=
+  ((equivShrink β).symm.algEquiv α).symm