refactor(algebra/module/dedekind_domain): eliminate existentials (#14734

)

This extracts some constructions from some long existentials so that we don't have to prove everything about the construction in a single place.

This makes some of the statements longer, so in places the existential version is kept in terms of the definition one.

src/algebra/module/dedekind_domain.lean

@@ -26,17 +26,17 @@ namespace submodule
 variables [is_dedekind_domain R]
 open unique_factorization_monoid
 
+open_locale classical
+
 /--Over a Dedekind domain, a `I`-torsion module is the internal direct sum of its `p i ^ e i`-
 torsion submodules, where `I = ∏ i, p i ^ e i` is its unique decomposition in prime ideals.-/
 lemma is_internal_prime_power_torsion_of_is_torsion_by_ideal {I : ideal R} (hI : I ≠ ⊥)
   (hM : module.is_torsion_by_set R M I) :
-  ∃ (P : finset $ ideal R) [decidable_eq P] [∀ p ∈ P, prime p] (e : P → ℕ),
-  by exactI direct_sum.is_internal (λ p : P, torsion_by_set R M (p ^ e p : ideal R)) :=
+  direct_sum.is_internal (λ p : (factors I).to_finset,
+    torsion_by_set R M (p ^ (factors I).count p : ideal R)) :=
 begin
-  classical,
   let P := factors I,
   have prime_of_mem := λ p (hp : p ∈ P.to_finset), prime_of_factor p (multiset.mem_to_finset.mp hp),
