case a
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
⊢ AddSubmonoid.closure (⋃ (i : ℕ), ↑(single R i) '' ↑(N F i)) ≤ (Filtration.submodule F).toAddSubmonoid

case a
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
⊢ (Filtration.submodule F).toAddSubmonoid ≤ AddSubmonoid.closure (⋃ (i : ℕ), ↑(single R i) '' ↑(N F i))
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
⊢ AddSubmonoid.closure (⋃ (i : ℕ), ↑(single R i) '' ↑(N F i)) = (Filtration.submodule F).toAddSubmonoid
apply le_antisymm
case a
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
⊢ ∀ (i : ℕ), ↑(single R i) '' ↑(N F i) ⊆ ↑(Filtration.submodule F).toAddSubmonoid
case a
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
⊢ AddSubmonoid.closure (⋃ (i : ℕ), ↑(single R i) '' ↑(N F i)) ≤ (Filtration.submodule F).toAddSubmonoid
rw [AddSubmonoid.closure_le, Set.iUnion_subset_iff]
case a.intro.intro
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
i : ℕ
m : M
hm : m ∈ ↑(N F i)
j : ℕ
⊢ ↑(↑(single R i) m) j ∈ N F j
case a
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
⊢ ∀ (i : ℕ), ↑(single R i) '' ↑(N F i) ⊆ ↑(Filtration.submodule F).toAddSubmonoid
rintro i _ ⟨m, hm, rfl⟩ j
case a.intro.intro
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
i : ℕ
m : M
hm : m ∈ ↑(N F i)
j : ℕ
⊢ (if i = j then m else 0) ∈ N F j
case a.intro.intro
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
i : ℕ
m : M
hm : m ∈ ↑(N F i)
j : ℕ
⊢ ↑(↑(single R i) m) j ∈ N F j
rw [single_apply]
case a.intro.intro.inl
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h✝ : Stable F
i : ℕ
m : M
hm : m ∈ ↑(N F i)
j : ℕ
h : i = j
⊢ m ∈ N F j

case a.intro.intro.inr
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h✝ : Stable F
i : ℕ
m : M
hm : m ∈ ↑(N F i)
j : ℕ
h : ¬i = j
⊢ 0 ∈ N F j
case a.intro.intro
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
i : ℕ
m : M
hm : m ∈ ↑(N F i)
j : ℕ
⊢ (if i = j then m else 0) ∈ N F j
split_ifs with h
no goals
case a.intro.intro.inl
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h✝ : Stable F
i : ℕ
m : M
hm : m ∈ ↑(N F i)
j : ℕ
h : i = j
⊢ m ∈ N F j
rwa [← h]
no goals
case a.intro.intro.inr
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h✝ : Stable F
i : ℕ
m : M
hm : m ∈ ↑(N F i)
j : ℕ
h : ¬i = j
⊢ 0 ∈ N F j
exact (F.N j).zero_mem
case a
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
f : PolynomialModule R M
hf : f ∈ (Filtration.submodule F).toAddSubmonoid
⊢ f ∈ AddSubmonoid.closure (⋃ (i : ℕ), ↑(single R i) '' ↑(N F i))
case a
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
⊢ (Filtration.submodule F).toAddSubmonoid ≤ AddSubmonoid.closure (⋃ (i : ℕ), ↑(single R i) '' ↑(N F i))
intro f hf
case a
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
f : PolynomialModule R M
hf : f ∈ (Filtration.submodule F).toAddSubmonoid
⊢ Finsupp.sum f Finsupp.single ∈ AddSubmonoid.closure (⋃ (i : ℕ), ↑(single R i) '' ↑(N F i))
case a
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
f : PolynomialModule R M
hf : f ∈ (Filtration.submodule F).toAddSubmonoid
⊢ f ∈ AddSubmonoid.closure (⋃ (i : ℕ), ↑(single R i) '' ↑(N F i))
rw [← f.sum_single]
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
f : PolynomialModule R M
hf : f ∈ (Filtration.submodule F).toAddSubmonoid
⊢ ∀ (c : ℕ), c ∈ f.support → Finsupp.single c (↑f c) ∈ AddSubmonoid.closure (⋃ (i : ℕ), ↑(single R i) '' ↑(N F i))
case a
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
f : PolynomialModule R M
hf : f ∈ (Filtration.submodule F).toAddSubmonoid
⊢ Finsupp.sum f Finsupp.single ∈ AddSubmonoid.closure (⋃ (i : ℕ), ↑(single R i) '' ↑(N F i))
apply AddSubmonoid.sum_mem _ _
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
f : PolynomialModule R M
hf : f ∈ (Filtration.submodule F).toAddSubmonoid
c : ℕ
⊢ Finsupp.single c (↑f c) ∈ AddSubmonoid.closure (⋃ (i : ℕ), ↑(single R i) '' ↑(N F i))
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
f : PolynomialModule R M
hf : f ∈ (Filtration.submodule F).toAddSubmonoid
⊢ ∀ (c : ℕ), c ∈ f.support → Finsupp.single c (↑f c) ∈ AddSubmonoid.closure (⋃ (i : ℕ), ↑(single R i) '' ↑(N F i))
rintro c -
no goals
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
f : PolynomialModule R M
hf : f ∈ (Filtration.submodule F).toAddSubmonoid
c : ℕ
⊢ Finsupp.single c (↑f c) ∈ AddSubmonoid.closure (⋃ (i : ℕ), ↑(single R i) '' ↑(N F i))
exact AddSubmonoid.subset_closure (Set.subset_iUnion _ c <| Set.mem_image_of_mem _ (hf c))