Topologies associated to ideal filters

This file constructs topological structures on a ring from an IdealFilter and characterizes uniform ideal filters in terms of ring filter bases.

Main definitions

• WithIdealFilter: Type synonym for a ring that depends on a choice of ideal filter. This can be used to assign and infer instances on a ring that depend on an ideal filter.
• IdealFilter.addGroupFilterBasis: the AddGroupFilterBasis with sets the ideals of F.
• IdealFilter.ringFilterBasis: under [F.IsUniform], the RingFilterBasis with sets the ideals of F.

Main statements

• IdealFilter.isUniform_iff_exists_ringFilterBasis: An IdealFilter on a ring A is uniform if and only if its ideals form a RingFilterBasis for A.

References

• nLab: Uniform filter

Tags

ring theory, ideal, filter, linear topology

def IdealFilter.addGroupFilterBasis {A : Type u_1} [Ring A] (F : IdealFilter A) : AddGroupFilterBasis A

The additive-group filter basis whose sets are the ideals belonging to the ideal filter F.

Equations

• F.addGroupFilterBasis = { sets := {x : Set A | ∃ I ∈ F, ↑I = x}, nonempty := ⋯, inter_sets := ⋯, zero' := ⋯, add' := ⋯, neg' := ⋯, conj' := ⋯ }

def IdealFilter.ringFilterBasis {A : Type u_1} [Ring A] {F : IdealFilter A} [F.IsUniform] : RingFilterBasis A

Under [F.IsUniform], the ring filter basis obtained from addGroupFilterBasis.

Equations

• IdealFilter.ringFilterBasis = { toAddGroupFilterBasis := F.addGroupFilterBasis, mul' := ⋯, mul_left' := ⋯, mul_right' := ⋯ }

theorem IdealFilter.ringFilterBasis_sets {A : Type u_1} [Ring A] {F : IdealFilter A} [F.IsUniform] : ringFilterBasis.sets = {x : Set A | ∃ I ∈ F, ↑I = x}

theorem IdealFilter.isUniform_iff_exists_ringFilterBasis {A : Type u_1} [Ring A] {F : IdealFilter A} : F.IsUniform ↔ ∃ (B : RingFilterBasis A), B.sets = {x : Set A | ∃ I ∈ F, ↑I = x}

An IdealFilter on a ring A is uniform if and only if its ideals form a RingFilterBasis for A.

def WithIdealFilter {A : Type u_1} [Ring A] : IdealFilter A → Type u_1

Type synonym for a ring that depends on a choice of ideal filter. We use this to assign a topology generated by the ideal filter.

Equations

• WithIdealFilter x✝ = A

instance WithIdealFilter.instRing {A : Type u_1} [Ring A] {F : IdealFilter A} : Ring (WithIdealFilter F)

Equations

• WithIdealFilter.instRing = inferInstanceAs (Ring A)

@[reducible, inline]

abbrev WithIdealFilter.idealSet {A : Type u_1} [Ring A] {F : IdealFilter A} (I : Ideal A) : Set (WithIdealFilter F)

View an ideal of A as a subset of WithIdealFilter F.

Equations

• WithIdealFilter.idealSet I = ↑I

instance WithIdealFilter.instTopologicalSpace {A : Type u_1} [Ring A] {F : IdealFilter A} : TopologicalSpace (WithIdealFilter F)

The topology on A induced by addGroupFilterBasis.

Equations

• WithIdealFilter.instTopologicalSpace = F.addGroupFilterBasis.topology

instance WithIdealFilter.instIsTopologicalAddGroup {A : Type u_1} [Ring A] {F : IdealFilter A} : IsTopologicalAddGroup (WithIdealFilter F)

The topology F.addGroupFilterBasis.topology endows A with the structure of a topological additive group.

theorem WithIdealFilter.mem_nhds_iff {A : Type u_1} [Ring A] {F : IdealFilter A} {a : WithIdealFilter F} {s : Set (WithIdealFilter F)} : s ∈ nhds a ↔ ∃ I ∈ F, a +ᵥ idealSet I ⊆ s

A set s is a neighbourhood of a iff it contains a left-additive coset of some ideal I ∈ F.

theorem WithIdealFilter.mem_nhds_zero_iff {A : Type u_1} [Ring A] {F : IdealFilter A} {s : Set (WithIdealFilter F)} : s ∈ nhds 0 ↔ ∃ I ∈ F, idealSet I ⊆ s

A set s is a neighbourhood of 0 iff it contains an ideal belonging to F.

instance WithIdealFilter.instIsLinearTopology {A : Type u_1} [Ring A] {F : IdealFilter A} : IsLinearTopology (WithIdealFilter F) (WithIdealFilter F)

The topology is linear in the sense that 𝓝 0 has a basis of ideals.

instance WithIdealFilter.instIsTopologicalRing {A : Type u_1} [Ring A] {F : IdealFilter A} [F.IsUniform] : IsTopologicalRing (WithIdealFilter F)

Under [F.IsUniform], A is a topological ring with the induced topology.