feat(algebra/module/torsion): torsion ideal, decomposition lemma (#13414

)

Defines the torsion ideal of an element in a module, and also shows a decomposition lemma for torsion modules.



Co-authored-by: pbazin <75327486+pbazin@users.noreply.github.com>

src/algebra/module/torsion.lean

@@ -7,28 +7,40 @@ import algebra.module
 import linear_algebra.quotient
 import ring_theory.ideal.quotient
 import ring_theory.non_zero_divisors
+import algebra.direct_sum.module
+import group_theory.torsion
+import linear_algebra.isomorphisms
 import group_theory.torsion
 
 /-!
 # Torsion submodules
 
 ## Main definitions
 
+* `torsion_of R M x` : the torsion ideal of `x`, containing all `a` such that `a • x = 0`.
 * `submodule.torsion_by R M a` : the `a`-torsion submodule, containing all elements `x` of `M` such
   that `a • x = 0`.
+* `submodule.torsion_by_set R M s` : the submodule containing all elements `x` of `M` such that
+  `a • x = 0` for all `a` in `s`.
 * `submodule.torsion' R M S` : the `S`-torsion submodule, containing all elements `x` of `M` such
   that `a • x = 0` for some `a` in `S`.
 * `submodule.torsion R M` : the torsion submoule, containing all elements `x` of `M` such that
   `a • x = 0` for some non-zero-divisor `a` in `R`.
 * `module.is_torsion_by R M a` : the property that defines a `a`-torsion module. Similarly,
-  `is_torsion'` and `is_torsion`.
+  `is_torsion_by_set`, `is_torsion'` and `is_torsion`.
+* `module.is_torsion_by_set.module` : Creates a `R ⧸ I`-module from a `R`-module that
+  `is_torsion_by_set R _ I`.
 
 ## Main statements
 
+* `quot_torsion_of_equiv_span_singleton` : isomorphism between the span of an element of `M` and
+  the quotient by its torsion ideal.
 * `torsion' R M S` and `torsion R M` are submodules.
-* `torsion_by R M a` can be viewed as a `(R ⧸ R∙a)`-module.
+* `torsion_by_set_eq_torsion_by_span` : torsion by a set is torsion by the ideal generated by it.
 * `submodule.torsion_by_is_torsion_by` : the `a`-torsion submodule is a `a`-torsion module.
   Similar lemmas for `torsion'` and `torsion`.
+* `submodule.torsion_is_internal` : a `∏ i, p i`-torsion module is the internal direct sum of its
+  `p i`-torsion submodules when the `p i` are pairwise coprime.
 * `submodule.no_zero_smul_divisors_iff_torsion_bot` : a module over a domain has
   `no_zero_smul_divisors` (that is, there is no non-zero `a`, `x` such that `a • x = 0`)
   iff its torsion submodule is trivial.
@@ -48,6 +60,27 @@ import group_theory.torsion
 Torsion, submodule, module, quotient
 -/
 
+section
+variables (R M : Type*) [semiring R] [add_comm_monoid M] [module R M]
+/--The torsion ideal of `x`, containing all `a` such that `a • x = 0`.-/
+@[simps] def torsion_of (x : M) : ideal R := (linear_map.to_span_singleton R M x).ker
+variables {R M}
+@[simp] lemma mem_torsion_of_iff (x : M) (a : R) : a ∈ torsion_of R M x ↔ a • x = 0 := iff.rfl
+end
+
+section
+variables (R M : Type*) [ring R] [add_comm_group M] [module R M]
+/--The span of `x` in `M` is isomorphic to `R` quotiented by the torsion ideal of `x`.-/
+noncomputable def quot_torsion_of_equiv_span_singleton (x : M) :
+  (R ⧸ torsion_of R M x) ≃ₗ[R] (R ∙ x) :=
+(linear_map.to_span_singleton R M x).quot_ker_equiv_range.trans $
+linear_equiv.of_eq _ _ (linear_map.span_singleton_eq_range R M x).symm
+
+@[simp] lemma quot_torsion_of_equiv_span_singleton_apply_mk (x : M) (a : R) :
+  quot_torsion_of_equiv_span_singleton R M x (submodule.quotient.mk a) =
+    a • ⟨x, submodule.mem_span_singleton_self x⟩ := rfl
+end
+
 open_locale non_zero_divisors
 
 section defs
