chore(Algebra/Module): further split Defs.lean (#18995)

The goal is that we can define `Module` without depending on `Units`.
The following moves out of `Defs.lean` are included in this PR:
 * Module structure over Nat and Int go to `Module/NatInt.lean`
 * Composition with `RingHom`s goes to `Module/RingHom.lean`
 * Results about units go to `Module/Basic.lean`

Author: Vierkantor

Mathlib.lean

@@ -520,6 +520,7 @@ import Mathlib.Algebra.Module.LocalizedModule.Int
 import Mathlib.Algebra.Module.LocalizedModule.IsLocalization
 import Mathlib.Algebra.Module.LocalizedModule.Submodule
 import Mathlib.Algebra.Module.MinimalAxioms
+import Mathlib.Algebra.Module.NatInt
 import Mathlib.Algebra.Module.Opposite
 import Mathlib.Algebra.Module.PID
 import Mathlib.Algebra.Module.Pi
@@ -533,6 +534,7 @@ import Mathlib.Algebra.Module.Presentation.Tautological
 import Mathlib.Algebra.Module.Prod
 import Mathlib.Algebra.Module.Projective
 import Mathlib.Algebra.Module.Rat
+import Mathlib.Algebra.Module.RingHom
 import Mathlib.Algebra.Module.SnakeLemma
 import Mathlib.Algebra.Module.Submodule.Basic
 import Mathlib.Algebra.Module.Submodule.Bilinear

Mathlib/Algebra/AddConstMap/Basic.lean

@@ -5,7 +5,7 @@ Authors: Yury Kudryashov
 -/
 import Mathlib.Algebra.Group.Action.Pi
 import Mathlib.Algebra.GroupPower.IterateHom
-import Mathlib.Algebra.Module.Defs
+import Mathlib.Algebra.Module.NatInt
 import Mathlib.Algebra.Order.Archimedean.Basic
 import Mathlib.Algebra.Order.Group.Instances
 import Mathlib.Logic.Function.Iterate

Mathlib/Algebra/CharZero/Quotient.lean

@@ -5,7 +5,7 @@ Authors: Eric Wieser
 -/
 import Mathlib.Algebra.Field.Basic
 import Mathlib.Algebra.Order.Group.Unbundled.Int
-import Mathlib.Algebra.Module.Defs
+import Mathlib.Algebra.Module.NatInt
 import Mathlib.GroupTheory.QuotientGroup.Defs
 import Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
 

Mathlib/Algebra/Group/Submonoid/Pointwise.lean

@@ -5,6 +5,7 @@ Authors: Eric Wieser
 -/
 import Mathlib.Algebra.Group.Hom.End
 import Mathlib.Algebra.Group.Submonoid.Membership
+import Mathlib.Algebra.GroupWithZero.Action.End
 import Mathlib.Algebra.Order.BigOperators.Group.List
 import Mathlib.Data.Set.Pointwise.SMul
 import Mathlib.Order.WellFoundedSet

Mathlib/Algebra/Homology/TotalComplex.lean

@@ -6,6 +6,7 @@ Authors: Joël Riou
 import Mathlib.CategoryTheory.Linear.Basic
 import Mathlib.Algebra.Homology.ComplexShapeSigns
 import Mathlib.Algebra.Homology.HomologicalBicomplex
+import Mathlib.Algebra.Module.Basic
 
 /-!
 # The total complex of a bicomplex

Mathlib/Algebra/Module/Basic.lean

@@ -6,7 +6,8 @@ Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro
 import Mathlib.Algebra.Field.Basic
 import Mathlib.Algebra.Group.Action.Pi
 import Mathlib.Algebra.Group.Indicator
-import Mathlib.Algebra.Module.Defs
+import Mathlib.Algebra.GroupWithZero.Action.Units
+import Mathlib.Algebra.Module.NatInt
 import Mathlib.Algebra.NoZeroSMulDivisors.Defs
 
 /-!
@@ -23,6 +24,11 @@ universe u v
 
 variable {α R M M₂ : Type*}
 
+@[simp]
+theorem Units.neg_smul [Ring R] [AddCommGroup M] [Module R M] (u : Rˣ) (x : M) :
+    -u • x = -(u • x) := by
+  rw [Units.smul_def, Units.val_neg, _root_.neg_smul, Units.smul_def]
+
 @[simp]
 theorem invOf_two_smul_add_invOf_two_smul (R) [Semiring R] [AddCommMonoid M] [Module R M]
     [Invertible (2 : R)] (x : M) :

Mathlib/Algebra/Module/Defs.lean

@@ -3,10 +3,11 @@ Copyright (c) 2015 Nathaniel Thomas. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro
 -/
-import Mathlib.Algebra.GroupWithZero.Action.End
-import Mathlib.Algebra.GroupWithZero.Action.Units
+import Mathlib.Algebra.Group.Action.End
+import Mathlib.Algebra.Group.Equiv.Basic
+import Mathlib.Algebra.GroupWithZero.Action.Defs
+import Mathlib.Algebra.Ring.Defs
 import Mathlib.Algebra.SMulWithZero
-import Mathlib.Data.Int.Cast.Lemmas
 
 /-!
 # Modules over a ring
@@ -39,7 +40,9 @@ assert_not_exists Field
 assert_not_exists Invertible
 assert_not_exists Multiset
 assert_not_exists Pi.single_smul₀
+assert_not_exists RingHom
 assert_not_exists Set.indicator
+assert_not_exists Units
 
 open Function Set
 
@@ -72,14 +75,6 @@ instance (priority := 100) Module.toMulActionWithZero
     smul_zero := smul_zero
     zero_smul := Module.zero_smul }
 
