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✝¹ : LocalRing R
inst✝ : Module.Finite R M
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✝¹ : LocalRing R
inst✝ : Module.Finite R M
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✝¹ : LocalRing R
inst✝ : Module.Finite R M
h : I ≠ ⊤
x : M
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✝¹ : LocalRing R
inst✝ : Module.Finite R M
h : I ≠ ⊤
⊢ (⨅ (i : ℕ), I ^ i • ⊤) ≤ ⊥
intro x 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✝¹ : LocalRing R
inst✝ : Module.Finite R M
h : I ≠ ⊤
x : M
hx : x ∈ ⨅ (i : ℕ), I ^ i • ⊤
r : { x // x ∈ I }
hr : ↑r • x = x
⊢ 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✝¹ : LocalRing R
inst✝ : Module.Finite R M
h : I ≠ ⊤
x : M
hx : x ∈ ⨅ (i : ℕ), I ^ i • ⊤
⊢ x ∈ ⊥
obtain ⟨r, hr⟩ := (I.mem_iInf_smul_pow_eq_bot_iff x).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✝¹ : LocalRing R
inst✝ : Module.Finite R M
h : I ≠ ⊤
x : M
hx : x ∈ ⨅ (i : ℕ), I ^ i • ⊤
r : { x // x ∈ I }
hr : ↑r • x = x
this : IsUnit (1 - ↑r)
⊢ x ∈ ⊥
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✝¹ : LocalRing R
inst✝ : Module.Finite R M
h : I ≠ ⊤
x : M
hx : x ∈ ⨅ (i : ℕ), I ^ i • ⊤
r : { x // x ∈ I }
hr : ↑r • x = x
⊢ x ∈ ⊥
have := LocalRing.isUnit_one_sub_self_of_mem_nonunits _ (LocalRing.le_maximalIdeal h r.prop)
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✝¹ : LocalRing R
inst✝ : Module.Finite R M
h : I ≠ ⊤
x : M
hx : x ∈ ⨅ (i : ℕ), I ^ i • ⊤
r : { x // x ∈ I }
hr : ↑r • x = x
this : IsUnit (1 - ↑r)
⊢ (1 - ↑r) • x = (1 - ↑r) • 0
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✝¹ : LocalRing R
inst✝ : Module.Finite R M
h : I ≠ ⊤
x : M
hx : x ∈ ⨅ (i : ℕ), I ^ i • ⊤
r : { x // x ∈ I }
hr : ↑r • x = x
this : IsUnit (1 - ↑r)
⊢ x ∈ ⊥
apply this.smul_left_cancel.mp
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✝¹ : LocalRing R
inst✝ : Module.Finite R M
h : I ≠ ⊤
x : M
hx : x ∈ ⨅ (i : ℕ), I ^ i • ⊤
r : { x // x ∈ I }
hr : ↑r • x = x
this : IsUnit (1 - ↑r)
⊢ (1 - ↑r) • x = (1 - ↑r) • 0
simp [sub_smul, hr]