@@ -60,6 +93,9 @@ namespace submodule
   `a • x = 0`. -/
 @[simps] def torsion_by (a : R) : submodule R M := (distrib_mul_action.to_linear_map _ _ a).ker
 
+/-- The submodule containing all elements `x` of `M` such that `a • x = 0` for all `a` in `s`. -/
+@[simps] def torsion_by_set (s : set R) : submodule R M := Inf (torsion_by R M '' s)
+
 /-- The `S`-torsion submodule, containing all elements `x` of `M` such that `a • x = 0` for some
 `a` in `S`. -/
 @[simps] def torsion' (S : Type*)
@@ -82,6 +118,9 @@ namespace module
 /-- A `a`-torsion module is a module where every element is `a`-torsion. -/
 @[reducible] def is_torsion_by (a : R) := ∀ ⦃x : M⦄, a • x = 0
 
+/-- A module where every element is `a`-torsion for all `a` in `s`. -/
+@[reducible] def is_torsion_by_set (s : set R) := ∀ ⦃x : M⦄ ⦃a : s⦄, (a : R) • x = 0
+
 /-- A `S`-torsion module is a module where every element is `a`-torsion for some `a` in `S`. -/
 @[reducible] def is_torsion' (S : Type*) [has_scalar S M] := ∀ ⦃x : M⦄, ∃ a : S, a • x = 0
 
@@ -93,60 +132,226 @@ end module
 
 end defs
 
+variables {R M : Type*}
+
 namespace submodule
 
 open module
 
-variables {R M : Type*}
-
-section torsion_by
-
-variables [comm_semiring R] [add_comm_monoid M] [module R M] (a : R)
+variables [comm_semiring R] [add_comm_monoid M] [module R M] (s : set R) (a : R)
 
 @[simp] lemma smul_torsion_by (x : torsion_by R M a) : a • x = 0 := subtype.ext x.prop
 @[simp] lemma smul_coe_torsion_by (x : torsion_by R M a) : a • (x : M) = 0 := x.prop
 @[simp] lemma mem_torsion_by_iff (x : M) : x ∈ torsion_by R M a ↔ a • x = 0 := iff.rfl
 
+@[simp] lemma mem_torsion_by_set_iff (x : M) :
+  x ∈ torsion_by_set R M s ↔ ∀ a : s, (a : R) • x = 0 :=
+begin
+  refine ⟨λ h ⟨a, ha⟩, mem_Inf.mp h _ (set.mem_image_of_mem _ ha), λ h, mem_Inf.mpr _⟩,
+  rintro _ ⟨a, ha, rfl⟩, exact h ⟨a, ha⟩
+end
+
+@[simp] lemma torsion_by_singleton_eq : torsion_by_set R M {a} = torsion_by R M a :=
+begin
+  ext x,
+  simp only [mem_torsion_by_set_iff, set_coe.forall, subtype.coe_mk, set.mem_singleton_iff,
+    forall_eq, mem_torsion_by_iff]
+end
+@[simp] lemma is_torsion_by_singleton_iff : is_torsion_by_set R M {a} ↔ is_torsion_by R M a :=
+begin
+  refine ⟨λ h x, @h _ ⟨_, set.mem_singleton _⟩, λ h x, _⟩,
+  rintro ⟨b, rfl : b = a⟩, exact @h _
+end
+
+lemma is_torsion_by_set_iff_torsion_by_set_eq_top :
+  is_torsion_by_set R M s ↔ torsion_by_set R M s = ⊤ :=
+⟨λ h, eq_top_iff.mpr (λ _ _, (mem_torsion_by_set_iff _ _).mpr $ @h _),
+  λ h x, by { rw [← mem_torsion_by_set_iff, h], trivial }⟩
+
 /-- A `a`-torsion module is a module whose `a`-torsion submodule is the full space. -/
 lemma is_torsion_by_iff_torsion_by_eq_top : is_torsion_by R M a ↔ torsion_by R M a = ⊤ :=