-instance AddCommGroup.toNatModule : Module ℕ M where
-  one_smul := one_nsmul
-  mul_smul m n a := mul_nsmul' a m n
-  smul_add n a b := nsmul_add a b n
-  smul_zero := nsmul_zero
-  zero_smul := zero_nsmul
-  add_smul r s x := add_nsmul x r s
-
 theorem add_smul : (r + s) • x = r • x + s • x :=
   Module.add_smul r s x
 
@@ -111,31 +106,7 @@ protected abbrev Function.Surjective.module [AddCommMonoid M₂] [SMul R M₂] (
       rcases hf x with ⟨x, rfl⟩
       rw [← f.map_zero, ← smul, zero_smul] }
 
-/-- Push forward the action of `R` on `M` along a compatible surjective map `f : R →+* S`.
-
-See also `Function.Surjective.mulActionLeft` and `Function.Surjective.distribMulActionLeft`.
--/
-abbrev Function.Surjective.moduleLeft {R S M : Type*} [Semiring R] [AddCommMonoid M] [Module R M]
-    [Semiring S] [SMul S M] (f : R →+* S) (hf : Function.Surjective f)
-    (hsmul : ∀ (c) (x : M), f c • x = c • x) : Module S M :=
-  { hf.distribMulActionLeft f.toMonoidHom hsmul with
-    zero_smul := fun x => by rw [← f.map_zero, hsmul, zero_smul]
-    add_smul := hf.forall₂.mpr fun a b x => by simp only [← f.map_add, hsmul, add_smul] }
-
-variable {R} (M)
-
-/-- Compose a `Module` with a `RingHom`, with action `f s • m`.
-
-See note [reducible non-instances]. -/
-abbrev Module.compHom [Semiring S] (f : S →+* R) : Module S M :=
-  { MulActionWithZero.compHom M f.toMonoidWithZeroHom, DistribMulAction.compHom M (f : S →* R) with
-    -- Porting note: the `show f (r + s) • x = f r • x + f s • x` wasn't needed in mathlib3.
-    -- Somehow, now that `SMul` is heterogeneous, it can't unfold earlier fields of a definition for
-    -- use in later fields.  See
-    -- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Heterogeneous.20scalar.20multiplication
-    add_smul := fun r s x => show f (r + s) • x = f r • x + f s • x by simp [add_smul] }
-
-variable {M}
+variable {R}
 
 theorem Module.eq_zero_of_zero_eq_one (zero_eq_one : (0 : R) = 1) : x = 0 := by
   rw [← one_smul R x, ← zero_eq_one, zero_smul]
@@ -146,20 +117,9 @@ theorem smul_add_one_sub_smul {R : Type*} [Ring R] [Module R M] {r : R} {m : M}
 
 end AddCommMonoid
 
-
 section AddCommGroup
 
-variable (R M) [Semiring R] [AddCommGroup M]
-
-instance AddCommGroup.toIntModule : Module ℤ M where
-  one_smul := one_zsmul
-  mul_smul m n a := mul_zsmul a m n
-  smul_add n a b := zsmul_add a b n
-  smul_zero := zsmul_zero
-  zero_smul := zero_zsmul
-  add_smul r s x := add_zsmul x r s
-
-variable {R M}
+variable [Semiring R] [AddCommGroup M]
 
 theorem Convex.combo_eq_smul_sub_add [Module R M] {x y : M} {a b : R} (h : a + b = 1) :
     a • x + b • y = b • (y - x) + x :=
