R M : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
F F' : Filtration I M
inst✝¹ : IsNoetherianRing R
inst✝ : IsDomain R
h : I ≠ ⊤
⊢ (⨅ (i : ℕ), I ^ i) ≤ ⊥
R M : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
F F' : Filtration I M
inst✝¹ : IsNoetherianRing R
inst✝ : IsDomain R
h : I ≠ ⊤
⊢ (⨅ (i : ℕ), I ^ i) = ⊥
rw [eq_bot_iff]
R M : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
F F' : Filtration I M
inst✝¹ : IsNoetherianRing R
inst✝ : IsDomain R
h : I ≠ ⊤
x : R
hx : x ∈ ⨅ (i : ℕ), I ^ i
⊢ x ∈ ⊥
R M : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
F F' : Filtration I M
inst✝¹ : IsNoetherianRing R
inst✝ : IsDomain R
h : I ≠ ⊤
⊢ (⨅ (i : ℕ), I ^ i) ≤ ⊥
intro x hx
R M : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
F F' : Filtration I M
inst✝¹ : IsNoetherianRing R
inst✝ : IsDomain R
h : I ≠ ⊤
x : R
hx : x ∈ ⨅ (i : ℕ), I ^ i
hx' : ¬x ∈ ⊥
⊢ False
R M : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
F F' : Filtration I M
inst✝¹ : IsNoetherianRing R
inst✝ : IsDomain R
h : I ≠ ⊤
x : R
hx : x ∈ ⨅ (i : ℕ), I ^ i
⊢ x ∈ ⊥
by_contra hx'
R M : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
F F' : Filtration I M
inst✝¹ : IsNoetherianRing R
inst✝ : IsDomain R
h : I ≠ ⊤
x : R
hx : x ∈ ⨅ (i : ℕ), I ^ i
hx' : ¬x ∈ ⊥
this : (x ∈ ⨅ (i : ℕ), I ^ i • ⊤) ↔ ∃ r, ↑r • x = x
⊢ False
R M : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
F F' : Filtration I M
inst✝¹ : IsNoetherianRing R
inst✝ : IsDomain R
h : I ≠ ⊤
x : R
hx : x ∈ ⨅ (i : ℕ), I ^ i
hx' : ¬x ∈ ⊥
⊢ False
have := Ideal.mem_iInf_smul_pow_eq_bot_iff I x
R M : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
F F' : Filtration I M
inst✝¹ : IsNoetherianRing R
inst✝ : IsDomain R
h : I ≠ ⊤
x : R
hx : x ∈ ⨅ (i : ℕ), I ^ i
hx' : ¬x ∈ ⊥
this : (x ∈ ⨅ (i : ℕ), I ^ i) ↔ ∃ r, ↑r * x = x
⊢ False
R M : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
F F' : Filtration I M
inst✝¹ : IsNoetherianRing R
inst✝ : IsDomain R
h : I ≠ ⊤
x : R
hx : x ∈ ⨅ (i : ℕ), I ^ i
hx' : ¬x ∈ ⊥
this : (x ∈ ⨅ (i : ℕ), I ^ i • ⊤) ↔ ∃ r, ↑r • x = x
⊢ False
simp_rw [smul_eq_mul, ← Ideal.one_eq_top, mul_one] at this
case intro
R M : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
F F' : Filtration I M
inst✝¹ : IsNoetherianRing R
inst✝ : IsDomain R
h : I ≠ ⊤
x : R
hx : x ∈ ⨅ (i : ℕ), I ^ i
hx' : ¬x ∈ ⊥
this : (x ∈ ⨅ (i : ℕ), I ^ i) ↔ ∃ r, ↑r * x = x
r : { x // x ∈ I }
hr : ↑r * x = x
⊢ False
R M : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
F F' : Filtration I M
inst✝¹ : IsNoetherianRing R
inst✝ : IsDomain R
h : I ≠ ⊤
x : R
hx : x ∈ ⨅ (i : ℕ), I ^ i
hx' : ¬x ∈ ⊥
this : (x ∈ ⨅ (i : ℕ), I ^ i) ↔ ∃ r, ↑r * x = x
⊢ False
obtain ⟨r, hr⟩ := this.mp hx
case intro
R M : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
F F' : Filtration I M
inst✝¹ : IsNoetherianRing R
inst✝ : IsDomain R
h : I ≠ ⊤
x : R
hx : x ∈ ⨅ (i : ℕ), I ^ i
hx' : ¬x ∈ ⊥
this✝ : (x ∈ ⨅ (i : ℕ), I ^ i) ↔ ∃ r, ↑r * x = x
r : { x // x ∈ I }
hr : ↑r * x = x
this : ↑r = 1
⊢ False
case intro
R M : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
F F' : Filtration I M
inst✝¹ : IsNoetherianRing R
inst✝ : IsDomain R
h : I ≠ ⊤
x : R
hx : x ∈ ⨅ (i : ℕ), I ^ i
hx' : ¬x ∈ ⊥
this : (x ∈ ⨅ (i : ℕ), I ^ i) ↔ ∃ r, ↑r * x = x
r : { x // x ∈ I }
hr : ↑r * x = x
⊢ False
have := mul_right_cancel₀ hx' (hr.trans (one_mul x).symm)
no goals
case intro
R M : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
F F' : Filtration I M
inst✝¹ : IsNoetherianRing R
inst✝ : IsDomain R
h : I ≠ ⊤
x : R
hx : x ∈ ⨅ (i : ℕ), I ^ i
hx' : ¬x ∈ ⊥
this✝ : (x ∈ ⨅ (i : ℕ), I ^ i) ↔ ∃ r, ↑r * x = x
r : { x // x ∈ I }
hr : ↑r * x = x
this : ↑r = 1
⊢ False
exact I.eq_top_iff_one.not.mp h (this ▸ r.prop)