-⟨λ h, eq_top_iff.mpr (λ _ _, @h _), λ h x, by { rw [← mem_torsion_by_iff, h], trivial }⟩
+by rw [← torsion_by_singleton_eq, ← is_torsion_by_singleton_iff,
+  is_torsion_by_set_iff_torsion_by_set_eq_top]
+
+lemma torsion_by_set_is_torsion_by_set : is_torsion_by_set R (torsion_by_set R M s) s :=
+λ ⟨x, hx⟩ a, subtype.ext $ (mem_torsion_by_set_iff _ _).mp hx a
 
 /-- The `a`-torsion submodule is a `a`-torsion module. -/
 lemma torsion_by_is_torsion_by : is_torsion_by R (torsion_by R M a) a := λ _, smul_torsion_by _ _
 
 @[simp] lemma torsion_by_torsion_by_eq_top : torsion_by R (torsion_by R M a) a = ⊤ :=
 (is_torsion_by_iff_torsion_by_eq_top a).mp $ torsion_by_is_torsion_by a
+@[simp] lemma torsion_by_set_torsion_by_set_eq_top :
+  torsion_by_set R (torsion_by_set R M s) s = ⊤ :=
+(is_torsion_by_set_iff_torsion_by_set_eq_top s).mp $ torsion_by_set_is_torsion_by_set s
+
+lemma torsion_by_set_le_torsion_by_set_of_subset {s t : set R} (st : s ⊆ t) :
+  torsion_by_set R M t ≤ torsion_by_set R M s :=
+Inf_le_Inf $ λ _ ⟨a, ha, h⟩, ⟨a, st ha, h⟩
+
+/-- Torsion by a set is torsion by the ideal generated by it. -/
+lemma torsion_by_set_eq_torsion_by_span :
+  torsion_by_set R M s = torsion_by_set R M (ideal.span s) :=
+begin
+  refine le_antisymm (λ x hx, _) (torsion_by_set_le_torsion_by_set_of_subset subset_span),
+  rw mem_torsion_by_set_iff at hx ⊢,
+  suffices : ideal.span s ≤ torsion_of R M x,
+  { rintro ⟨a, ha⟩, exact this ha },
+  rw ideal.span_le, exact λ a ha, hx ⟨a, ha⟩
+end
+lemma is_torsion_by_set_iff_is_torsion_by_span :
+  is_torsion_by_set R M s ↔ is_torsion_by_set R M (ideal.span s) :=
+by rw [is_torsion_by_set_iff_torsion_by_set_eq_top, is_torsion_by_set_iff_torsion_by_set_eq_top,
+  torsion_by_set_eq_torsion_by_span]
+
+lemma torsion_by_span_singleton_eq : torsion_by_set R M (R ∙ a) = torsion_by R M a :=
+((torsion_by_set_eq_torsion_by_span _).symm.trans $ torsion_by_singleton_eq _)
+lemma is_torsion_by_span_singleton_iff : is_torsion_by_set R M (R ∙ a) ↔ is_torsion_by R M a :=
+((is_torsion_by_set_iff_is_torsion_by_span _).symm.trans $ is_torsion_by_singleton_iff _)
+
+lemma torsion_by_le_torsion_by_of_dvd (a b : R) (dvd : a ∣ b) :
+  torsion_by R M a ≤ torsion_by R M b :=
+begin
+  rw [← torsion_by_span_singleton_eq, ← torsion_by_singleton_eq],
+  apply torsion_by_set_le_torsion_by_set_of_subset,
+  rintro c (rfl : c = b), exact ideal.mem_span_singleton.mpr dvd
+end
+
+@[simp] lemma torsion_by_one : torsion_by R M 1 = ⊥ :=
+eq_bot_iff.mpr (λ _ h, by { rw [mem_torsion_by_iff, one_smul] at h, exact h })
+@[simp] lemma torsion_by_univ : torsion_by_set R M set.univ = ⊥ :=
+by { rw [eq_bot_iff, ← torsion_by_one, ← torsion_by_singleton_eq],
+  exact torsion_by_set_le_torsion_by_set_of_subset (λ _ _, trivial) }
+
+section coprime
+open_locale big_operators
+open dfinsupp
+variables {ι : Type*} {p : ι → R} {S : finset ι} (hp : pairwise (is_coprime on λ s : S, p s))
+include hp
+
+lemma supr_torsion_by_eq_torsion_by_prod :
+  (⨆ i : S, torsion_by R M (p i)) = torsion_by R M (∏ i in S, p i) :=
+begin
+  cases S.eq_empty_or_nonempty with h h,
+  { rw [h, finset.prod_empty, torsion_by_one],
+    convert supr_of_empty _, exact subtype.is_empty_false },
+  apply le_antisymm,
+  { apply supr_le _, rintro ⟨i, is⟩,
+    exact torsion_by_le_torsion_by_of_dvd _ _ (finset.dvd_prod_of_mem p is) },
+  { intros x hx, classical, rw mem_supr_iff_exists_dfinsupp',
+    cases (exists_sum_eq_one_iff_pairwise_coprime h).mpr hp with f hf,
+    use equiv_fun_on_fintype.inv_fun (λ i, ⟨(f i * ∏ j in S \ {i}, p j) • x, begin
+      obtain ⟨i, is⟩ := i,
+      change p i • (f i * ∏ j in S \ {i}, _) • _ = _, change _ • _ = _ at hx,
+      rw [smul_smul, mul_comm, mul_assoc, mul_smul, ← finset.prod_eq_prod_diff_singleton_mul is,
+        hx, smul_zero]
+    end⟩),
+    simp only [equiv.inv_fun_as_coe, sum_eq_sum_fintype, coe_eq_zero, eq_self_iff_true,
+      implies_true_iff, finset.univ_eq_attach, equiv_fun_on_fintype_apply],
+    change ∑ i : S, ((f i * ∏ j in S \ {i}, p j) • x) = x,
+    have : ∑ i : S, _ = _ := S.sum_finset_coe (λ i, f i * ∏ j in S \ {i}, p j),
+    rw [← finset.sum_smul, this, hf, one_smul] }
+end
 
