Ideal Filters

An ideal filter is a filter in the lattice of ideals of a ring A.

Main definitions

• IdealFilter A: the type of an ideal filter on a ring A.
• IsUniform F : a filter F is uniform if whenever I is an ideal in the filter, then for all a : A, the colon ideal I.colon {a} is in F.
• IsTorsionElem : Given a filter F, an element, m, of an A-module, M, is F-torsion if there exists an ideal L in F that annihilates m.
• IsTorsion : Given a filter F, an A-module, M, is F-torsion if every element is torsion.
• gabrielComposition : Given two filters F and G, the Gabriel composition of F and G is the set of ideals L of A such that there exists an ideal K in G with K/L F-torsion. This is again a filter.
• IsGabriel F : a filter F is a Gabriel filter if it is uniform and satisfies axiom T4: for all I : Ideal A, if there exists J ∈ F such that for all a ∈ J the colon ideal I.colon {a} is in F, then I ∈ F.

Main statements

• isGabriel_iff: a filter is Gabriel iff it is uniform and F • F = F.

Notation

• F • G: the Gabriel composition of ideal filters F and G, defined by gabrielComposition F G.

Implementation notes

In the classical literature (e.g. Stenström), right linear topologies on a ring are often described via filters of open right ideals, and the terminology is frequently abused by identifying the topology with its filter of ideals.

In this development we work systematically with left ideals. Accordingly, Stenström’s right-ideal construction (L : a) = {x ∈ A | a * x ∈ L} is replaced by the left ideal L.colon {a} = {a | x * a ∈ L}.

With this convention, uniform filters correspond to linear (additive) topologies, while the additional Gabriel condition (axiom T4) imposes an algebraic saturation property that does not change the induced topology.

References

• Bo Stenström, Rings and Modules of Quotients
• Bo Stenström, Rings of Quotients
• nLab: Uniform filter
• nLab: Gabriel filter
• nLab: Gabriel composition

Tags

ring theory, ideal, filter, uniform filter, Gabriel filter, torsion theory

@[reducible, inline]

abbrev IdealFilter (A : Type u_1) [Ring A] : Type u_1

IdealFilter A is the type of Order.PFilters on the lattice of ideals of A.

Equations

• IdealFilter A = Order.PFilter (Ideal A)

structure IdealFilter.IsUniform {A : Type u_1} [Ring A] (F : IdealFilter A) : Prop

A filter of ideals is uniform if it is closed under colon by singletons.

• colon_mem {I : Ideal A} (hI : I ∈ F) (a : A) : Submodule.colon I {a} ∈ F

  Axiom T3. See [Ste75].

def IdealFilter.IsTorsionElem {A : Type u_1} [Ring A] (F : IdealFilter A) {M : Type u_2} [AddCommMonoid M] [Module A M] (m : M) : Prop

We say that an element m : M is F-torsion if it is annihilated by some ideal belonging to the filter F.

Equations

• F.IsTorsionElem m = ∃ L ∈ F, ∀ a ∈ L, a • m = 0

def IdealFilter.IsTorsion {A : Type u_1} [Ring A] (F : IdealFilter A) (M : Type u_2) [AddCommMonoid M] [Module A M] : Prop

Module-level F-torsion: every element is F-torsion.

Equations

• F.IsTorsion M = ∀ (m : M), F.IsTorsionElem m

def IdealFilter.IsTorsionQuot {A : Type u_1} [Ring A] (F : IdealFilter A) (L K : Ideal A) : Prop

We say that the quotient K/L is F-torsion if every element k ∈ K is annihilated (modulo L) by some ideal in F. Equivalently, for each k ∈ K there exists I ∈ F such that I ≤ L.colon {k}. This formulation avoids forming the quotient module explicitly.

Equations

• F.IsTorsionQuot L K = ∀ k ∈ K, ∃ I ∈ F, I ≤ Submodule.colon L {k}

