[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
⊢ DirectSum.IsInternal fun p => torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors I))
[PROOFSTEP]
let P := factors I
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
⊢ DirectSum.IsInternal fun p => torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors I))
[PROOFSTEP]
have prime_of_mem := fun p (hp : p ∈ P.toFinset) => prime_of_factor p (Multiset.mem_toFinset.mp hp)
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
⊢ DirectSum.IsInternal fun p => torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors I))
[PROOFSTEP]
apply @torsionBySet_isInternal _ _ _ _ _ _ _ _ (fun p => p ^ P.count p) _
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
⊢ Module.IsTorsionBySet R M ↑(⨅ (i : Ideal R) (_ : i ∈ Multiset.toFinset (factors I)), i ^ Multiset.count i P)
[PROOFSTEP]
convert hM
[GOAL]
case h.e'_6.h.e'_4
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
⊢ ⨅ (i : Ideal R) (_ : i ∈ Multiset.toFinset (factors I)), i ^ Multiset.count i P = I
[PROOFSTEP]
rw [← Finset.inf_eq_iInf, IsDedekindDomain.inf_prime_pow_eq_prod, ← Finset.prod_multiset_count, ← associated_iff_eq]
[GOAL]
case h.e'_6.h.e'_4
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
⊢ Associated (Multiset.prod (factors I)) I
[PROOFSTEP]
exact factors_prod hI
[GOAL]
case h.e'_6.h.e'_4.prime
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
⊢ ∀ (i : Ideal R), i ∈ Multiset.toFinset (factors I) → Prime i
[PROOFSTEP]
exact prime_of_mem
[GOAL]
case h.e'_6.h.e'_4.coprime
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
⊢ ∀ (i : Ideal R),
    i ∈ Multiset.toFinset (factors I) → ∀ (j : Ideal R), j ∈ Multiset.toFinset (factors I) → i ≠ j → i ≠ j
[PROOFSTEP]
exact fun _ _ _ _ ij => ij
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
⊢ Set.Pairwise ↑(Multiset.toFinset (factors I)) fun i j =>
    (fun p => p ^ Multiset.count p P) i ⊔ (fun p => p ^ Multiset.count p P) j = ⊤
