English
The SupSet construction yields a filtration whose N-component is the sup of the N-components over the set.
Русский
Конструкция supSet задаёт фильтрацию, у которой компонент N является наибольшим объединением N-компонентов по множеству.
LaTeX
$$N = sSup (N '' S)$$
Lean4
/-- The `sSup` of a family of `I.Filtration`s is an `I.Filtration`. -/
instance : SupSet (I.Filtration M) :=
⟨fun S =>
{ N := sSup (Ideal.Filtration.N '' S)
mono := fun i => by
apply sSup_le_sSup_of_isCofinalFor _
rintro _ ⟨⟨_, F, hF, rfl⟩, rfl⟩
exact ⟨_, ⟨⟨_, F, hF, rfl⟩, rfl⟩, F.mono i⟩
smul_le := fun i => by
rw [sSup_eq_iSup', iSup_apply, Submodule.smul_iSup, iSup_apply]
apply iSup_mono _
rintro ⟨_, F, hF, rfl⟩
exact F.smul_le i }⟩