theorem IdealFilter.isTorsionQuot_inter_left_iff {A : Type u_1} [Ring A] {F : IdealFilter A} {L K : Ideal A} : F.IsTorsionQuot (L ⊓ K) K ↔ F.IsTorsionQuot L K

Intersecting the left ideal with K does not change IsTorsionQuot on the right. In particular, IsTorsionQuot F L K need not require L ≤ K for it is equivalent to asserting the quotient K / (L ⊓ K) is F-torsion.

@[simp]

theorem IdealFilter.isTorsion_def {A : Type u_1} [Ring A] (F : IdealFilter A) (M : Type u_2) [AddCommMonoid M] [Module A M] : F.IsTorsion M ↔ ∀ (m : M), F.IsTorsionElem m

@[simp]

theorem IdealFilter.isTorsionQuot_def {A : Type u_1} [Ring A] {F : IdealFilter A} {L K : Ideal A} : F.IsTorsionQuot L K ↔ ∀ k ∈ ↑K, ∃ I ∈ F, I ≤ Submodule.colon L {k}

theorem IdealFilter.isTorsionQuot_self {A : Type u_1} [Ring A] (F : IdealFilter A) (I : Ideal A) : F.IsTorsionQuot I I

theorem IdealFilter.IsTorsionQuot.mono_left {A : Type u_1} [Ring A] {F : IdealFilter A} {I J K : Ideal A} (hIJ : I ≤ J) (hIK : F.IsTorsionQuot I K) : F.IsTorsionQuot J K

theorem IdealFilter.IsTorsionQuot.anti_right {A : Type u_1} [Ring A] {F : IdealFilter A} {I J K : Ideal A} (hJK : J ≤ K) (hIK : F.IsTorsionQuot I K) : F.IsTorsionQuot I J

theorem IdealFilter.IsTorsionQuot.mono {A : Type u_1} [Ring A] {F : IdealFilter A} {I J K L : Ideal A} (hIK : F.IsTorsionQuot I K) (hIJ : I ≤ J) (hLK : L ≤ K) : F.IsTorsionQuot J L

theorem IdealFilter.IsTorsionQuot.inf {A : Type u_1} [Ring A] {F : IdealFilter A} {I J K : Ideal A} (hI : F.IsTorsionQuot I K) (hJ : F.IsTorsionQuot J K) : F.IsTorsionQuot (I ⊓ J) K

theorem IdealFilter.isPFilter_gabrielComposition {A : Type u_1} [Ring A] (F G : IdealFilter A) : Order.IsPFilter {L : Ideal A | ∃ K ∈ G, F.IsTorsionQuot L K}

def IdealFilter.gabrielComposition {A : Type u_1} [Ring A] (F G : IdealFilter A) : IdealFilter A

The Gabriel composition of ideal filters F and G. See nLab: Gabriel composition.

Equations

• F.gabrielComposition G = ⋯.toPFilter

def IdealFilter.«term_•_» : Lean.TrailingParserDescr

F • G is the Gabriel composition of ideal filters F and G.

Equations

• IdealFilter.«term_•_» = Lean.ParserDescr.trailingNode `IdealFilter.«term_•_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " • ") (Lean.ParserDescr.cat `term 71))

structure IdealFilter.IsGabriel {A : Type u_1} [Ring A] (F : IdealFilter A) extends F.IsUniform : Prop

An ideal filter is Gabriel if it satisfies IsUniform and axiom T4. See nLab: Gabriel filter.

• colon_mem {I : Ideal A} (hI : I ∈ F) (a : A) : Submodule.colon I {a} ∈ F
• gabriel_closed (I : Ideal A) (h : ∃ J ∈ F, ∀ x ∈ J, Submodule.colon I {x} ∈ F) : I ∈ F

  Axiom T4. See [Ste75].

theorem IdealFilter.isGabriel_iff {A : Type u_1} [Ring A] (F : IdealFilter A) : F.IsGabriel ↔ F.IsUniform ∧ F.gabrielComposition F = F

Characterization of Gabriel filters via IsUniform and idempotence of gabrielComposition.