Irreducibility in topological spaces #
Main definitions #
IrreducibleSpace: a typeclass applying to topological spaces, stating that the space is not the union of a nontrivial pair of disjoint opens.
IsIrreducible: for a nonempty set in a topological space, the property that the set is an irreducible space in the subspace topology.
On the definition of irreducible and connected sets/spaces #
In informal mathematics, irreducible spaces are assumed to be nonempty.
We formalise the predicate without that assumption as
In other words, the only difference is whether the empty space counts as irreducible.
There are good reasons to consider the empty space to be “too simple to be simple”
See also https://ncatlab.org/nlab/show/too+simple+to+be+simple,
and in particular
A preirreducible set
s is one where there is no non-trivial pair of disjoint opens on
An infinite type with cofinite topology is an irreducible topological space.
s is irreducible if and only if
for every finite collection of open sets all of whose members intersect
s also intersects the intersection of the entire collection
(i.e., there is an element of
s contained in every member of the collection).
A set is preirreducible if and only if for every cover by two closed sets, it is contained in one of the two covering sets.
A set is irreducible if and only if for every cover by a finite collection of closed sets, it is contained in one of the members of the collection.
∅ ≠ U ⊆ S ⊆ t such that
U is open and
t is preirreducible, then
S is irreducible.