chore(Algebra): replace NoZeroSMulDivisors with Module.IsTorsionFree, losing generality (#33873)

`NoZeroSMulDivisors R M` is mathematically wrong when `R` isn't a domain, so we replace it with the better definition `Module.IsTorsionFree R M` whenever they are equivalent.

This PR continues #30563, replacing `NoZeroSMulDivisors R M` with `Module.IsTorsionFree R M` even when this loses generality.

Author: YaelDillies

Mathlib/Algebra/Algebra/Basic.lean

@@ -31,7 +31,7 @@ open Function Module
 
 namespace Algebra
 
-variable {R : Type u} {A : Type w}
+variable {R A M : Type*}
 
 section Semiring
 
@@ -368,26 +368,27 @@ namespace NoZeroSMulDivisors
 
 -- see Note [lower instance priority]
 instance (priority := 100) instOfFaithfulSMul {R A : Type*}
-    [CommSemiring R] [Semiring A] [Algebra R A] [NoZeroDivisors A] [FaithfulSMul R A] :
-    NoZeroSMulDivisors R A :=
-  ⟨fun hcx => (mul_eq_zero.mp ((Algebra.smul_def _ _).symm.trans hcx)).imp_left
-    (map_eq_zero_iff (algebraMap R A) <| FaithfulSMul.algebraMap_injective R A).mp⟩
+    [CommSemiring R] [Nontrivial R] [Ring A] [Algebra R A] [NoZeroDivisors A] [FaithfulSMul R A] :
+    IsTorsionFree R A where
+  isSMulRegular r hr a b hab := by
+    rw [← sub_eq_zero, ← smul_sub] at hab
+    simpa [Algebra.smul_def, FaithfulSMul.algebraMap_eq_zero_iff, sub_eq_zero, hr.ne_zero] using hab
 
-variable {R A : Type*} [CommRing R] [Ring A] [Algebra R A]
+variable {R A : Type*} [CommRing R] [IsDomain R] [Ring A] [Algebra R A]
 
-instance [Nontrivial A] [NoZeroSMulDivisors R A] : FaithfulSMul R A where
+instance [Nontrivial A] [IsTorsionFree R A] : FaithfulSMul R A where
   eq_of_smul_eq_smul {r₁ r₂} h := by
     specialize h 1
     rw [← sub_eq_zero, ← sub_smul, smul_eq_zero, sub_eq_zero] at h
     exact h.resolve_right one_ne_zero
 
-theorem iff_faithfulSMul [IsDomain A] : NoZeroSMulDivisors R A ↔ FaithfulSMul R A :=
-  ⟨fun _ ↦ inferInstance, fun _ ↦ inferInstance⟩
+lemma iff_faithfulSMul [IsDomain A] : IsTorsionFree R A ↔ FaithfulSMul R A where
+  mp _ := inferInstance
+  mpr _ := inferInstance
 
 theorem iff_algebraMap_injective [IsDomain A] :
-    NoZeroSMulDivisors R A ↔ Injective (algebraMap R A) := by
-  rw [iff_faithfulSMul]
-  exact faithfulSMul_iff_algebraMap_injective R A
+    IsTorsionFree R A ↔ Injective (algebraMap R A) := by
+  rw [iff_faithfulSMul, faithfulSMul_iff_algebraMap_injective]
 
 end NoZeroSMulDivisors
 
@@ -408,15 +409,6 @@ lemma isSMulRegular_algebraMap_iff {r : R} :
     IsSMulRegular M (algebraMap R A r) ↔ IsSMulRegular M r :=
   (Equiv.refl M).isSMulRegular_congr (algebraMap_smul A r)
 
-/-- If `M` is `A`-torsion free and `algebraMap R A` is injective, `M` is also `R`-torsion free. -/
-theorem NoZeroSMulDivisors.trans_faithfulSMul (R A M : Type*) [CommSemiring R] [Semiring A]
-    [Algebra R A] [FaithfulSMul R A] [AddCommMonoid M] [Module R M] [Module A M]
-    [IsScalarTower R A M] [NoZeroSMulDivisors A M] : NoZeroSMulDivisors R M where
-  eq_zero_or_eq_zero_of_smul_eq_zero hx := by
-    rw [← algebraMap_smul (A := A)] at hx
-    simpa only [map_eq_zero_iff _ <| FaithfulSMul.algebraMap_injective R A] using
-      eq_zero_or_eq_zero_of_smul_eq_zero hx
-
 variable {A}
 
 -- see Note [lower instance priority]

Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

@@ -287,10 +287,8 @@ instance instSMulCommClass' [Semiring R'] [SMul R' R] [Module R' A] [IsScalarTow
 instance instSMulCommClass [SMulCommClass R A A] : SMulCommClass R S S where
   smul_comm r x y := Subtype.ext <| smul_comm r (x : A) (y : A)
 
-instance noZeroSMulDivisors_bot [NoZeroSMulDivisors R A] : NoZeroSMulDivisors R S :=
-  ⟨fun {c x} h =>
-    have : c = 0 ∨ (x : A) = 0 := eq_zero_or_eq_zero_of_smul_eq_zero (congr_arg ((↑) : S → A) h)
-    this.imp_right Subtype.ext⟩
+instance instIsTorsionFree [Module.IsTorsionFree R A] : Module.IsTorsionFree R S :=
+  S.toSubmodule.instIsTorsionFree
 
 end
 

Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

@@ -336,11 +336,6 @@ end
 instance instIsTorsionFree [IsTorsionFree R A] : IsTorsionFree R S :=
   S.toSubmodule.instIsTorsionFree
 
-instance noZeroSMulDivisors_bot [NoZeroSMulDivisors R A] : NoZeroSMulDivisors R S :=
-  ⟨fun {c} {x : S} h =>
-    have : c = 0 ∨ (x : A) = 0 := eq_zero_or_eq_zero_of_smul_eq_zero (congr_arg Subtype.val h)
-    this.imp_right (@Subtype.ext_iff _ _ x 0).mpr⟩
-
 protected theorem coe_add (x y : S) : (↑(x + y) : A) = ↑x + ↑y := rfl
 
 protected theorem coe_mul (x y : S) : (↑(x * y) : A) = ↑x * ↑y := rfl
@@ -881,11 +876,6 @@ instance instIsTorsionFree' [IsDomain A] (S : Subalgebra R A) : IsTorsionFree S
   .comap Subtype.val (fun r hr ↦ by simpa [isRegular_iff_ne_zero] using hr.ne_zero)
     (by simp [smul_def])
 
-instance noZeroSMulDivisors_top [NoZeroDivisors A] (S : Subalgebra R A) : NoZeroSMulDivisors S A :=
-  ⟨fun {c} x h =>
-    have : (c : A) = 0 ∨ x = 0 := eq_zero_or_eq_zero_of_mul_eq_zero h
-    this.imp_left (@Subtype.ext_iff _ _ c 0).mpr⟩
-
 end Actions
 
 section Center

Mathlib/Algebra/Algebra/Tower.lean

@@ -386,13 +386,13 @@ section Ring
 
 namespace Algebra
 
-variable [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B]
+variable [CommSemiring R] [Semiring A] [IsDomain A] [Semiring B] [Algebra R A] [Algebra R B]
 variable [AddCommGroup M] [Module R M] [Module A M] [Module B M]
 variable [IsScalarTower R A M] [IsScalarTower R B M] [SMulCommClass A B M]
 
-theorem lsmul_injective [NoZeroSMulDivisors A M] {x : A} (hx : x ≠ 0) :
+theorem lsmul_injective [Module.IsTorsionFree A M] {x : A} (hx : x ≠ 0) :
     Function.Injective (lsmul R B M x) :=
-  NoZeroSMulDivisors.smul_right_injective M hx
+  smul_right_injective M hx
 
 end Algebra
 

Mathlib/Algebra/BigOperators/Finprod.lean

@@ -314,14 +314,13 @@ theorem finsum_smul {R M : Type*} [Ring R] [IsDomain R] [AddCommGroup M] [Module
   · simp
   · exact ((smulAddHom R M).flip x).map_finsum_of_injective (smul_left_injective R hx) _
 
-/-- The `NoZeroSMulDivisors` makes sure that the result holds even when the support of `f` is
+/-- The torsion-free assumption makes sure that the result holds even when the support of `f` is
 infinite. For a more usual version assuming `(support f).Finite` instead, see `smul_finsum'`. -/
-theorem smul_finsum {R M : Type*} [Semiring R] [AddCommGroup M] [Module R M]
-    [NoZeroSMulDivisors R M] (c : R) (f : ι → M) : (c • ∑ᶠ i, f i) = ∑ᶠ i, c • f i := by
+theorem smul_finsum {R M : Type*} [Semiring R] [IsDomain R] [AddCommGroup M] [Module R M]
+    [Module.IsTorsionFree R M] (c : R) (f : ι → M) : c • ∑ᶠ i, f i = ∑ᶠ i, c • f i := by
   rcases eq_or_ne c 0 with (rfl | hc)
   · simp
-  · exact (smulAddHom R M c).map_finsum_of_injective
-      (NoZeroSMulDivisors.smul_right_injective M hc) _
+  · exact (smulAddHom R M c).map_finsum_of_injective (smul_right_injective M hc) _
 
 @[to_additive]
 theorem finprod_inv_distrib [DivisionCommMonoid G] (f : α → G) : (∏ᶠ x, (f x)⁻¹) = (∏ᶠ x, f x)⁻¹ :=

Mathlib/Algebra/Central/Basic.lean

@@ -6,6 +6,7 @@ Authors: Kevin Buzzard, Jujian Zhang, Yunzhou Xie
 module
 
 public import Mathlib.Algebra.Central.Defs
+public import Mathlib.Algebra.Module.Torsion.Field
 
 import Mathlib.Algebra.Module.Torsion.Field
 

Mathlib/Algebra/GroupWithZero/Action/Pointwise/Finset.lean

@@ -54,15 +54,6 @@ scoped[Pointwise] attribute [instance] Finset.smulZeroClass Finset.distribSMul
 instance [DecidableEq α] [Zero α] [Mul α] [NoZeroDivisors α] : NoZeroDivisors (Finset α) :=
   Function.Injective.noZeroDivisors _ coe_injective coe_zero coe_mul
 
-instance noZeroSMulDivisors [Zero α] [Zero β] [SMul α β] [NoZeroSMulDivisors α β] :
-    NoZeroSMulDivisors (Finset α) (Finset β) where
-  eq_zero_or_eq_zero_of_smul_eq_zero {s t} := by
-    exact_mod_cast eq_zero_or_eq_zero_of_smul_eq_zero (c := (s : Set α)) (x := (t : Set β))
-
-instance noZeroSMulDivisors_finset [Zero α] [Zero β] [SMul α β] [NoZeroSMulDivisors α β] :
-    NoZeroSMulDivisors α (Finset β) :=
-  Function.Injective.noZeroSMulDivisors _ coe_injective coe_zero coe_smul_finset
-
 section SMulZeroClass
 variable [Zero β] [SMulZeroClass α β] {s : Finset α} {t : Finset β} {a : α}
 
@@ -74,11 +65,6 @@ lemma Nonempty.smul_zero (hs : s.Nonempty) : s • (0 : Finset β) = 0 :=
 lemma zero_mem_smul_finset (h : (0 : β) ∈ t) : (0 : β) ∈ a • t :=
   mem_smul_finset.2 ⟨0, h, smul_zero _⟩
 
-variable [Zero α] [NoZeroSMulDivisors α β]
-
-lemma zero_mem_smul_finset_iff (ha : a ≠ 0) : (0 : β) ∈ a • t ↔ (0 : β) ∈ t := by
-  rw [← mem_coe, coe_smul_finset, Set.zero_mem_smul_set_iff ha, mem_coe]
-
 end SMulZeroClass
 
 section SMulWithZero
@@ -101,12 +87,6 @@ lemma Nonempty.zero_smul (ht : t.Nonempty) : (0 : Finset α) • t = 0 :=
 lemma zero_smul_finset_subset (s : Finset β) : (0 : α) • s ⊆ 0 :=
   image_subset_iff.2 fun x _ ↦ mem_zero.2 <| zero_smul α x
 
-variable [NoZeroSMulDivisors α β]
-
-lemma zero_mem_smul_iff :
-    (0 : β) ∈ s • t ↔ (0 : α) ∈ s ∧ t.Nonempty ∨ (0 : β) ∈ t ∧ s.Nonempty := by
-  rw [← mem_coe, coe_smul, Set.zero_mem_smul_iff]; rfl
-
 end SMulWithZero
 
 section GroupWithZero

Mathlib/Algebra/GroupWithZero/Action/Pointwise/Set.lean

@@ -9,7 +9,6 @@ public import Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
 public import Mathlib.Algebra.GroupWithZero.Action.Basic
 public import Mathlib.Algebra.GroupWithZero.Action.Units
 public import Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic
-public import Mathlib.Algebra.NoZeroSMulDivisors.Defs
 
 /-!
 # Pointwise operations of sets in a group with zero
@@ -59,13 +58,6 @@ lemma Nonempty.smul_zero (hs : s.Nonempty) : s • (0 : Set β) = 0 :=
 
 lemma zero_mem_smul_set (h : (0 : β) ∈ t) : (0 : β) ∈ a • t := ⟨0, h, smul_zero _⟩
 
-variable [Zero α] [NoZeroSMulDivisors α β]
-
-lemma zero_mem_smul_set_iff (ha : a ≠ 0) : (0 : β) ∈ a • t ↔ (0 : β) ∈ t := by
-  refine ⟨?_, zero_mem_smul_set⟩
-  rintro ⟨b, hb, h⟩
-  rwa [(eq_zero_or_eq_zero_of_smul_eq_zero h).resolve_left ha] at hb
-
 end SMulZeroClass
 section SMulWithZero
 
@@ -91,19 +83,6 @@ lemma zero_smul_set_subset (s : Set β) : (0 : α) • s ⊆ 0 :=
 lemma subsingleton_zero_smul_set (s : Set β) : ((0 : α) • s).Subsingleton :=
   subsingleton_singleton.anti <| zero_smul_set_subset s
 
-variable [NoZeroSMulDivisors α β] {a : α}
-
-lemma zero_mem_smul_iff : 0 ∈ s • t ↔ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty where
-  mp := by
-    rintro ⟨a, ha, b, hb, h⟩
-    obtain rfl | rfl := eq_zero_or_eq_zero_of_smul_eq_zero h
-    · exact Or.inl ⟨ha, b, hb⟩
-    · exact Or.inr ⟨hb, a, ha⟩
-  mpr := by
-    rintro (⟨hs, b, hb⟩ | ⟨ht, a, ha⟩)
-    · exact ⟨0, hs, b, hb, zero_smul _ _⟩
-    · exact ⟨a, ha, 0, ht, smul_zero _⟩
-
 end SMulWithZero
 
 /-- If the scalar multiplication `(· • ·) : α → β → β` is distributive,
@@ -129,28 +108,14 @@ protected noncomputable def mulDistribMulActionSet [Monoid α] [Monoid β] [MulD
 
 scoped[Pointwise] attribute [instance] Set.distribMulActionSet Set.mulDistribMulActionSet
 
-instance instNoZeroSMulDivisors [Zero α] [Zero β] [SMul α β] [NoZeroSMulDivisors α β] :
-    NoZeroSMulDivisors (Set α) (Set β) where
-  eq_zero_or_eq_zero_of_smul_eq_zero {s t} h := by
+instance [Zero α] [Mul α] [NoZeroDivisors α] : NoZeroDivisors (Set α) where
+  eq_zero_or_eq_zero_of_mul_eq_zero {s t} h := by
     by_contra! H
-    have hst : (s • t).Nonempty := h.symm.subst zero_nonempty
-    rw [Ne, ← hst.of_smul_left.subset_zero_iff, Ne,
-      ← hst.of_smul_right.subset_zero_iff] at H
+    have hst : (s * t).Nonempty := h.symm.subst zero_nonempty
+    rw [Ne, ← hst.of_smul_left.subset_zero_iff, Ne, ← hst.of_smul_right.subset_zero_iff] at H
     simp only [not_subset, mem_zero] at H
     obtain ⟨⟨a, hs, ha⟩, b, ht, hb⟩ := H
-    exact (eq_zero_or_eq_zero_of_smul_eq_zero <| h.subset <| smul_mem_smul hs ht).elim ha hb
-
-instance noZeroSMulDivisors_set [Zero α] [Zero β] [SMul α β] [NoZeroSMulDivisors α β] :
-    NoZeroSMulDivisors α (Set β) where
-  eq_zero_or_eq_zero_of_smul_eq_zero {a s} h := by
-    by_contra! H
-    have hst : (a • s).Nonempty := h.symm.subst zero_nonempty
-    rw [Ne, Ne, ← hst.of_image.subset_zero_iff, not_subset] at H
-    obtain ⟨ha, b, ht, hb⟩ := H
-    exact (eq_zero_or_eq_zero_of_smul_eq_zero <| h.subset <| smul_mem_smul_set ht).elim ha hb
-
-instance [Zero α] [Mul α] [NoZeroDivisors α] : NoZeroDivisors (Set α) where
-  eq_zero_or_eq_zero_of_mul_eq_zero h := eq_zero_or_eq_zero_of_smul_eq_zero h
+    exact (eq_zero_or_eq_zero_of_mul_eq_zero <| h.subset <| mul_mem_mul hs ht).elim ha hb
 
 section GroupWithZero
 variable [GroupWithZero α] [MulAction α β] {s t : Set β} {a : α}

Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean

@@ -8,7 +8,6 @@ module
 public import Mathlib.Algebra.Group.Submonoid.Membership
 public import Mathlib.Algebra.GroupWithZero.Associated
 public import Mathlib.Algebra.GroupWithZero.Regular
-public import Mathlib.Algebra.NoZeroSMulDivisors.Defs
 public import Mathlib.Algebra.Regular.SMul
 public import Mathlib.Algebra.BigOperators.Group.Finset.Defs
 
@@ -246,10 +245,6 @@ lemma noZeroDivisors_iff_forall_mem_nonZeroDivisors :
     NoZeroDivisors M₀ ↔ ∀ x : M₀, x ≠ 0 → x ∈ M₀⁰ :=
   noZeroDivisors_iff_eq_zero_of_mul
 
-lemma noZeroSMulDivisors_iff_forall_mem_nonZeroSMulDivisors {M : Type*} [Zero M] [MulAction M₀ M] :
-    NoZeroSMulDivisors M₀ M ↔ ∀ x : M₀, x ≠ 0 → x ∈ nonZeroSMulDivisors M₀ M :=
-  noZeroSMulDivisors_iff_right_eq_zero_of_smul
-
 lemma IsSMulRegular.mem_nonZeroSMulDivisors {M : Type*} [Zero M] [MulActionWithZero M₀ M] {m₀ : M₀}
     (h : IsSMulRegular M m₀) : m₀ ∈ nonZeroSMulDivisors M₀ M :=
   fun _ ↦ h.right_eq_zero_of_smul

Mathlib/Algebra/Module/Basic.lean

@@ -7,10 +7,9 @@ module
 
 public import Mathlib.Algebra.Field.Defs
 public import Mathlib.Algebra.Group.Action.Pi
-public import Mathlib.Algebra.Notation.Indicator
 public import Mathlib.Algebra.GroupWithZero.Action.Units
-public import Mathlib.Algebra.Module.NatInt
-public import Mathlib.Algebra.NoZeroSMulDivisors.Defs
+public import Mathlib.Algebra.Module.Torsion.Free
+public import Mathlib.Algebra.Notation.Indicator
 public import Mathlib.Algebra.Ring.Invertible
 
 /-!
@@ -103,12 +102,12 @@ lemma support_smul_subset_right [Zero M] [SMulZeroClass R M] (f : α → R) (g :
     support (f • g) ⊆ support g :=
   fun x hbf hf ↦ hbf <| by rw [Pi.smul_apply', hf, smul_zero]
 
-lemma support_const_smul_of_ne_zero [Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M]
-    (c : R) (g : α → M) (hc : c ≠ 0) : support (c • g) = support g :=
-  ext fun x ↦ by simp only [hc, mem_support, Pi.smul_apply, Ne, smul_eq_zero, false_or]
+lemma support_const_smul_of_ne_zero [Semiring R] [IsDomain R] [AddCommMonoid M] [Module R M]
+    [Module.IsTorsionFree R M] (c : R) (g : α → M) (hc : c ≠ 0) : support (c • g) = support g :=
+  ext fun _ ↦ smul_ne_zero_iff_right hc
 
-lemma support_smul [Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M] (f : α → R)
-    (g : α → M) : support (f • g) = support f ∩ support g :=
+lemma support_smul [Semiring R] [IsDomain R] [AddCommMonoid M] [Module R M]
+    [Module.IsTorsionFree R M] (f : α → R) (g : α → M) : support (f • g) = support f ∩ support g :=
   ext fun _ => smul_ne_zero_iff
 
 lemma support_const_smul_subset [Zero M] [SMulZeroClass R M] (a : R) (f : α → M) :