@@ -187,10 +147,6 @@ theorem neg_smul : -r • x = -(r • x) :=
 
 theorem neg_smul_neg : -r • -x = r • x := by rw [neg_smul, smul_neg, neg_neg]
 
-@[simp]
-theorem Units.neg_smul (u : Rˣ) (x : M) : -u • x = -(u • x) := by
-  rw [Units.smul_def, Units.val_neg, _root_.neg_smul, Units.smul_def]
-
 variable (R)
 
 theorem neg_one_smul (x : M) : (-1 : R) • x = -x := by simp
@@ -202,26 +158,6 @@ theorem sub_smul (r s : R) (y : M) : (r - s) • y = r • y - s • y := by
 
 end Module
 
-variable (R)
-
-/-- An `AddCommMonoid` that is a `Module` over a `Ring` carries a natural `AddCommGroup`
-structure.
-See note [reducible non-instances]. -/
-abbrev Module.addCommMonoidToAddCommGroup
-    [Ring R] [AddCommMonoid M] [Module R M] : AddCommGroup M :=
-  { (inferInstance : AddCommMonoid M) with
-    neg := fun a => (-1 : R) • a
-    neg_add_cancel := fun a =>
-      show (-1 : R) • a + a = 0 by
-        nth_rw 2 [← one_smul R a]
-        rw [← add_smul, neg_add_cancel, zero_smul]
-    zsmul := fun z a => (z : R) • a
-    zsmul_zero' := fun a => by simpa only [Int.cast_zero] using zero_smul R a
-    zsmul_succ' := fun z a => by simp [add_comm, add_smul]
-    zsmul_neg' := fun z a => by simp [← smul_assoc, neg_one_smul] }
-
-variable {R}
-
 /-- A module over a `Subsingleton` semiring is a `Subsingleton`. We cannot register this
 as an instance because Lean has no way to guess `R`. -/
 protected theorem Module.subsingleton (R M : Type*) [Semiring R] [Subsingleton R] [AddCommMonoid M]
@@ -242,87 +178,3 @@ instance (priority := 910) Semiring.toModule [Semiring R] : Module R R where
 
 instance [NonUnitalNonAssocSemiring R] : DistribSMul R R where
   smul_add := left_distrib
-
-/-- A ring homomorphism `f : R →+* M` defines a module structure by `r • x = f r * x`. -/
-def RingHom.toModule [Semiring R] [Semiring S] (f : R →+* S) : Module R S :=
-  Module.compHom S f
-
-/-- If the module action of `R` on `S` is compatible with multiplication on `S`, then
-`fun x ↦ x • 1` is a ring homomorphism from `R` to `S`.
-
-This is the `RingHom` version of `MonoidHom.smulOneHom`.
-
-When `R` is commutative, usually `algebraMap` should be preferred. -/
-@[simps!] def RingHom.smulOneHom
-    [Semiring R] [NonAssocSemiring S] [Module R S] [IsScalarTower R S S] : R →+* S where
-  __ := MonoidHom.smulOneHom
-  map_zero' := zero_smul R 1
-  map_add' := (add_smul · · 1)
-
-/-- A homomorphism between semirings R and S can be equivalently specified by a R-module
-structure on S such that S/S/R is a scalar tower. -/
-def ringHomEquivModuleIsScalarTower [Semiring R] [Semiring S] :
-    (R →+* S) ≃ {_inst : Module R S // IsScalarTower R S S} where
-  toFun f := ⟨Module.compHom S f, SMul.comp.isScalarTower _⟩
-  invFun := fun ⟨_, _⟩ ↦ RingHom.smulOneHom
-  left_inv f := RingHom.ext fun r ↦ mul_one (f r)
-  right_inv := fun ⟨_, _⟩ ↦ Subtype.ext <| Module.ext <| funext₂ <| smul_one_smul S
-
-section AddCommMonoid
-
-variable [Semiring R] [AddCommMonoid M] [Module R M]
-
-section
-
-variable (R)
-
-/-- `nsmul` is equal to any other module structure via a cast. -/
-lemma Nat.cast_smul_eq_nsmul (n : ℕ) (b : M) : (n : R) • b = n • b := by
-  induction n with
-  | zero => rw [Nat.cast_zero, zero_smul, zero_smul]
-  | succ n ih => rw [Nat.cast_succ, add_smul, add_smul, one_smul, ih, one_smul]
-
-/-- `nsmul` is equal to any other module structure via a cast. -/
--- See note [no_index around OfNat.ofNat]
-lemma ofNat_smul_eq_nsmul (n : ℕ) [n.AtLeastTwo] (b : M) :
-    (no_index (OfNat.ofNat n) : R) • b = OfNat.ofNat n • b := Nat.cast_smul_eq_nsmul ..
-
-/-- `nsmul` is equal to any other module structure via a cast. -/
-@[deprecated Nat.cast_smul_eq_nsmul (since := "2024-07-23")]
-lemma nsmul_eq_smul_cast (n : ℕ) (b : M) : n • b = (n : R) • b := (Nat.cast_smul_eq_nsmul ..).symm
-
-end
-
-/-- Convert back any exotic `ℕ`-smul to the canonical instance. This should not be needed since in
-mathlib all `AddCommMonoid`s should normally have exactly one `ℕ`-module structure by design.
--/
-theorem nat_smul_eq_nsmul (h : Module ℕ M) (n : ℕ) (x : M) : @SMul.smul ℕ M h.toSMul n x = n • x :=
-  Nat.cast_smul_eq_nsmul ..
-
-/-- All `ℕ`-module structures are equal. Not an instance since in mathlib all `AddCommMonoid`
-should normally have exactly one `ℕ`-module structure by design. -/
-def AddCommMonoid.uniqueNatModule : Unique (Module ℕ M) where
-  default := by infer_instance
-  uniq P := (Module.ext' P _) fun n => by convert nat_smul_eq_nsmul P n
-
-instance AddCommMonoid.nat_isScalarTower : IsScalarTower ℕ R M where
-  smul_assoc n x y := by
-    induction n with
-    | zero => simp only [zero_smul]
-    | succ n ih => simp only [add_smul, one_smul, ih]
-
-end AddCommMonoid
-
-theorem map_natCast_smul [AddCommMonoid M] [AddCommMonoid M₂] {F : Type*} [FunLike F M M₂]
-    [AddMonoidHomClass F M M₂] (f : F) (R S : Type*) [Semiring R] [Semiring S] [Module R M]
-    [Module S M₂] (x : ℕ) (a : M) : f ((x : R) • a) = (x : S) • f a := by
-  simp only [Nat.cast_smul_eq_nsmul, AddMonoidHom.map_nsmul, map_nsmul]
-
-theorem Nat.smul_one_eq_cast {R : Type*} [NonAssocSemiring R] (m : ℕ) : m • (1 : R) = ↑m := by
-  rw [nsmul_eq_mul, mul_one]
-
-theorem Int.smul_one_eq_cast {R : Type*} [NonAssocRing R] (m : ℤ) : m • (1 : R) = ↑m := by
-  rw [zsmul_eq_mul, mul_one]
-
-@[deprecated (since := "2024-05-03")] alias Nat.smul_one_eq_coe := Nat.smul_one_eq_cast
-@[deprecated (since := "2024-05-03")] alias Int.smul_one_eq_coe := Int.smul_one_eq_cast

Mathlib/Algebra/Module/End.lean

@@ -5,6 +5,7 @@ Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro
 -/
 import Mathlib.Algebra.Group.Hom.End
 import Mathlib.Algebra.Module.Defs
+import Mathlib.Algebra.Module.NatInt
 
 /-!
 # Module structure and endomorphisms

Mathlib/Algebra/Module/Hom.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
 import Mathlib.Algebra.Group.Hom.Instances
+import Mathlib.Algebra.GroupWithZero.Action.End
 import Mathlib.Algebra.Module.End
 import Mathlib.Algebra.Ring.Opposite
 import Mathlib.GroupTheory.GroupAction.DomAct.Basic

Mathlib/Algebra/Module/LinearMap/Defs.lean

@@ -5,6 +5,8 @@ Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro, Anne
   Frédéric Dupuis, Heather Macbeth
 -/
 import Mathlib.Algebra.Group.Hom.Instances
+import Mathlib.Algebra.Module.NatInt
+import Mathlib.Algebra.Module.RingHom
 import Mathlib.Algebra.Ring.CompTypeclasses
 import Mathlib.GroupTheory.GroupAction.Hom