[PROOFSTEP]
intro p hp q hq pq
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
p : Ideal R
hp : p ∈ ↑(Multiset.toFinset (factors I))
q : Ideal R
hq : q ∈ ↑(Multiset.toFinset (factors I))
pq : p ≠ q
⊢ (fun p => p ^ Multiset.count p P) p ⊔ (fun p => p ^ Multiset.count p P) q = ⊤
[PROOFSTEP]
dsimp
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
p : Ideal R
hp : p ∈ ↑(Multiset.toFinset (factors I))
q : Ideal R
hq : q ∈ ↑(Multiset.toFinset (factors I))
pq : p ≠ q
⊢ p ^ Multiset.count p (factors I) ⊔ q ^ Multiset.count q (factors I) = ⊤
[PROOFSTEP]
rw [irreducible_pow_sup]
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
p : Ideal R
hp : p ∈ ↑(Multiset.toFinset (factors I))
q : Ideal R
hq : q ∈ ↑(Multiset.toFinset (factors I))
pq : p ≠ q
⊢ p ^ min (Multiset.count p (normalizedFactors (q ^ Multiset.count q (factors I)))) (Multiset.count p (factors I)) = ⊤
[PROOFSTEP]
suffices (normalizedFactors _).count p = 0 by rw [this, zero_min, pow_zero, Ideal.one_eq_top]
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
p : Ideal R
hp : p ∈ ↑(Multiset.toFinset (factors I))
q : Ideal R
hq : q ∈ ↑(Multiset.toFinset (factors I))
pq : p ≠ q
this : Multiset.count p (normalizedFactors ?m.97629) = 0
⊢ p ^ min (Multiset.count p (normalizedFactors (q ^ Multiset.count q (factors I)))) (Multiset.count p (factors I)) = ⊤
[PROOFSTEP]
rw [this, zero_min, pow_zero, Ideal.one_eq_top]
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
p : Ideal R
hp : p ∈ ↑(Multiset.toFinset (factors I))
q : Ideal R
hq : q ∈ ↑(Multiset.toFinset (factors I))
pq : p ≠ q
⊢ Multiset.count p (normalizedFactors (q ^ Multiset.count q (factors I))) = 0
[PROOFSTEP]
rw [Multiset.count_eq_zero, normalizedFactors_of_irreducible_pow (prime_of_mem q hq).irreducible,
  Multiset.mem_replicate]
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
p : Ideal R
hp : p ∈ ↑(Multiset.toFinset (factors I))
q : Ideal R
hq : q ∈ ↑(Multiset.toFinset (factors I))
pq : p ≠ q
⊢ ¬(Multiset.count q (factors I) ≠ 0 ∧ p = ↑normalize q)
[PROOFSTEP]
exact fun H => pq <| H.2.trans <| normalize_eq q
[GOAL]
case hI
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
p : Ideal R
hp : p ∈ ↑(Multiset.toFinset (factors I))
q : Ideal R
hq : q ∈ ↑(Multiset.toFinset (factors I))
pq : p ≠ q
⊢ q ^ Multiset.count q (factors I) ≠ ⊥
[PROOFSTEP]
rw [← Ideal.zero_eq_bot]
[GOAL]
case hI
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
p : Ideal R
hp : p ∈ ↑(Multiset.toFinset (factors I))
q : Ideal R
hq : q ∈ ↑(Multiset.toFinset (factors I))
pq : p ≠ q
⊢ q ^ Multiset.count q (factors I) ≠ 0
[PROOFSTEP]
apply pow_ne_zero
[GOAL]
case hI.h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
p : Ideal R
hp : p ∈ ↑(Multiset.toFinset (factors I))
q : Ideal R
hq : q ∈ ↑(Multiset.toFinset (factors I))
pq : p ≠ q
⊢ q ≠ 0
[PROOFSTEP]
exact (prime_of_mem q hq).ne_zero
[GOAL]
case hJ
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
p : Ideal R
hp : p ∈ ↑(Multiset.toFinset (factors I))
q : Ideal R
hq : q ∈ ↑(Multiset.toFinset (factors I))
pq : p ≠ q
⊢ Irreducible p
[PROOFSTEP]
exact (prime_of_mem p hp).irreducible
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDedekindDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
⊢ DirectSum.IsInternal fun p => torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors (annihilator ⊤)))
[PROOFSTEP]
have hM' := Module.isTorsionBySet_annihilator_top R M
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDedekindDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M ↑(annihilator ⊤)
⊢ DirectSum.IsInternal fun p => torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors (annihilator ⊤)))
[PROOFSTEP]
have hI := Submodule.annihilator_top_inter_nonZeroDivisors hM
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDedekindDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M ↑(annihilator ⊤)
hI : ↑(annihilator ⊤) ∩ ↑(nonZeroDivisors R) ≠ ∅
⊢ DirectSum.IsInternal fun p => torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors (annihilator ⊤)))
[PROOFSTEP]
refine' isInternal_prime_power_torsion_of_is_torsion_by_ideal _ hM'
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDedekindDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M ↑(annihilator ⊤)
hI : ↑(annihilator ⊤) ∩ ↑(nonZeroDivisors R) ≠ ∅
⊢ annihilator ⊤ ≠ ⊥
[PROOFSTEP]
rw [← Set.nonempty_iff_ne_empty] at hI 
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDedekindDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M ↑(annihilator ⊤)
hI : Set.Nonempty (↑(annihilator ⊤) ∩ ↑(nonZeroDivisors R))
⊢ annihilator ⊤ ≠ ⊥
[PROOFSTEP]
rw [Submodule.ne_bot_iff]
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDedekindDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M ↑(annihilator ⊤)
hI : Set.Nonempty (↑(annihilator ⊤) ∩ ↑(nonZeroDivisors R))
⊢ ∃ x, x ∈ annihilator ⊤ ∧ x ≠ 0
[PROOFSTEP]
obtain ⟨x, H, hx⟩ := hI
[GOAL]
case intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDedekindDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M ↑(annihilator ⊤)
x : R
H : x ∈ ↑(annihilator ⊤)
hx : x ∈ ↑(nonZeroDivisors R)
⊢ ∃ x, x ∈ annihilator ⊤ ∧ x ≠ 0
[PROOFSTEP]
exact ⟨x, H, nonZeroDivisors.ne_zero hx⟩