-end torsion_by
+lemma torsion_by_independent : complete_lattice.independent (λ i : S, torsion_by R M (p i)) :=
+λ i, begin
+  classical,
+  dsimp, rw [disjoint_iff, eq_bot_iff], intros x hx,
+  rw submodule.mem_inf at hx, obtain ⟨hxi, hxj⟩ := hx,
+  have hxi : p i • x = 0 := hxi,
+  rw mem_supr_iff_exists_dfinsupp' at hxj, cases hxj with f hf,
+  obtain ⟨b, c, h1⟩ := pairwise_coprime_iff_coprime_prod.mp hp i i.2,
+  rw [mem_bot, ← one_smul _ x, ← h1, add_smul],
+  convert (zero_add (0:M)),
+  { rw [mul_smul, hxi, smul_zero] },
+  { rw [← hf, smul_sum, sum_eq_zero],
+    intro j, by_cases ji : j = i,
+    { convert smul_zero _,
+      rw ← mem_bot _, convert coe_mem (f j),
+      symmetry, rw supr_eq_bot, intro hj',
+      exfalso, exact hj' ji },
+    { have hj' : ↑j ∈ S \ {i},
+      { rw finset.mem_sdiff, refine ⟨j.2, λ hj', ji _⟩, ext, rw ← finset.mem_singleton, exact hj' },
+      rw [finset.prod_eq_prod_diff_singleton_mul hj', ← mul_assoc, mul_smul],
+      have : (⨆ (H : ¬j = i), torsion_by R M (p j)) ≤ torsion_by R M (p j) := supr_const_le,
+      have : _ • _ = _ := this (coe_mem _),
+      rw [this, smul_zero] } }
+end
+end coprime
+end submodule
 
-section quotient
+section needs_group
+variables [comm_ring R] [add_comm_group M] [module R M]
+
+namespace submodule
+open_locale big_operators
+variables {ι : Type*} {p : ι → R} {S : finset ι} (hp : pairwise (is_coprime on λ s : S, p s))
+include hp
 
-variables [comm_ring R] [add_comm_group M] [module R M] (a : R)
+/--If the `p i` are pairwise coprime, a `∏ i, p i`-torsion module is the internal direct sum of
+its `p i`-torsion submodules.-/
+lemma torsion_is_internal [decidable_eq ι] (hM : torsion_by R M (∏ i in S, p i) = ⊤) :
+  direct_sum.submodule_is_internal (λ i : S, torsion_by R M (p i)) :=
+direct_sum.submodule_is_internal_of_independent_of_supr_eq_top
+  (torsion_by_independent hp) (by { rw ← hM, exact supr_torsion_by_eq_torsion_by_prod hp})
+
+end submodule
+
+namespace module
+variables {I : ideal R} (hM : is_torsion_by_set R M I)
+include hM
 
-instance : has_scalar (R ⧸ R ∙ a) (torsion_by R M a) :=
+/-- can't be an instance because hM can't be inferred -/
+def is_torsion_by_set.has_scalar : has_scalar (R ⧸ I) M :=
 { smul := λ b x, quotient.lift_on' b (• x) $ λ b₁ b₂ h, begin
-    rw submodule.quotient_rel_r_def at h,
     show b₁ • x = b₂ • x,
-    obtain ⟨c, h⟩ := ideal.mem_span_singleton'.mp h,
-    rw [← sub_eq_zero, ← sub_smul, ← h, mul_smul, smul_torsion_by, smul_zero],
+    have : (-b₁ + b₂) • x = 0 := @hM x ⟨_, h⟩,
+    rw [add_smul, neg_smul, neg_add_eq_zero] at this,
+    exact this
   end }
 
-@[simp] lemma torsion_by.mk_smul (b : R) (x : torsion_by R M a) :
-  ideal.quotient.mk (R ∙ a) b • x = b • x := rfl
+@[simp] lemma is_torsion_by_set.mk_smul (b : R) (x : M) :
+  by haveI := hM.has_scalar; exact ideal.quotient.mk I b • x = b • x := rfl
+
+/-- A `(R ⧸ I)`-module is a `R`-module which `is_torsion_by_set R M I`. -/
+def is_torsion_by_set.module : module (R ⧸ I) M :=
+@function.surjective.module_left _ _ _ _ _ _ _ hM.has_scalar
+  _ ideal.quotient.mk_surjective (is_torsion_by_set.mk_smul hM)
+
+end module
+
+namespace submodule
+
+instance (I : ideal R) : module (R ⧸ I) (torsion_by_set R M I) :=
+module.is_torsion_by_set.module $ torsion_by_set_is_torsion_by_set I
+
+@[simp] lemma torsion_by_set.mk_smul (I : ideal R) (b : R) (x : torsion_by_set R M I) :
+  ideal.quotient.mk I b • x = b • x := rfl
+
+instance (I : ideal R) {S : Type*} [has_scalar S R] [has_scalar S M]
+  [is_scalar_tower S R M] [is_scalar_tower S R R] :
+  is_scalar_tower S (R ⧸ I) (torsion_by_set R M I) :=
+{ smul_assoc := λ b d x, quotient.induction_on' d $ λ c, (smul_assoc b c x : _) }
 
 /-- The `a`-torsion submodule as a `(R ⧸ R∙a)`-module. -/
-instance : module (R ⧸ R ∙ a) (torsion_by R M a) :=
-@function.surjective.module_left _ _ (torsion_by R M a) _ _ _ _ _ (ideal.quotient.mk $ R ∙ a)
-  ideal.quotient.mk_surjective (torsion_by.mk_smul _)
+instance (a : R) : module (R ⧸ R ∙ a) (torsion_by R M a) :=
+module.is_torsion_by_set.module $
+  (is_torsion_by_span_singleton_iff a).mpr $ torsion_by_is_torsion_by a
+
+@[simp] lemma torsion_by.mk_smul (a b : R) (x : torsion_by R M a) :
+  ideal.quotient.mk (R ∙ a) b • x = b • x := rfl
 
-instance {S : Type*} [has_scalar S R] [has_scalar S M]
+instance (a : R) {S : Type*} [has_scalar S R] [has_scalar S M]
   [is_scalar_tower S R M] [is_scalar_tower S R R] :
   is_scalar_tower S (R ⧸ R ∙ a) (torsion_by R M a) :=
 { smul_assoc := λ b d x, quotient.induction_on' d $ λ c, (smul_assoc b c x : _) }
 
-end quotient
+end submodule
+end needs_group
 
+namespace submodule
 section torsion'
+open module
 
 variables [comm_semiring R] [add_comm_monoid M] [module R M]
 variables (S : Type*) [comm_monoid S] [distrib_mul_action S M] [smul_comm_class S R M]
@@ -177,6 +382,11 @@ torsion module. -/
 /-- The torsion submodule is always a torsion module. -/
 lemma torsion_is_torsion : module.is_torsion R (torsion R M) := torsion'_is_torsion' R⁰
 
+lemma is_torsion'_powers_iff (p : R) :
+  is_torsion' M (submonoid.powers p) ↔ ∀ x : M, ∃ n : ℕ, p ^ n • x = 0 :=
+⟨λ h x, let ⟨⟨a, ⟨n, rfl⟩⟩, hx⟩ := @h x in ⟨n, hx⟩,
+λ h x, let ⟨n, hn⟩ := h x in ⟨⟨_, ⟨n, rfl⟩⟩, hn⟩⟩
+
 end torsion'
 
 section torsion
@@ -228,12 +438,28 @@ instance no_zero_smul_divisors [is_domain R] : no_zero_smul_divisors R (M ⧸ to
 no_zero_smul_divisors_iff_torsion_eq_bot.mpr torsion_eq_bot
 
 end quotient_torsion
-
 end submodule
 
-namespace add_monoid
+namespace ideal.quotient
+
+open submodule
 
-variables {M : Type*}
+lemma torsion_by_eq_span_singleton {R : Type*} [comm_ring R] (a b : R) (ha : a ∈ R⁰) :
+  torsion_by R (R ⧸ R ∙ a * b) a = R ∙ (mk _ b) :=
+begin
+  ext x, rw [mem_torsion_by_iff, mem_span_singleton],
+  obtain ⟨x, rfl⟩ := mk_surjective x, split; intro h,
+  { rw [← mk_eq_mk, ← quotient.mk_smul, quotient.mk_eq_zero, mem_span_singleton] at h,
+    obtain ⟨c, h⟩ := h, rw [smul_eq_mul, smul_eq_mul, mul_comm, mul_assoc,
+      mul_cancel_left_mem_non_zero_divisor ha, mul_comm] at h,
+    use c, rw [← h, ← mk_eq_mk, ← quotient.mk_smul, smul_eq_mul, mk_eq_mk] },
+  { obtain ⟨c, h⟩ := h,
+    rw [← h, smul_comm, ← mk_eq_mk, ← quotient.mk_smul,
+      (quotient.mk_eq_zero _).mpr $ mem_span_singleton_self _, smul_zero] }
+end
+end ideal.quotient
+
+namespace add_monoid
 
 theorem is_torsion_iff_is_torsion_nat [add_comm_monoid M] :
   add_monoid.is_torsion M ↔ module.is_torsion ℕ M :=