case h
R : Type u_1
inst✝⁵ : CommRing R
I J✝ : Ideal R
M : Type ?u.81481
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type ?u.82014
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsNoetherianRing R
hI : Ideal.IsPrimary I
J : Ideal R
⊢ J ∈ associatedPrimes R (R ⧸ I) ↔ J ∈ {Ideal.radical I}
R : Type u_1
inst✝⁵ : CommRing R
I J : Ideal R
M : Type ?u.81481
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type ?u.82014
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsNoetherianRing R
hI : Ideal.IsPrimary I
⊢ associatedPrimes R (R ⧸ I) = {Ideal.radical I}
ext J
case h
R : Type u_1
inst✝⁵ : CommRing R
I J✝ : Ideal R
M : Type ?u.81481
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type ?u.82014
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsNoetherianRing R
hI : Ideal.IsPrimary I
J : Ideal R
⊢ J ∈ associatedPrimes R (R ⧸ I) ↔ J = Ideal.radical I
case h
R : Type u_1
inst✝⁵ : CommRing R
I J✝ : Ideal R
M : Type ?u.81481
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type ?u.82014
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsNoetherianRing R
hI : Ideal.IsPrimary I
J : Ideal R
⊢ J ∈ associatedPrimes R (R ⧸ I) ↔ J ∈ {Ideal.radical I}
rw [Set.mem_singleton_iff]
case h
R : Type u_1
inst✝⁵ : CommRing R
I J✝ : Ideal R
M : Type ?u.81481
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type ?u.82014
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsNoetherianRing R
hI : Ideal.IsPrimary I
J : Ideal R
⊢ J = Ideal.radical I → J ∈ associatedPrimes R (R ⧸ I)
case h
R : Type u_1
inst✝⁵ : CommRing R
I J✝ : Ideal R
M : Type ?u.81481
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type ?u.82014
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsNoetherianRing R
hI : Ideal.IsPrimary I
J : Ideal R
⊢ J ∈ associatedPrimes R (R ⧸ I) ↔ J = Ideal.radical I
refine' ⟨IsAssociatedPrime.eq_radical hI, _⟩
case h
R : Type u_1
inst✝⁵ : CommRing R
I J : Ideal R
M : Type ?u.81481
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type ?u.82014
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsNoetherianRing R
hI : Ideal.IsPrimary I
⊢ Ideal.radical I ∈ associatedPrimes R (R ⧸ I)
case h
R : Type u_1
inst✝⁵ : CommRing R
I J✝ : Ideal R
M : Type ?u.81481
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type ?u.82014
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsNoetherianRing R
hI : Ideal.IsPrimary I
J : Ideal R
⊢ J = Ideal.radical I → J ∈ associatedPrimes R (R ⧸ I)
rintro rfl
case h
R : Type u_1
inst✝⁵ : CommRing R
I J : Ideal R
M : Type ?u.81481
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type ?u.82014
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsNoetherianRing R
hI : Ideal.IsPrimary I
this : Nontrivial (R ⧸ I)
⊢ Ideal.radical I ∈ associatedPrimes R (R ⧸ I)
case h
R : Type u_1
inst✝⁵ : CommRing R
I J : Ideal R
M : Type ?u.81481
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type ?u.82014
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsNoetherianRing R
hI : Ideal.IsPrimary I
⊢ Ideal.radical I ∈ associatedPrimes R (R ⧸ I)
haveI : Nontrivial (R ⧸ I) := by
  refine ⟨(Ideal.Quotient.mk I : _) 1, (Ideal.Quotient.mk I : _) 0, ?_⟩
  rw [Ne.def, Ideal.Quotient.eq, sub_zero, ← Ideal.eq_top_iff_one]
  exact hI.1
case h.intro
R : Type u_1
inst✝⁵ : CommRing R
I J : Ideal R
M : Type ?u.81481
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type ?u.82014
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsNoetherianRing R
hI : Ideal.IsPrimary I
this : Nontrivial (R ⧸ I)
a : Ideal R
ha : a ∈ associatedPrimes R (R ⧸ I)
⊢ Ideal.radical I ∈ associatedPrimes R (R ⧸ I)
case h
R : Type u_1
inst✝⁵ : CommRing R
I J : Ideal R
M : Type ?u.81481
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type ?u.82014
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsNoetherianRing R
hI : Ideal.IsPrimary I
this : Nontrivial (R ⧸ I)
⊢ Ideal.radical I ∈ associatedPrimes R (R ⧸ I)
obtain ⟨a, ha⟩ := associatedPrimes.nonempty R (R ⧸ I)
no goals
case h.intro
R : Type u_1
inst✝⁵ : CommRing R
I J : Ideal R
M : Type ?u.81481
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type ?u.82014
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsNoetherianRing R
hI : Ideal.IsPrimary I
this : Nontrivial (R ⧸ I)
a : Ideal R
ha : a ∈ associatedPrimes R (R ⧸ I)
⊢ Ideal.radical I ∈ associatedPrimes R (R ⧸ I)
exact ha.eq_radical hI ▸ ha
R : Type u_1
inst✝⁵ : CommRing R
I J : Ideal R
M : Type ?u.81481
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type ?u.82014
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsNoetherianRing R
hI : Ideal.IsPrimary I
⊢ ↑(Ideal.Quotient.mk I) 1 ≠ ↑(Ideal.Quotient.mk I) 0
R : Type u_1
inst✝⁵ : CommRing R
I J : Ideal R
M : Type ?u.81481
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type ?u.82014
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsNoetherianRing R
hI : Ideal.IsPrimary I
⊢ Nontrivial (R ⧸ I)
refine ⟨(Ideal.Quotient.mk I : _) 1, (Ideal.Quotient.mk I : _) 0, ?_⟩
R : Type u_1
inst✝⁵ : CommRing R
I J : Ideal R
M : Type ?u.81481
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type ?u.82014
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsNoetherianRing R
hI : Ideal.IsPrimary I
⊢ ¬I = ⊤
R : Type u_1
inst✝⁵ : CommRing R
I J : Ideal R
M : Type ?u.81481
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type ?u.82014
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsNoetherianRing R
hI : Ideal.IsPrimary I
⊢ ↑(Ideal.Quotient.mk I) 1 ≠ ↑(Ideal.Quotient.mk I) 0
rw [Ne.def, Ideal.Quotient.eq, sub_zero, ← Ideal.eq_top_iff_one]
no goals
R : Type u_1
inst✝⁵ : CommRing R
I J : Ideal R
M : Type ?u.81481
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type ?u.82014
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsNoetherianRing R
hI : Ideal.IsPrimary I
⊢ ¬I = ⊤
exact hI.1