-  refine ⟨P.to_finset, infer_instance, prime_of_mem, λ i, P.count i, _⟩,
   apply @torsion_by_set_is_internal _ _ _ _ _ _ _ _ (λ p, p ^ P.count p) _,
   { convert hM,
     rw [← finset.inf_eq_infi, is_dedekind_domain.inf_prime_pow_eq_prod,
@@ -55,15 +55,25 @@ begin
 end
 
 /--A finitely generated torsion module over a Dedekind domain is an internal direct sum of its
-`p i ^ e i`-torsion submodules for some prime ideals `p i` and numbers `e i`.-/
+`p i ^ e i`-torsion submodules where `p i` are factors of `(⊤ : submodule R M).annihilator` and
+`e i` are their multiplicities. -/
 theorem is_internal_prime_power_torsion [module.finite R M] (hM : module.is_torsion R M) :
-  ∃ (P : finset $ ideal R) [decidable_eq P] [∀ p ∈ P, prime p] (e : P → ℕ),
-  by exactI direct_sum.is_internal (λ p : P, torsion_by_set R M (p ^ e p : ideal R)) :=
+  direct_sum.is_internal (λ p : (factors (⊤ : submodule R M).annihilator).to_finset,
+    torsion_by_set R M (p ^ (factors (⊤ : submodule R M).annihilator).count p : ideal R)) :=
 begin
-  obtain ⟨I, hI, hM'⟩ := is_torsion_by_ideal_of_finite_of_is_torsion hM,
+  have hM' := module.is_torsion_by_set_annihilator_top R M,
+  have hI := submodule.annihilator_top_inter_non_zero_divisors hM,
   refine is_internal_prime_power_torsion_of_is_torsion_by_ideal _ hM',
   rw ←set.nonempty_iff_ne_empty at hI, rw submodule.ne_bot_iff,
   obtain ⟨x, H, hx⟩ := hI, exact ⟨x, H, non_zero_divisors.ne_zero hx⟩
 end
 
+/--A finitely generated torsion module over a Dedekind domain is an internal direct sum of its
+`p i ^ e i`-torsion submodules for some prime ideals `p i` and numbers `e i`.-/
+theorem exists_is_internal_prime_power_torsion [module.finite R M] (hM : module.is_torsion R M) :
+  ∃ (P : finset $ ideal R) [decidable_eq P] [∀ p ∈ P, prime p] (e : P → ℕ),
+  by exactI direct_sum.is_internal (λ p : P, torsion_by_set R M (p ^ e p : ideal R)) :=
+⟨_, _, λ p hp, prime_of_factor p (multiset.mem_to_finset.mp hp), _,
+    is_internal_prime_power_torsion hM⟩
+
 end submodule

src/algebra/module/pid.lean

@@ -47,7 +47,7 @@ Finitely generated module, principal ideal domain, classification, structure the
 -/
 
 universes u v
-open_locale big_operators
+open_locale big_operators classical
 
 variables {R : Type u} [comm_ring R] [is_domain R] [is_principal_ideal_ring R]
 variables {M : Type v} [add_comm_group M] [module R M]
@@ -56,21 +56,36 @@ variables {N : Type (max u v)} [add_comm_group N] [module R N]
 open_locale direct_sum
 open submodule
 
+open unique_factorization_monoid
+
 /--A finitely generated torsion module over a PID is an internal direct sum of its
 `p i ^ e i`-torsion submodules for some primes `p i` and numbers `e i`.-/
 theorem submodule.is_internal_prime_power_torsion_of_pid
+  [module.finite R M] (hM : module.is_torsion R M) :
+  direct_sum.is_internal (λ p : (factors (⊤ : submodule R M).annihilator).to_finset,
+    torsion_by R M
+      (is_principal.generator (p : ideal R)
+        ^ (factors (⊤ : submodule R M).annihilator).count p)) :=
+begin
+  convert is_internal_prime_power_torsion hM,
+  ext p : 1,
+  rw [← torsion_by_span_singleton_eq, ideal.submodule_span_eq, ← ideal.span_singleton_pow,
+    ideal.span_singleton_generator],
+end
+
+/--A finitely generated torsion module over a PID is an internal direct sum of its
+`p i ^ e i`-torsion submodules for some primes `p i` and numbers `e i`.-/
+theorem submodule.exists_is_internal_prime_power_torsion_of_pid
   [module.finite R M] (hM : module.is_torsion R M) :
   ∃ (ι : Type u) [fintype ι] [decidable_eq ι] (p : ι → R) (h : ∀ i, irreducible $ p i) (e : ι → ℕ),
   by exactI direct_sum.is_internal (λ i, torsion_by R M $ p i ^ e i) :=
 begin
-  obtain ⟨P, dec, hP, e, this⟩ := is_internal_prime_power_torsion hM,
-  refine ⟨P, infer_instance, dec, λ p, is_principal.generator (p : ideal R), _, e, _⟩,
+  refine ⟨_, _, _, _, _, _, submodule.is_internal_prime_power_torsion_of_pid hM⟩,
+  exact finset.fintype_coe_sort _,
   { rintro ⟨p, hp⟩,
-    haveI := ideal.is_prime_of_prime (hP p hp),
-    exact (is_principal.prime_generator_of_is_prime p (hP p hp).ne_zero).irreducible },
-  { convert this, ext p : 1,
-    rw [← torsion_by_span_singleton_eq, ideal.submodule_span_eq, ← ideal.span_singleton_pow,
-      ideal.span_singleton_generator] }
+    have hP := prime_of_factor p (multiset.mem_to_finset.mp hp),
+    haveI := ideal.is_prime_of_prime hP,
+    exact (is_principal.prime_generator_of_is_prime p hP.ne_zero).irreducible },
 end
 
 namespace module
@@ -205,7 +220,7 @@ theorem equiv_direct_sum_of_is_torsion [h' : module.finite R N] (hN : module.is_
   ∃ (ι : Type u) [fintype ι] (p : ι → R) (h : ∀ i, irreducible $ p i) (e : ι → ℕ),
   nonempty $ N ≃ₗ[R] ⨁ (i : ι), R ⧸ R ∙ (p i ^ e i) :=
 begin
-  obtain ⟨I, fI, _, p, hp, e, h⟩ := submodule.is_internal_prime_power_torsion_of_pid hN,
+  obtain ⟨I, fI, _, p, hp, e, h⟩ := submodule.exists_is_internal_prime_power_torsion_of_pid hN,
   haveI := fI,
   have : ∀ i, ∃ (d : ℕ) (k : fin d → ℕ),
     nonempty $ torsion_by R N (p i ^ e i) ≃ₗ[R] ⨁ j, R ⧸ R ∙ (p i ^ k j),

src/algebra/module/torsion.lean

@@ -496,19 +496,25 @@ section torsion
 variables [comm_semiring R] [add_comm_monoid M] [module R M]
 open_locale big_operators
 
-lemma is_torsion_by_ideal_of_finite_of_is_torsion [module.finite R M] (hM : module.is_torsion R M) :
-  ∃ I : ideal R, (I : set R) ∩ R⁰ ≠ ∅ ∧ module.is_torsion_by_set R M I :=
+variables (R M)
+
+lemma _root_.module.is_torsion_by_set_annihilator_top :
+  module.is_torsion_by_set R M (⊤ : submodule R M).annihilator :=
+λ x ha, mem_annihilator.mp ha.prop x mem_top
+
+variables {R M}
+
+lemma _root_.submodule.annihilator_top_inter_non_zero_divisors [module.finite R M]
+  (hM : module.is_torsion R M) :
+  ((⊤ : submodule R M).annihilator : set R) ∩ R⁰ ≠ ∅:=
 begin
-  cases (module.finite_def.mp infer_instance : (⊤ : submodule R M).fg) with S h,
-  refine ⟨∏ x in S, ideal.torsion_of R M x, _, _⟩,
-  { refine set.nonempty.ne_empty ⟨_, _, (∏ x in S, (@hM x).some : R⁰).2⟩,
-    rw [subtype.val_eq_coe, submonoid.coe_finset_prod],
-    apply ideal.prod_mem_prod,
-    exact λ x _, (@hM x).some_spec },
-  { rw [module.is_torsion_by_set_iff_torsion_by_set_eq_top, eq_top_iff, ← h, span_le],
-    intros x hx, apply torsion_by_set_le_torsion_by_set_of_subset,
-    { apply ideal.le_of_dvd, exact finset.dvd_prod_of_mem _ hx },
-    { rw mem_torsion_by_set_iff, rintro ⟨a, ha⟩, exact ha } }
+  obtain ⟨S, hS⟩ := ‹module.finite R M›.out,
+  refine set.nonempty.ne_empty ⟨_, _, (∏ x in S, (@hM x).some : R⁰).prop⟩,
+  rw [submonoid.coe_finset_prod, set_like.mem_coe, ←hS, mem_annihilator_span],
+  intro n,
+  letI := classical.dec_eq M,
+  rw [←finset.prod_erase_mul _ _ n.prop, mul_smul, ←submonoid.smul_def, (@hM n).some_spec,
+    smul_zero],
 end
 
 variables [no_zero_divisors R] [nontrivial R]