The filtration on abelian groups and rings

In this file, we define the concept of filtration for abelian groups, rings, and modules.

Main definitions

• IsFiltration : For a family of subsets σ of A, an increasing series of F in σ is a filtration if there is another series F_lt in σ equal to the supremum of F with smaller index.

• IsRingFiltration : For a family of subsets σ of semiring R, an increasing series F in σ is a ring filtration if IsFiltration F F_lt and the pointwise multiplication of F i and F j is in F (i + j).

• IsModuleFiltration : For F satisfying IsRingFiltration F F_lt in a semiring R and σM a family of subsets of an R-module M, an increasing series FM in σM is a module filtration if IsFiltration F F_lt and the pointwise scalar multiplication of F i and FM j is in F (i +ᵥ j).

class IsFiltration {ι : Type u_1} {σ : Type u_3} [Preorder ι] [Preorder σ] (F : ι → σ) (F_lt : outParam (ι → σ)) : Prop

For a family of subsets σ of A, an increasing series of F in σ is a filtration if there is another series F_lt in σ equal to the supremum of F with smaller index.

In the intended applications, σ is a complete lattice, and F_lt is uniquely-determined as F_lt j = ⨆ i < j, F i. Thus F_lt is an implementation detail which allows us defer depending on a complete lattice structure on σ. It also provides the ancillary benefit of giving us better definition control. This is convenient e.g., when the index is ℤ.

• mono : Monotone F
• is_le {i j : ι} : i < j → F i ≤ F_lt j
• is_sup (B : σ) (j : ι) : (∀ i < j, F i ≤ B) → F_lt j ≤ B

theorem IsFiltration.F_lt_le_F {ι : Type u_1} {σ : Type u_3} [Preorder ι] [Preorder σ] (F : ι → σ) (F_lt : outParam (ι → σ)) (i : ι) [IsFiltration F F_lt] : F_lt i ≤ F i

theorem IsFiltration.mk_int {σ : Type u_3} [Preorder σ] (F : ℤ → σ) (mono : Monotone F) : IsFiltration F fun (n : ℤ) => F (n - 1)

A convenience constructor for IsFiltration when the index is the integers.

class IsRingFiltration {ι : Type u_1} {R : Type u_2} {σ : Type u_3} [AddMonoid ι] [PartialOrder ι] [Preorder σ] [Semiring R] [SetLike σ R] (F : ι → σ) (F_lt : outParam (ι → σ)) extends IsFiltration F F_lt, SetLike.GradedMonoid F : Prop

For a family of subsets σ of semiring R, an increasing series F in σ is a ring filtration if IsFiltration F F_lt and the pointwise multiplication of F i and F j is in F (i + j).

• mono : Monotone F
• is_le {i j : ι} : i < j → F i ≤ F_lt j
• is_sup (B : σ) (j : ι) : (∀ i < j, F i ≤ B) → F_lt j ≤ B
• one_mem : 1 ∈ F 0
• mul_mem ⦃i j : ι⦄ {gi gj : R} : gi ∈ F i → gj ∈ F j → gi * gj ∈ F (i + j)

theorem IsRingFiltration.mk_int {R : Type u_2} {σ : Type u_3} [Preorder σ] [Semiring R] [SetLike σ R] (F : ℤ → σ) (mono : Monotone F) [SetLike.GradedMonoid F] : IsRingFiltration F fun (n : ℤ) => F (n - 1)

A convenience constructor for IsRingFiltration when the index is the integers.

class IsModuleFiltration {ι : Type u_1} {ιM : Type u_2} {R : Type u_3} {M : Type u_4} {σ : Type u_5} {σM : Type u_6} [AddMonoid ι] [PartialOrder ι] [PartialOrder ιM] [VAdd ι ιM] [Preorder σ] [Semiring R] [SetLike σ R] [Preorder σM] [AddCommMonoid M] [Module R M] [SetLike σM M] (F : ι → σ) (F_lt : outParam (ι → σ)) [IsRingFiltration F F_lt] (F' : ιM → σM) (F'_lt : outParam (ιM → σM)) extends IsFiltration F' F'_lt, SetLike.GradedSMul F F' : Prop

For F satisfying IsRingFiltration F F_lt in a semiring R and σM a family of subsets of an R-module M, an increasing series FM in σM is a module filtration if IsFiltration F F_lt and the pointwise scalar multiplication of F i and FM j is in F (i +ᵥ j).

The index set ιM for the module can be more general, however usually we take ιM = ι.

• mono : Monotone F'
• is_le {i j : ιM} : i < j → F' i ≤ F'_lt j
• is_sup (B : σM) (j : ιM) : (∀ i < j, F' i ≤ B) → F'_lt j ≤ B
• smul_mem ⦃i : ι⦄ ⦃j : ιM⦄ {ai : R} {bj : M} : ai ∈ F i → bj ∈ F' j → ai • bj ∈ F' (i +ᵥ j)

theorem IsModuleFiltration.mk_int {R : Type u_3} {M : Type u_4} {σ : Type u_5} {σM : Type u_6} [Preorder σ] [Semiring R] [SetLike σ R] [Preorder σM] [AddCommMonoid M] [Module R M] [SetLike σM M] (F : ℤ → σ) (mono : Monotone F) [SetLike.GradedMonoid F] (F' : ℤ → σM) (mono' : Monotone F') [SetLike.GradedSMul F F'] : IsModuleFiltration F (fun (n : ℤ) => F (n - 1)) F' fun (n : ℤ) => F' (n - 1)

A convenience constructor for IsModuleFiltration when the index is the integers.