Maximal Filters in the Lattice of Partitions of an Infinite Set
David Victor Feldman, Alexander Wilce
math.GN
Aug 11, 2026 · v1
TL;DR
The paper's results were formalized and machine-checked in Lean 4 with Mathlib, using the Aristotle system; partitions are modelled as Setoids and the ultrapower as germs.
Abstract
We study maximal (proper) filters in the complete lattice of partitions of an infinite set $X$. In the language of uniform spaces, these are precisely the atoms of the lattice of zero-dimensional uniformities on $X$, introduced by Pelant and Reiterman and studied further by Pelant, Reiterman, Rödl and Simon. The first half of this paper recovers, sharpens, and extends their classification in purely partition-theoretic terms. {Call a maximal filter of partitions {\em type I} if it does not contain all finite partitions, and {\em type II} if it does.} Type I filters are induced, in an essentially unique way, by ultrafilters on families of pairwise disjoint doubletons. {A type II filter} determines a non-principal ultrafilter on $X$, the heart; the heart determines the filter precisely when {the former} is minimal in the Rudin–Keisler order. Each member $F$ of {a type II filter} gives rise to a closed fiber in $X^{*} = βX \setminus X$, {consisting of} the set of ultrafilters agreeing with the heart on $F$. We prove a trichotomy describing the topology of arbitrary fibers. We then show that the fibers do not encode the filter: fibers do not form a semilattice under intersection, the closure of an infinite discrete set of ultrafilters of a single Rudin–Keisler type (a sparse set, in our terminology) need not be a fiber, and a partition incompatible with a member of the filter may have a {fiber strictly larger than that member.} A representation that does succeed is nevertheless available in another category: the {type-II filters} with heart $\mathfrak{u}$ correspond to the maximal proper substructures of the ultrapower $X^X\!/\mathfrak{u}$ of the full structure on $X$. The topological representation problem remains open.
Problem
The paper studies maximal proper filters (parultrafilters) in the complete lattice of partitions of an infinite set. These correspond to atoms of the lattice of zero-dimensional uniformities, as studied by Pelant, Reiterman, Rödl and Simon. The aim is to classify them and to represent them topologically.
Approach
Parultrafilters are split into type I, which omit some finite partition, and type II, which contain all finite partitions. Type I filters are induced by ultrafilters on families of disjoint doubletons. Type II filters determine a non-principal ultrafilter, the heart, and closed fibers in the growth X*. The analysis uses the Rudin–Keisler order, fiber topology, and ultrapowers of the full structure on X. All results were machine-checked in Lean 4 over Mathlib, with a development archived on Zenodo.
Results
A type II filter's heart determines it exactly when the heart is Rudin–Keisler minimal. A trichotomy describes the topology of fibers. Fibers fail to encode the filter, but type-II filters with heart u correspond to maximal proper substructures of the ultrapower X^X/u. The topological representation problem is left open.