feat(RingTheory/IdealFilter): topologies associated to ideal filters (leanprover-community#33853)

This PR introduces topological structures on a ring arising from an IdealFilter.

Main additions:
* `IdealFilter.addGroupFilterBasis` and the induced additive group topology.
* Under `F.IsUniform`, `IdealFilter.ringFilterBasis` and the induced ring topology.
* A characterization of uniform ideal filters in terms of the existence of a `RingFilterBasis` (`isUniform_iff_exists_ringFilterBasis`).
* Neighborhood characterizations for both the additive and ring topologies.
* A proof that the resulting ring topology is linear (`IsLinearTopology`).

The construction follows the standard picture of uniform (Gabriel) filters generating linear topologies on rings, using colon ideals to witness stability under right multiplication. This provides the topological counterpart to the algebraic theory of ideal filters developed in RingTheory/IdealFilter/Basic.

Co-authored-by: blake-farman <blake.farman@gmail.com>

Author: farmanb

Mathlib.lean

@@ -6130,6 +6130,7 @@ public import Mathlib.RingTheory.Ideal.Quotient.Operations
 public import Mathlib.RingTheory.Ideal.Quotient.PowTransition
 public import Mathlib.RingTheory.Ideal.Span
 public import Mathlib.RingTheory.IdealFilter.Basic
+public import Mathlib.RingTheory.IdealFilter.Topology
 public import Mathlib.RingTheory.Idempotents
 public import Mathlib.RingTheory.Int.Basic
 public import Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Mathlib/RingTheory/IdealFilter/Basic.lean

@@ -76,7 +76,7 @@ namespace IdealFilter
 variable {A : Type*} [Ring A]
 
 /-- A filter of ideals is *uniform* if it is closed under colon by singletons. -/
-structure IsUniform (F : IdealFilter A) : Prop where
+class IsUniform (F : IdealFilter A) : Prop where
   /-- **Axiom T3.**  See [stenstrom1975]. -/
   colon_mem {I : Ideal A} (hI : I ∈ F) (a : A) : I.colon {a} ∈ F
 
@@ -166,24 +166,26 @@ scoped infixl:70 " • " => gabrielComposition
 
 /-- An ideal filter is Gabriel if it satisfies `IsUniform` and axiom T4.
 See [nLab: Gabriel filter](<https://ncatlab.org/nlab/show/Gabriel+filter>). -/
-structure IsGabriel (F : IdealFilter A) extends F.IsUniform where
+class IsGabriel (F : IdealFilter A) extends F.IsUniform where
   /-- **Axiom T4.** See [stenstrom1975]. -/
   gabriel_closed (I : Ideal A) (h : ∃ J ∈ F, ∀ x ∈ J, I.colon {x} ∈ F) : I ∈ F
 
 /-- Characterization of Gabriel filters via `IsUniform` and idempotence of
 `gabrielComposition`. -/
 theorem isGabriel_iff (F : IdealFilter A) : F.IsGabriel ↔ F.IsUniform ∧ F • F = F := by
   constructor
-  · rintro ⟨h₁, h₂⟩
-    refine ⟨h₁, ?_⟩
+  · intro hF
+    refine ⟨hF.toIsUniform, ?_⟩
     ext I
     constructor <;> intro hI
     · rcases hI with ⟨J, hJ, htors⟩
-      refine h₂ I ⟨J, hJ, fun x hx ↦ ?_⟩
+      refine hF.gabriel_closed I ⟨J, hJ, fun x hx ↦ ?_⟩
       rcases htors x hx with ⟨K, hK, hincl⟩
       exact Order.PFilter.mem_of_le hincl hK
     · exact ⟨I, hI, isTorsionQuot_self F I⟩
-  · refine fun ⟨h₁, h₂⟩ ↦ ⟨h₁, fun I ⟨J, hJ, hcolon⟩ ↦ ?_⟩
+  · rintro ⟨h₁, h₂⟩
+    refine { toIsUniform := h₁, gabriel_closed := ?_ }
+    rintro I ⟨J, hJ, hcolon⟩
     exact h₂.le ⟨J, hJ, fun x hx ↦ ⟨I.colon {x}, hcolon x hx, by simp⟩⟩
 
 end IdealFilter

Mathlib/RingTheory/IdealFilter/Topology.lean

@@ -0,0 +1,140 @@
+/-
+Copyright (c) 2025 Blake Farman. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Blake Farman
+-/
+module
+
+public import Mathlib.RingTheory.IdealFilter.Basic
+public import Mathlib.Topology.Algebra.LinearTopology
+public import Mathlib.Topology.Algebra.FilterBasis
+
+/-!
+# 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](<https://ncatlab.org/nlab/show/uniform+filter>)
+
+## Tags
+
+ring theory, ideal, filter, linear topology
+-/
+
+@[expose] public section
+
+open scoped Pointwise Topology
+
+namespace IdealFilter
+
+/-- The additive-group filter basis whose sets are the ideals belonging to the ideal filter `F`. -/
+def addGroupFilterBasis {A : Type*} [Ring A] (F : IdealFilter A) : AddGroupFilterBasis A where
+  sets := {(I : Set A) | I ∈ F}
+  nonempty := ⟨_, ⟨_, F.nonempty.choose_spec, rfl⟩⟩
+  inter_sets := by
+    rintro s t ⟨I, hI, rfl⟩ ⟨J, hJ, rfl⟩
+    exact ⟨I ⊓ J, ⟨I ⊓ J, Order.PFilter.inf_mem hI hJ, rfl⟩, fun _ h ↦ h⟩
+  zero' := by aesop
+  add' := by aesop
+  neg' := by aesop
+  conj' := by aesop
+
+/-- Under `[F.IsUniform]`, the ring filter basis obtained from `addGroupFilterBasis`. -/
+@[simps! -isSimp sets]
+def ringFilterBasis {A : Type*} [Ring A] {F : IdealFilter A} [F.IsUniform] :
+    RingFilterBasis A where
+  __ := F.addGroupFilterBasis
+  mul' := by
+    rintro U ⟨I, hI, rfl⟩
+    exact ⟨I, ⟨I, hI, rfl⟩, Set.mul_subset_iff.mpr fun _ h₁ _ h₂ ↦ mul_mem h₁ h₂⟩
+  mul_left' := by
+    rintro x₀ U ⟨I, hI, rfl⟩
+    exact ⟨I, ⟨I, hI, rfl⟩, fun a ha ↦ Ideal.mul_mem_left I x₀ ha⟩
+  mul_right' := by
+    rintro x₀ U ⟨I, hI, rfl⟩
+    refine ⟨I.colon {x₀}, ⟨I.colon {x₀}, IsUniform.colon_mem hI x₀, rfl⟩,
+      fun a ha ↦ Set.mem_preimage.mpr (Submodule.mem_colon_singleton.mp ha)⟩
+
+/-- An `IdealFilter` on a ring `A` is uniform if and only if its ideals form a `RingFilterBasis`
+for `A`. -/
+theorem isUniform_iff_exists_ringFilterBasis {A : Type*} [Ring A] {F : IdealFilter A} :
+    F.IsUniform ↔ ∃ B : RingFilterBasis A, B.sets = {(I : Set A) | I ∈ F} := by
+  refine ⟨fun _ ↦ ⟨F.ringFilterBasis, rfl⟩, fun ⟨B, hB⟩ ↦ ⟨fun {I} hI a ↦ ?_⟩⟩
+  obtain ⟨V, hbasis, hsub⟩ := B.mul_right a (U := I) (hB.ge (by simpa))
+  obtain ⟨J, hJ, rfl⟩ := hB.le hbasis
+  exact Order.PFilter.mem_of_le (fun x hx ↦ by simpa using (hsub hx)) hJ
+
+end IdealFilter
+
+/-- 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. -/
+@[nolint unusedArguments]
+def WithIdealFilter {A : Type*} [Ring A] : IdealFilter A → Type _ := fun _ => A
+
+namespace WithIdealFilter
+
+open IdealFilter
+
+variable {A : Type*} [Ring A] {F : IdealFilter A}
+
+instance instRing : Ring (WithIdealFilter F) := inferInstanceAs (Ring A)
+
+/-- View an ideal of `A` as a subset of `WithIdealFilter F`. -/
+abbrev idealSet (I : Ideal A) : Set (WithIdealFilter F) := (I : Set A)
+
+/-- The topology on `A` induced by `addGroupFilterBasis`. -/
+instance instTopologicalSpace : TopologicalSpace (WithIdealFilter F) :=
+  F.addGroupFilterBasis.topology
+
+/-- The topology `F.addGroupFilterBasis.topology` endows `A` with the structure of a topological
+additive group. -/
+instance instIsTopologicalAddGroup : IsTopologicalAddGroup (WithIdealFilter F) :=
+  F.addGroupFilterBasis.isTopologicalAddGroup
+
+/-- A set `s` is a neighbourhood of `a` iff it contains a left-additive coset of some ideal
+`I ∈ F`. -/
+lemma mem_nhds_iff {a : (WithIdealFilter F)} {s : Set (WithIdealFilter F)} :
+    s ∈ 𝓝 a ↔ ∃ I ∈ F, a +ᵥ idealSet I ⊆ s := by
+  constructor
+  · intro hs
+    rcases ((F.addGroupFilterBasis).nhds_hasBasis a).mem_iff.1 hs with ⟨t, ht, hts⟩
+    rcases ht with ⟨I, hI, rfl⟩
+    exact ⟨I, hI, hts⟩
+  · rintro ⟨I, hI, hIs⟩
+    refine ((F.addGroupFilterBasis).nhds_hasBasis a).mem_iff.2 ?_
+    exact ⟨I, ⟨I, hI, rfl⟩, hIs⟩
+
+/-- A set `s` is a neighbourhood of `0` iff it contains an ideal belonging to `F`. -/
+lemma mem_nhds_zero_iff {s : Set (WithIdealFilter F)} :
+    s ∈ 𝓝 0 ↔ ∃ I ∈ F, idealSet I ⊆ s := by
+  simpa [zero_vadd] using mem_nhds_iff (a := 0) (s := s)
+
+/-- The topology is linear in the sense that `𝓝 0` has a basis of ideals. -/
+instance instIsLinearTopology : IsLinearTopology (WithIdealFilter F) (WithIdealFilter F) :=
+  IsLinearTopology.mk_of_hasBasis' (R := (WithIdealFilter F))
+    (M := (WithIdealFilter F))
+    (ι := Ideal A) (S := Ideal A)
+    (p := fun I : Ideal A ↦ I ∈ F) (s := fun I : Ideal A ↦ I)
+    ⟨fun _ ↦ mem_nhds_zero_iff⟩
+    (fun I a _ hm ↦ Submodule.smul_mem I a hm)
+
+/-- Under `[F.IsUniform]`, `A` is a topological ring with the induced topology. -/
+instance instIsTopologicalRing [F.IsUniform] : IsTopologicalRing (WithIdealFilter F) :=
+  F.ringFilterBasis.isTopologicalRing
+
+end WithIdealFilter