English
If F is stable, then the infimum with F' preserves stability: (F ⊓ F').Stable.
Русский
Если F стабильна, пересечение с F' сохраняет стабильность.
LaTeX
$$$ (F \\sqcap F').Stable $$$
Lean4
theorem mem_iInf_smul_pow_eq_bot_iff [IsNoetherianRing R] [Module.Finite R M] (x : M) :
x ∈ (⨅ i : ℕ, I ^ i • ⊤ : Submodule R M) ↔ ∃ r : I, (r : R) • x = x :=
by
let N := (⨅ i : ℕ, I ^ i • ⊤ : Submodule R M)
have hN : ∀ k, (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N := fun k =>
inf_eq_right.mpr ((iInf_le _ k).trans <| le_of_eq <| by simp)
constructor
· obtain ⟨r, hr₁, hr₂⟩ :=
Submodule.exists_mem_and_smul_eq_self_of_fg_of_le_smul I N (IsNoetherian.noetherian N)
(by
obtain ⟨k, hk⟩ := (I.stableFiltration_stable ⊤).inter_right (I.trivialFiltration N)
have := hk k (le_refl _)
rw [hN, hN] at this
exact le_of_eq this.symm)
intro H
exact ⟨⟨r, hr₁⟩, hr₂ _ H⟩
· rintro ⟨r, eq⟩
rw [Submodule.mem_iInf]
intro i
induction i with
| zero => simp
| succ i hi =>
rw [add_comm, pow_add, ← smul_smul, pow_one, ← eq]
exact Submodule.smul_mem_smul r.prop hi
