[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
h : IsAssociatedPrime I M
hf : Function.Injective ↑f
⊢ IsAssociatedPrime I M'
[PROOFSTEP]
obtain ⟨x, rfl⟩ := h.2
[GOAL]
case intro
R : Type u_1
inst✝⁴ : CommRing R
J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ↑f
x : M
h : IsAssociatedPrime (Submodule.annihilator (Submodule.span R {x})) M
⊢ IsAssociatedPrime (Submodule.annihilator (Submodule.span R {x})) M'
[PROOFSTEP]
refine' ⟨h.1, ⟨f x, _⟩⟩
[GOAL]
case intro
R : Type u_1
inst✝⁴ : CommRing R
J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ↑f
x : M
h : IsAssociatedPrime (Submodule.annihilator (Submodule.span R {x})) M
⊢ Submodule.annihilator (Submodule.span R {x}) = Submodule.annihilator (Submodule.span R {↑f x})
[PROOFSTEP]
ext r
[GOAL]
case intro.h
R : Type u_1
inst✝⁴ : CommRing R
J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ↑f
x : M
h : IsAssociatedPrime (Submodule.annihilator (Submodule.span R {x})) M
r : R
⊢ r ∈ Submodule.annihilator (Submodule.span R {x}) ↔ r ∈ Submodule.annihilator (Submodule.span R {↑f x})
[PROOFSTEP]
rw [Submodule.mem_annihilator_span_singleton, Submodule.mem_annihilator_span_singleton, ← map_smul, ← f.map_zero,
  hf.eq_iff]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
I J : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type u_3
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : Subsingleton M
⊢ ¬IsAssociatedPrime I M
[PROOFSTEP]
rintro ⟨hI, x, hx⟩
[GOAL]
case intro.intro
R : Type u_1
inst✝⁵ : CommRing R
I J : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type u_3
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : Subsingleton M
hI : Ideal.IsPrime I
x : M
hx : I = Submodule.annihilator (Submodule.span R {x})
⊢ False
[PROOFSTEP]
apply hI.ne_top
[GOAL]
case intro.intro
R : Type u_1
inst✝⁵ : CommRing R
I J : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type u_3
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : Subsingleton M
hI : Ideal.IsPrime I
x : M
hx : I = Submodule.annihilator (Submodule.span R {x})
⊢ I = ⊤
[PROOFSTEP]
rwa [Subsingleton.elim x 0, Submodule.span_singleton_eq_bot.mpr rfl, Submodule.annihilator_bot] at hx 
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
H : IsNoetherianRing R
x : M
hx : x ≠ 0
⊢ ∃ P, IsAssociatedPrime P M ∧ Submodule.annihilator (Submodule.span R {x}) ≤ P
[PROOFSTEP]
have : (R ∙ x).annihilator ≠ ⊤ := by
  rwa [Ne.def, Ideal.eq_top_iff_one, Submodule.mem_annihilator_span_singleton, one_smul]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
H : IsNoetherianRing R
x : M
hx : x ≠ 0
⊢ Submodule.annihilator (Submodule.span R {x}) ≠ ⊤
[PROOFSTEP]
rwa [Ne.def, Ideal.eq_top_iff_one, Submodule.mem_annihilator_span_singleton, one_smul]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
H : IsNoetherianRing R
x : M
hx : x ≠ 0
this : Submodule.annihilator (Submodule.span R {x}) ≠ ⊤
⊢ ∃ P, IsAssociatedPrime P M ∧ Submodule.annihilator (Submodule.span R {x}) ≤ P
[PROOFSTEP]
obtain ⟨P, ⟨l, h₁, y, rfl⟩, h₃⟩ :=
  set_has_maximal_iff_noetherian.mpr H {P | (R ∙ x).annihilator ≤ P ∧ P ≠ ⊤ ∧ ∃ y : M, P = (R ∙ y).annihilator}
    ⟨(R ∙ x).annihilator, rfl.le, this, x, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
H : IsNoetherianRing R
x : M
hx : x ≠ 0
this : Submodule.annihilator (Submodule.span R {x}) ≠ ⊤
y : M
h₃ :
  ∀ (I : Submodule R R),
    I ∈
        {P |
          Submodule.annihilator (Submodule.span R {x}) ≤ P ∧
            P ≠ ⊤ ∧ ∃ y, P = Submodule.annihilator (Submodule.span R {y})} →
      ¬Submodule.annihilator (Submodule.span R {y}) < I
l : Submodule.annihilator (Submodule.span R {x}) ≤ Submodule.annihilator (Submodule.span R {y})
h₁ : Submodule.annihilator (Submodule.span R {y}) ≠ ⊤
⊢ ∃ P, IsAssociatedPrime P M ∧ Submodule.annihilator (Submodule.span R {x}) ≤ P
[PROOFSTEP]
refine' ⟨_, ⟨⟨h₁, _⟩, y, rfl⟩, l⟩
[GOAL]
case intro.intro.intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
H : IsNoetherianRing R
x : M
hx : x ≠ 0
this : Submodule.annihilator (Submodule.span R {x}) ≠ ⊤
y : M
h₃ :
  ∀ (I : Submodule R R),
    I ∈
        {P |
          Submodule.annihilator (Submodule.span R {x}) ≤ P ∧
            P ≠ ⊤ ∧ ∃ y, P = Submodule.annihilator (Submodule.span R {y})} →
      ¬Submodule.annihilator (Submodule.span R {y}) < I
l : Submodule.annihilator (Submodule.span R {x}) ≤ Submodule.annihilator (Submodule.span R {y})
h₁ : Submodule.annihilator (Submodule.span R {y}) ≠ ⊤
⊢ ∀ {x y_1 : R},
    x * y_1 ∈ Submodule.annihilator (Submodule.span R {y}) →
      x ∈ Submodule.annihilator (Submodule.span R {y}) ∨ y_1 ∈ Submodule.annihilator (Submodule.span R {y})
[PROOFSTEP]
intro a b hab
[GOAL]
case intro.intro.intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
H : IsNoetherianRing R
x : M
hx : x ≠ 0
this : Submodule.annihilator (Submodule.span R {x}) ≠ ⊤
y : M
h₃ :
  ∀ (I : Submodule R R),
    I ∈
        {P |
          Submodule.annihilator (Submodule.span R {x}) ≤ P ∧
            P ≠ ⊤ ∧ ∃ y, P = Submodule.annihilator (Submodule.span R {y})} →
      ¬Submodule.annihilator (Submodule.span R {y}) < I
l : Submodule.annihilator (Submodule.span R {x}) ≤ Submodule.annihilator (Submodule.span R {y})
h₁ : Submodule.annihilator (Submodule.span R {y}) ≠ ⊤
a b : R
hab : a * b ∈ Submodule.annihilator (Submodule.span R {y})
⊢ a ∈ Submodule.annihilator (Submodule.span R {y}) ∨ b ∈ Submodule.annihilator (Submodule.span R {y})
[PROOFSTEP]
rw [or_iff_not_imp_left]
[GOAL]
case intro.intro.intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
H : IsNoetherianRing R
x : M
hx : x ≠ 0
this : Submodule.annihilator (Submodule.span R {x}) ≠ ⊤
y : M
h₃ :
  ∀ (I : Submodule R R),
    I ∈
        {P |
          Submodule.annihilator (Submodule.span R {x}) ≤ P ∧
            P ≠ ⊤ ∧ ∃ y, P = Submodule.annihilator (Submodule.span R {y})} →
      ¬Submodule.annihilator (Submodule.span R {y}) < I
l : Submodule.annihilator (Submodule.span R {x}) ≤ Submodule.annihilator (Submodule.span R {y})
h₁ : Submodule.annihilator (Submodule.span R {y}) ≠ ⊤
a b : R
hab : a * b ∈ Submodule.annihilator (Submodule.span R {y})
⊢ ¬a ∈ Submodule.annihilator (Submodule.span R {y}) → b ∈ Submodule.annihilator (Submodule.span R {y})
[PROOFSTEP]
intro ha
[GOAL]
case intro.intro.intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
H : IsNoetherianRing R
x : M
hx : x ≠ 0
this : Submodule.annihilator (Submodule.span R {x}) ≠ ⊤
y : M
h₃ :
  ∀ (I : Submodule R R),
    I ∈
        {P |
          Submodule.annihilator (Submodule.span R {x}) ≤ P ∧
            P ≠ ⊤ ∧ ∃ y, P = Submodule.annihilator (Submodule.span R {y})} →
      ¬Submodule.annihilator (Submodule.span R {y}) < I
l : Submodule.annihilator (Submodule.span R {x}) ≤ Submodule.annihilator (Submodule.span R {y})
h₁ : Submodule.annihilator (Submodule.span R {y}) ≠ ⊤
a b : R
hab : a * b ∈ Submodule.annihilator (Submodule.span R {y})
ha : ¬a ∈ Submodule.annihilator (Submodule.span R {y})
⊢ b ∈ Submodule.annihilator (Submodule.span R {y})
[PROOFSTEP]
rw [Submodule.mem_annihilator_span_singleton] at ha hab 
[GOAL]
case intro.intro.intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
H : IsNoetherianRing R
x : M
hx : x ≠ 0
this : Submodule.annihilator (Submodule.span R {x}) ≠ ⊤
y : M
h₃ :
  ∀ (I : Submodule R R),
    I ∈
        {P |
          Submodule.annihilator (Submodule.span R {x}) ≤ P ∧
            P ≠ ⊤ ∧ ∃ y, P = Submodule.annihilator (Submodule.span R {y})} →
      ¬Submodule.annihilator (Submodule.span R {y}) < I
l : Submodule.annihilator (Submodule.span R {x}) ≤ Submodule.annihilator (Submodule.span R {y})
h₁ : Submodule.annihilator (Submodule.span R {y}) ≠ ⊤
a b : R
hab : (a * b) • y = 0
ha : ¬a • y = 0
⊢ b ∈ Submodule.annihilator (Submodule.span R {y})
[PROOFSTEP]
have H₁ : (R ∙ y).annihilator ≤ (R ∙ a • y).annihilator :=
  by
  intro c hc
  rw [Submodule.mem_annihilator_span_singleton] at hc ⊢
  rw [smul_comm, hc, smul_zero]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
H : IsNoetherianRing R
x : M
hx : x ≠ 0
this : Submodule.annihilator (Submodule.span R {x}) ≠ ⊤
y : M
h₃ :
  ∀ (I : Submodule R R),
    I ∈
        {P |
          Submodule.annihilator (Submodule.span R {x}) ≤ P ∧
            P ≠ ⊤ ∧ ∃ y, P = Submodule.annihilator (Submodule.span R {y})} →
      ¬Submodule.annihilator (Submodule.span R {y}) < I
l : Submodule.annihilator (Submodule.span R {x}) ≤ Submodule.annihilator (Submodule.span R {y})
h₁ : Submodule.annihilator (Submodule.span R {y}) ≠ ⊤
a b : R
hab : (a * b) • y = 0
ha : ¬a • y = 0
⊢ Submodule.annihilator (Submodule.span R {y}) ≤ Submodule.annihilator (Submodule.span R {a • y})
[PROOFSTEP]
intro c hc
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
H : IsNoetherianRing R
x : M
hx : x ≠ 0
this : Submodule.annihilator (Submodule.span R {x}) ≠ ⊤
y : M
h₃ :
  ∀ (I : Submodule R R),
    I ∈
        {P |
          Submodule.annihilator (Submodule.span R {x}) ≤ P ∧
            P ≠ ⊤ ∧ ∃ y, P = Submodule.annihilator (Submodule.span R {y})} →
      ¬Submodule.annihilator (Submodule.span R {y}) < I
l : Submodule.annihilator (Submodule.span R {x}) ≤ Submodule.annihilator (Submodule.span R {y})
h₁ : Submodule.annihilator (Submodule.span R {y}) ≠ ⊤
a b : R
hab : (a * b) • y = 0
ha : ¬a • y = 0
c : R
hc : c ∈ Submodule.annihilator (Submodule.span R {y})
⊢ c ∈ Submodule.annihilator (Submodule.span R {a • y})
[PROOFSTEP]
rw [Submodule.mem_annihilator_span_singleton] at hc ⊢
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
H : IsNoetherianRing R
x : M
hx : x ≠ 0
this : Submodule.annihilator (Submodule.span R {x}) ≠ ⊤
y : M
h₃ :
  ∀ (I : Submodule R R),
    I ∈
        {P |
          Submodule.annihilator (Submodule.span R {x}) ≤ P ∧
            P ≠ ⊤ ∧ ∃ y, P = Submodule.annihilator (Submodule.span R {y})} →
      ¬Submodule.annihilator (Submodule.span R {y}) < I
l : Submodule.annihilator (Submodule.span R {x}) ≤ Submodule.annihilator (Submodule.span R {y})
h₁ : Submodule.annihilator (Submodule.span R {y}) ≠ ⊤
a b : R
hab : (a * b) • y = 0
ha : ¬a • y = 0
c : R
hc : c • y = 0
⊢ c • a • y = 0
[PROOFSTEP]
rw [smul_comm, hc, smul_zero]
[GOAL]
case intro.intro.intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
H : IsNoetherianRing R
x : M
hx : x ≠ 0
this : Submodule.annihilator (Submodule.span R {x}) ≠ ⊤
y : M
h₃ :
  ∀ (I : Submodule R R),
    I ∈
        {P |
          Submodule.annihilator (Submodule.span R {x}) ≤ P ∧
            P ≠ ⊤ ∧ ∃ y, P = Submodule.annihilator (Submodule.span R {y})} →
      ¬Submodule.annihilator (Submodule.span R {y}) < I
l : Submodule.annihilator (Submodule.span R {x}) ≤ Submodule.annihilator (Submodule.span R {y})
h₁ : Submodule.annihilator (Submodule.span R {y}) ≠ ⊤
a b : R
hab : (a * b) • y = 0
ha : ¬a • y = 0
H₁ : Submodule.annihilator (Submodule.span R {y}) ≤ Submodule.annihilator (Submodule.span R {a • y})
⊢ b ∈ Submodule.annihilator (Submodule.span R {y})
[PROOFSTEP]
have H₂ : (Submodule.span R {a • y}).annihilator ≠ ⊤ := by
  rwa [Ne.def, Submodule.annihilator_eq_top_iff, Submodule.span_singleton_eq_bot]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
H : IsNoetherianRing R
x : M
hx : x ≠ 0
this : Submodule.annihilator (Submodule.span R {x}) ≠ ⊤
y : M
h₃ :
  ∀ (I : Submodule R R),
    I ∈
        {P |
          Submodule.annihilator (Submodule.span R {x}) ≤ P ∧
            P ≠ ⊤ ∧ ∃ y, P = Submodule.annihilator (Submodule.span R {y})} →
      ¬Submodule.annihilator (Submodule.span R {y}) < I
l : Submodule.annihilator (Submodule.span R {x}) ≤ Submodule.annihilator (Submodule.span R {y})
h₁ : Submodule.annihilator (Submodule.span R {y}) ≠ ⊤
a b : R
hab : (a * b) • y = 0
ha : ¬a • y = 0
H₁ : Submodule.annihilator (Submodule.span R {y}) ≤ Submodule.annihilator (Submodule.span R {a • y})
⊢ Submodule.annihilator (Submodule.span R {a • y}) ≠ ⊤
[PROOFSTEP]
rwa [Ne.def, Submodule.annihilator_eq_top_iff, Submodule.span_singleton_eq_bot]
[GOAL]
case intro.intro.intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
H : IsNoetherianRing R
x : M
hx : x ≠ 0
this : Submodule.annihilator (Submodule.span R {x}) ≠ ⊤
y : M
h₃ :
  ∀ (I : Submodule R R),
    I ∈
        {P |
          Submodule.annihilator (Submodule.span R {x}) ≤ P ∧
            P ≠ ⊤ ∧ ∃ y, P = Submodule.annihilator (Submodule.span R {y})} →
      ¬Submodule.annihilator (Submodule.span R {y}) < I
l : Submodule.annihilator (Submodule.span R {x}) ≤ Submodule.annihilator (Submodule.span R {y})
h₁ : Submodule.annihilator (Submodule.span R {y}) ≠ ⊤
a b : R
hab : (a * b) • y = 0
ha : ¬a • y = 0
H₁ : Submodule.annihilator (Submodule.span R {y}) ≤ Submodule.annihilator (Submodule.span R {a • y})
H₂ : Submodule.annihilator (Submodule.span R {a • y}) ≠ ⊤
⊢ b ∈ Submodule.annihilator (Submodule.span R {y})
[PROOFSTEP]
rwa [H₁.eq_of_not_lt (h₃ (R ∙ a • y).annihilator ⟨l.trans H₁, H₂, _, rfl⟩), Submodule.mem_annihilator_span_singleton,
  smul_comm, smul_smul]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
I J : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type u_3
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : Subsingleton M
⊢ associatedPrimes R M = ∅
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
inst✝⁵ : CommRing R
I J : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type u_3
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : Subsingleton M
x✝ : Ideal R
⊢ x✝ ∈ associatedPrimes R M ↔ x✝ ∈ ∅
[PROOFSTEP]
simp only [Set.mem_empty_iff_false, iff_false_iff]
[GOAL]
case h
R : Type u_1
inst✝⁵ : CommRing R
I J : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type u_3
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : Subsingleton M
x✝ : Ideal R
⊢ ¬x✝ ∈ associatedPrimes R M
[PROOFSTEP]
apply not_isAssociatedPrime_of_subsingleton
[GOAL]
R : Type u_1
inst✝⁶ : CommRing R
I J : Ideal R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsNoetherianRing R
inst✝ : Nontrivial M
⊢ Set.Nonempty (associatedPrimes R M)
[PROOFSTEP]
obtain ⟨x, hx⟩ := exists_ne (0 : M)
[GOAL]
case intro
R : Type u_1
inst✝⁶ : CommRing R
I J : Ideal R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsNoetherianRing R
inst✝ : Nontrivial M
x : M
hx : x ≠ 0
⊢ Set.Nonempty (associatedPrimes R M)
[PROOFSTEP]
obtain ⟨P, hP, _⟩ := exists_le_isAssociatedPrime_of_isNoetherianRing R x hx
[GOAL]
case intro.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
I J : Ideal R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsNoetherianRing R
inst✝ : Nontrivial M
x : M
hx : x ≠ 0
P : Ideal R
hP : IsAssociatedPrime P M
right✝ : Submodule.annihilator (Submodule.span R {x}) ≤ P
⊢ Set.Nonempty (associatedPrimes R M)
[PROOFSTEP]
exact ⟨P, hP⟩
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
h : IsAssociatedPrime I M
⊢ Submodule.annihilator ⊤ ≤ I
[PROOFSTEP]
obtain ⟨hI, x, rfl⟩ := h
[GOAL]
case intro.intro
R : Type u_1
inst✝⁴ : CommRing R
J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
x : M
hI : Ideal.IsPrime (Submodule.annihilator (Submodule.span R {x}))
⊢ Submodule.annihilator ⊤ ≤ Submodule.annihilator (Submodule.span R {x})
[PROOFSTEP]
exact Submodule.annihilator_mono le_top
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
h : IsAssociatedPrime J (R ⧸ I)
⊢ J = Ideal.radical I
[PROOFSTEP]
obtain ⟨hJ, x, e⟩ := h
[GOAL]
case intro.intro
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R ⧸ I
e : J = Submodule.annihilator (Submodule.span R {x})
⊢ J = Ideal.radical I
[PROOFSTEP]
have : x ≠ 0 := by
  rintro rfl
  apply hJ.1
  rwa [Submodule.span_singleton_eq_bot.mpr rfl, Submodule.annihilator_bot] at e 
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R ⧸ I
e : J = Submodule.annihilator (Submodule.span R {x})
⊢ x ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
e : J = Submodule.annihilator (Submodule.span R {0})
⊢ False
[PROOFSTEP]
apply hJ.1
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
e : J = Submodule.annihilator (Submodule.span R {0})
⊢ J = ⊤
[PROOFSTEP]
rwa [Submodule.span_singleton_eq_bot.mpr rfl, Submodule.annihilator_bot] at e 
[GOAL]
case intro.intro
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R ⧸ I
e : J = Submodule.annihilator (Submodule.span R {x})
this : x ≠ 0
⊢ J = Ideal.radical I
[PROOFSTEP]
obtain ⟨x, rfl⟩ := Ideal.Quotient.mkₐ_surjective R _ x
[GOAL]
case intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R
e : J = Submodule.annihilator (Submodule.span R {↑(Ideal.Quotient.mkₐ R I) x})
this : ↑(Ideal.Quotient.mkₐ R I) x ≠ 0
⊢ J = Ideal.radical I
[PROOFSTEP]
replace e : ∀ {y}, y ∈ J ↔ x * y ∈ I
[GOAL]
case e
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R
e : J = Submodule.annihilator (Submodule.span R {↑(Ideal.Quotient.mkₐ R I) x})
this : ↑(Ideal.Quotient.mkₐ R I) x ≠ 0
⊢ ∀ {y : R}, y ∈ J ↔ x * y ∈ I
[PROOFSTEP]
intro y
[GOAL]
case e
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R
e : J = Submodule.annihilator (Submodule.span R {↑(Ideal.Quotient.mkₐ R I) x})
this : ↑(Ideal.Quotient.mkₐ R I) x ≠ 0
y : R
⊢ y ∈ J ↔ x * y ∈ I
[PROOFSTEP]
rw [e, Submodule.mem_annihilator_span_singleton, ← map_smul, smul_eq_mul, mul_comm, Ideal.Quotient.mkₐ_eq_mk, ←
  Ideal.Quotient.mk_eq_mk, Submodule.Quotient.mk_eq_zero]
[GOAL]
case intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R
this : ↑(Ideal.Quotient.mkₐ R I) x ≠ 0
e : ∀ {y : R}, y ∈ J ↔ x * y ∈ I
⊢ J = Ideal.radical I
[PROOFSTEP]
apply le_antisymm
[GOAL]
case intro.intro.intro.a
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R
this : ↑(Ideal.Quotient.mkₐ R I) x ≠ 0
e : ∀ {y : R}, y ∈ J ↔ x * y ∈ I
⊢ J ≤ Ideal.radical I
[PROOFSTEP]
intro y hy
[GOAL]
case intro.intro.intro.a
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R
this : ↑(Ideal.Quotient.mkₐ R I) x ≠ 0
e : ∀ {y : R}, y ∈ J ↔ x * y ∈ I
y : R
hy : y ∈ J
⊢ y ∈ Ideal.radical I
[PROOFSTEP]
exact (hI.2 <| e.mp hy).resolve_left ((Submodule.Quotient.mk_eq_zero I).not.mp this)
[GOAL]
case intro.intro.intro.a
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R
this : ↑(Ideal.Quotient.mkₐ R I) x ≠ 0
e : ∀ {y : R}, y ∈ J ↔ x * y ∈ I
⊢ Ideal.radical I ≤ J
[PROOFSTEP]
rw [hJ.radical_le_iff]
[GOAL]
case intro.intro.intro.a
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R
this : ↑(Ideal.Quotient.mkₐ R I) x ≠ 0
e : ∀ {y : R}, y ∈ J ↔ x * y ∈ I
⊢ I ≤ J
[PROOFSTEP]
intro y hy
[GOAL]
case intro.intro.intro.a
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R
this : ↑(Ideal.Quotient.mkₐ R I) x ≠ 0
e : ∀ {y : R}, y ∈ J ↔ x * y ∈ I
y : R
hy : y ∈ I
⊢ y ∈ J
[PROOFSTEP]
exact e.mpr (I.mul_mem_left x hy)
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
I J : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type u_3
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}
[PROOFSTEP]
ext J
[GOAL]
case h
R : Type u_1
inst✝⁵ : CommRing R
I J✝ : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type u_3
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}
[PROOFSTEP]
rw [Set.mem_singleton_iff]
[GOAL]
case h
R : Type u_1
inst✝⁵ : CommRing R
I J✝ : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type u_3
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
[PROOFSTEP]
refine' ⟨IsAssociatedPrime.eq_radical hI, _⟩
[GOAL]
case h
R : Type u_1
inst✝⁵ : CommRing R
I J✝ : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type u_3
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)
[PROOFSTEP]
rintro rfl
[GOAL]
case h
R : Type u_1
inst✝⁵ : CommRing R
I J : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type u_3
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)
[PROOFSTEP]
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
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
I J : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type u_3
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsNoetherianRing R
hI : Ideal.IsPrimary I
⊢ Nontrivial (R ⧸ I)
[PROOFSTEP]
refine ⟨(Ideal.Quotient.mk I : _) 1, (Ideal.Quotient.mk I : _) 0, ?_⟩
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
I J : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type u_3
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
[PROOFSTEP]
rw [Ne.def, Ideal.Quotient.eq, sub_zero, ← Ideal.eq_top_iff_one]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
I J : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type u_3
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsNoetherianRing R
hI : Ideal.IsPrimary I
⊢ ¬I = ⊤
[PROOFSTEP]
exact hI.1
[GOAL]
case h
R : Type u_1
inst✝⁵ : CommRing R
I J : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type u_3
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)
[PROOFSTEP]
obtain ⟨a, ha⟩ := associatedPrimes.nonempty R (R ⧸ I)
[GOAL]
case h.intro
R : Type u_1
inst✝⁵ : CommRing R
I J : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type u_3
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)
[PROOFSTEP]
exact ha.eq_radical hI ▸ ha
