Fixed Points and Noetherian Topologies

Abstract

Noetherian spaces are a generalisation of well-quasi-orderings to topologies, that can be used to prove termination of programs. They find applications in the verification of transition systems, some of which are better described using topology. The goal of this paper is to allow the systematic description of computations using inductively defined datatypes via Noetherian spaces. This is achieved through a fixed point theorem based on a topological minimal bad sequence argument.

1 Introduction

Let $(\mathcal {E}, \le )$ be a set endowed with a quasi-order. A sequence $(x_n)_n \in \mathcal {E}^{\mathbb {N}}$ is good whenever there exists $i < j$ such that $x_i \le x_j$. A quasi-ordered set $(\mathcal {E}, \le )$ is a well-quasi-ordered — abbreviated as wqo — if every sequence is good. By calling a sequence bad whenever it is not good, well-quasi-orderings are equivalently defined as having no infinite bad sequences. This generalisation of well-founded total orderings can be used as a basis for proving program termination. For instance, algorithms alike Example 1.1 can be studied via well-quasi-orderings and the length of their bad sequences [5]. More generally, one can map the states of a run to a wqo via a so-called quasi-ranking function to both prove the termination of the program and gain information about its runtime [27, Chapter 2]. Let us provide a concrete example of this proof scheme.

Example 1.1

Let $\textsf{Alg}$ be the algorithm with three integer variables a, b, c that non-deterministically performs one of the following operations until a, b or c becomes negative: (l) $\langle a,b,c \rangle \leftarrow \langle a - 1, b , 2c \rangle$ or (r) $\langle a,b,c \rangle \leftarrow \langle 2c, b -1 , 1 \rangle$.

Lemma 1.2

For every choice of $a,b,c \in \mathbb {N}^3$, the algorithm $\textsf{Alg}$ terminates.

Proof

Let us prove that $\textsf{Alg}$ builds a bad sequence of triples when ordering $\mathbb {N}^3$ with $(a_1,b_1,c_1) \le (a_2, b_2, c_2)$ whenever $a_1 \le a_2$, $b_1 \le b_2$, and $c_1 \le c_2$. If $(a_i, b_i, c_i)$ and $(a_j, b_j, c_j)$ represent two configurations in a run of $\textsf{Alg}$, either only rule (l) was fired and $a_j < a_i$, or rule (r) was fired as least once, and $b_j < b_i$.

Because $(\mathbb {N}^3, \le )$ is a well-quasi-ordering (see Dickson’s Lemma in [28]), $\textsf{Alg}$ terminates for every choice of initial triple $(a,b,c) \in \mathbb {N}^3$.

As a combinatorial tool, well-quasi-orderings appear frequently in varying fields of computer science, ranging from graph theory to number theory [3, 18, 21, 22]. Well-quasi-orderings have also been highly successful in proving the termination of verification algorithms. One critical application of well-quasi-orderings is to the verification of infinite state transition systems, via the study of so-called Well-Structured Transition Systems (WSTS) [1, 2, 7, 16].

Noetherian spaces. A major roadblock arises when using well-quasi-orders: the powerset of a well-quasi-order may fail to be one itself [26]. This is particularly problematic in the study of WSTS, where the powerset construction appears frequently [1, 19, 29]. To tackle this issue, one can justify that the quasi-orders of interest are not pathological, and are actually better quasi-orders [23, 25]. Another approach is offered by the topological notion of Noetherian space, which as pointed out by Goubault-Larrecq, can act as a suitable generalisation of well-quasi-orderings that is preserved under the powerset construction [10].

The topological analogues to WSTS enjoy similar decidability properties, and there even exists an analogue to Karp and Miller’s forward analysis for Petri nets [11]. Moreover, their topological nature allows to verify systems beyond the reach of quasi-orderings, such as lossy concurrent polynomial programs [11]. This is possible because the polynomials are handled via results from algebraic geometry, through the notion of the Zariski topology over $\mathbb {C}^n$ [12, Exercise 9.7.53].

One drawback of the topological approach is that many topologies correspond to a single quasi-ordering. Hence, when the problem is better described via an ordering, one has to choose a specific topology, and there usually does not exist a finest one that is Noetherian.

Inductively defined datatypes. As for well-quasi-orders, Noetherian spaces are stable under finite products and finite sums [12, 28]. While this can be enough to describe the set of configurations of a Petri net using $\mathbb {N}^k$, it does not allow to talk about more complex data structures, that are typically defined inductively, such as lists and trees. To make the above statement precise, let $\textbf{1}$ be the singleton set, $A + B$ be the disjoint union of A and B, and $A \times B$ their cartesian product. Then, the set of finite words over an alphabet $\varSigma$ is precisely the least fixed point of $F :X \mapsto \textbf{1}+ \varSigma \times X$. Similarly, the set of finite trees over $\varSigma$ equals $\textsf{lfp}_{X}.{\varSigma \times X^{*}}$, where $\textsf{lfp}_{X}.{F(X)}$ denotes the least fixed point of F.

In the realm of well-quasi-orderings, the specific cases of finite words and finite trees are handled respectively via Higman’s Lemma [18] and Kruskal’s Tree Theorem [22]. Let us recall that a word u embeds into a word w (written $u \le _{*}v$) whenever whenever there exists a strictly increasing map $h :|w| \rightarrow |w'|$ such that $w_i \le w_{h(i)}$ for $1 \le i \le |w|$. Similarly, a tree t embeds into a tree $t'$ (written $t \le _\textsf{tree}t'$) whenever there exists a map from nodes of t to nodes of $t'$ respecting the least common ancestor relation, and increasing the colours of the nodes. Proofs that finite words and finite trees preserve well-quasi-orderings typically rely on a so-called minimal bad sequence argument due to Nash-Williams [24]. However, the argument is quite subtle, and needs to be handled with care [9, 30]. In addition, the argument is not compositional and has to be slightly modified whenever a new inductive construction is desired [as in, e.g., 3, 4].

This picture has been adapted by Goubault-Larrecq to the topological setting by proposing analogues of the word embedding and tree embedding, together with a proof that they preserve Noetherian spaces [12, Section 9.7]. However, both the definitions and the proofs have an increased complexity, as they rely on an adapted “topological minimal bad sequence argument” that appears to be even more subtle [14, errata n. 26]. Moreover, the newly introduced topologies have involved definitions often relying on ad-hoc constructions.

In the case of well-quasi-orderings, two generic fixed point constructions have been proposed to handle inductively defined datatypes [8, 17]. In these frameworks, $\textsf{lfp}_{X}.{F(X)}$ is guaranteed to be a well-quasi-ordering provided that F is a “well-behaved functor” of quasi-orders. Both proposals, while relying on different categorical notions, successfully recover Higman’s word embedding and Kruskal’s tree embedding through their respective definitions as least fixed points. As a side effect, they reinforce the idea that these two quasi-orders are somehow canonical.

In the case of Noetherian spaces, no equivalent framework exists to build inductive datatypes, and the notions of “well-behaved” constructors from [8, 17] rule out the use of important Noetherian spaces, as they require that an element $a \in F(X)$ has been built using finitely many elements of X: while this is the case for finite words and finite trees, it does not hold for the arbitrary powerset. Moreover, there have been recent advances in placing Noetherian topologies over spaces that are not straightforwardly obtained through “well-behaved” definitions, such as infinite words [13], or even ordinal length words [15].

1.1 Contributions of this paper

In this paper, we propose a least fixed point theorem for Noetherian topologies. This is done in a way that greatly differs from the categorical frameworks introduced in the study of well-quasi-orders, as the construction of the space is entirely decoupled from the construction of the topology. In particular, the carrier set X itself need not be inductively defined.

In this setting, we consider a fixed set X and a map R from topologies $\tau$ over X to topologies $R(\tau )$ over X. Because the set of topologies over X is a complete lattice, it suffices to ask for R to be monotone to guarantee that it has a least fixed point, that we write $\textsf{lfp}_{\tau }.{R(\tau )}$. In general, this least fixed point will not be Noetherian, but we show that a simple sufficient condition on R guarantees that it is. This main theorem (Theorem 3.21), encapsulates all the complexity of the topological adaptations of the minimal bad sequences arguments [12, Section 9.7], and we believe that it has its own interest.

The necessity to separate the construction of the set of points from the construction of the topology might be perceived as a weakness of the theory, when it is in fact a strength of our approach. We illustrate this by giving a shorter proof that the words of ordinal length are Noetherian [15], without providing an inductive definition of the space. As an illustration of the versatility of our framework, we introduce a reasonable topology over ordinal branching trees (with finite depth), and prove that it is Noetherian using the same technique.

In the specific cases where the space of interest can be obtained as a least fixed point of a “well-behaved” functor, we show how Theorem 3.21 can be used to generalise the categorical framework of Hasegawa [17] to a topological setting. As well as adding inductively defined topologies (hence, inductively defined datatypes) to the theory of Noetherian spaces, this provide a reasonable answer to the canonicity issue previously mentioned.

Outline. In Section 2 we recall some of the main results in the theory of Noetherian spaces. In Section 3 we prove our main result (Theorem 3.21). In Section 4 we explore how this result covers existing topological results in the literature, and provide a new non-trivial Noetherian space (Definition 4.7). In Section 5, we leverage our main result to devise a Noetherian topology over inductively defined datatypes (Theorem 5.13), and prove that this generalises the work of Hasegawa over well-quasi-orders (Theorem 5.15).

2 A Quick Primer on Noetherian Topologies

A topological space is a pair $(\mathcal {X}, \tau )$ where $\tau \subseteq \mathbb {P}(\mathcal {X})$, $\tau$ is stable under finite intersections, and $\tau$ is stable under arbitrary unions. A subset $U \subseteq \mathcal {X}$ is an open subset when $U \in \tau$, and a closed subset when $\mathcal {X}\setminus U \in \tau$. As an order-theoretic counterpart to open and closed subsets, we say that a subest U of a quasi-ordered set $(\mathcal {E}, \le )$ is upwards-closed whenever for all $x \in U$, $x \le y$ implies $y \in U$. Similarly, a subset is downwards-closed whenever its complement is upwards-closed. One can convert back and forth between the two as follows:

Notation 2.1

Let $(\mathcal {E}, \le )$ be a quasi-order and $(\mathcal {X},\tau )$ be a topological space. The Alexandroff topology $\textsf{alex}(\le )$ over $\mathcal {E}$ is the collection of upwards-closed subsets of $\mathcal {E}$. The specialisation preorder $\mathrel {{\le }_{\tau }}$ is defined via $x \mathrel {{\le }_{\tau }} y$ whenever for every open subset $U \in \tau$, if $x \in U$ then $y \in U$.

It is an easy check that the specialisation pre-order of the Alexandroff topology of a quasi-order $\le$ is the quasi-order itself. Beware that several topologies can share the same specialisation pre-order$\le$, and among those, the Alexandroff topology is the finest.

We can now build the topological analogue to wqos through the notion of compactness: a subset K of $\mathcal {X}$ is defined as compact whenever from every family $(U_i)_{i \in I}$ of open sets such that $K \subseteq \bigcup _{i \in I} U_i$, one can extract a finite subset $J \subseteq I$ such that $K \subseteq \bigcup _{i \in J} U_i$. A quasi-order $(\mathcal {E},\le )$ is wqo if and only if every subset K of $\mathcal {E}$ is compact for $\textsf{alex}(\le )$. Generalising this property to arbitrary topological spaces $(\mathcal {X},\tau )$, a topological space $(\mathcal {X},\tau )$ is said to be a Noetherian space whenever every subset of $\mathcal {X}$ is compact.

Remark 2.2

A space $(\mathcal {X}, \tau )$ is Noetherian if and only if for every increasing sequence of open subsets $(U_i)_{i \in \mathbb {N}}$, there exists $j \in \mathbb {N}$ such that $\bigcup _{i \in \mathbb {N}} U_i = \bigcup _{i \le j} U_i$.

In order to inductively define Noetherian spaces, we will often rely on basic constructors such as the disjoint sum and the finite product. For completeness, we recall in Table 1 usual constructors that preserve Noetherian spaces. This table also illustrate the versatility of the concept, that encompasses both the algebraic properties of $\mathbb {C}^k$ and the order properties of well-quasi-orders.

Table 1. An algebra of Noetherian spaces [see 10, 12, 15]

3 Refinements of Noetherian topologies

Let us fix a set $\mathcal {X}$. The collection of topologies over $\mathcal {X}$ is itself a set, and forms a complete lattice for inclusion. In this lattice, the least element is the trivial topology $\tau _{\text {triv}}:=\{ \emptyset , \mathcal {X}\}$, and the greatest element is the discrete topology $\mathbb {P}(\mathcal {X})$. Thanks to Tarski’s fixed point theorem, every monotone function R mapping topologies over $\mathcal {X}$ to topologies over $\mathcal {X}$ has a least fixed point, which can be obtained by transfinitely iterating R from the trivial topology. Writing $\textsf{lfp}_{\tau }.{R(\tau )}$ for the least fixed point of R, our goal is to provide sufficient conditions for $(\mathcal {X}, \textsf{lfp}_{\tau }.{R(\tau )})$ to be Noetherian.

Definition 3.1

A refinement function over a set $\mathcal {X}$ is a function $\textsf{R}$ mapping topologies over $\mathcal {X}$ to topologies over $\mathcal {X}$. Moreover, we assume that $\textsf{R}(\tau )$ is Noetherian whenever $\tau$ is, and that $\textsf{R}(\tau ) \subseteq \textsf{R}(\tau ')$ when $\tau \subseteq \tau '$.

As $(\mathcal {X}, \tau _{\text {triv}})$ is always Noetherian, $(\mathcal {X}, \textsf{R}^n (\tau _{\text {triv}}))$ is Noetherian for all $n \in \mathbb {N}$ and refinement function $\textsf{R}$. However, it remains unclear whether the transfinite iterations needed to reach a fixed point preserve Noetherian spaces.

We demonstrate in Example 3.2 how to obtain the topology $\textsf{alex}(\le )$ over $\mathbb {N}$ as a least fixed point of some simple refinement function. Before that, let us define the notion of upwards-closure: given a quasi-order $(\mathcal {E}, \le )$ and a set $E \subseteq \mathcal {E}$, let us define the upwards-closure of E, written $\uparrow _{\le }{E}$, as the set of elements that are greater or equal than some element of E in $\mathcal {E}$.

Example 3.2

(Natural Numbers). Over $X :=\mathbb {N}$, one can define $\textsf{Div}(\tau )$ as the collection of the sets $\uparrow _{\le }{(U + 1)}$ for $U \in \tau$, plus $\mathbb {N}$ itself. Then $\textsf{Div}(\tau _{\text {triv}}) = \left\{ \emptyset , \uparrow _{\le }{1}, \mathbb {N} \right\}$, $\textsf{Div}^2(\tau _{\text {triv}}) = \left\{ \emptyset , \uparrow _{\le }{1}, \uparrow _{\le }{2}, \mathbb {N} \right\}$. More generally, for every $k \ge 0$, $\textsf{Div}^k(\tau _{\text {triv}}) = \left\{ \emptyset , \uparrow _{\le }{1}, \dots , \uparrow _{\le }{k}, \mathbb {N} \right\}$. It is an easy check that $\textsf{lfp}_{\tau }.{\textsf{Div}(\tau )}$ is precisely $\textsf{alex}(\le )$, which is Noetherian because $(\mathbb {N}, \le )$ is a well-quasi-ordering.

3.1 An ill-behaved refinement function

Not all refinement functions behave as nicely as in Example 3.2, and one can obtain non-Noetherian topologies via their least fixed points.

Let us consider for this section $\varSigma :=\{a,b\}$ with the discrete topology, i.e., $\left\{ \emptyset , \{a\}, \{b\}, \varSigma \right\}$. Let us now build the set $\varSigma ^{*}$ of finite words over $\varSigma$. Whenever U and V are subsets of $\varSigma ^{*}$, let us write UV for their concatenation, defined as $\left\{ {uv} {:} {u \in U, v \in V} \right\}$. To construct an ill-behaved refinement function, we will associate to a topology $\tau$ the set $\left\{ { UV } {:} { U \in \left\{ \emptyset , \{a\}, \{b\}, \varSigma \right\} , V \in \tau } \right\}$. However, the latter fails to be a topology in general. This problem frequently appears in this paper, and is solved by considering the so-called generated topology.

Let us briefly recall that for every set $\mathcal {X}$ and collection of subsets $B \subseteq \mathbb {P}(\mathcal {X})$, one can construct the topology generated from B as the least topology on $\mathcal {X}$ containing B. This topology coincides with the one containing arbitrary unions of finite intersections of subsets in B. We say that B is a subbasis of $\tau$ when $\tau$ is the topology generated by B. Alexanders’s Subbase Lemma allows to study Noetherian spaces in this setting [12, Thm. 4.4.29]: it states that checking whether a subset K of $\mathcal {X}$ is compact in $\tau$ can be done by considering only open subsets in B, i.e., that for every family $(U_i)_{i \in I}$ of a subbasis B of $\tau$ such that $K \subseteq \bigcup _{i \in I} U_i$, one can extract a finite subset $J \subseteq I$ such that $K \subseteq \bigcup _{j \in J} U_j$.

Definition 3.3

Let $\textsf{R}_\textsf {\text {pref}}$ be the function mapping a topology $\tau$ over $\varSigma ^{*}$ to the topology generated by the sets UV where $U \subseteq \varSigma$ and $V \in \tau$,

We refer to Figure 1 for a graphical presentation of the first two iterations of the refinement function $\textsf{R}_\textsf {\text {pref}}$. For the sake of completeness, let us compute $\textsf{lfp}_{\tau }.{\textsf{R}_\textsf {\text {pref}}(\tau )}$, which is the Alexandroff topology of the prefix ordering on words.

Definition 3.4

The prefix topology¹ $\tau _{\textrm{pref}^*}$, over $\varSigma ^{*}$ is generated by the following open sets: $U_1 \dots U_n \varSigma ^{*}$, where $n \ge 0$ and $U_i \subseteq \varSigma$.

Lemma 3.5

The prefix topology over $\varSigma ^{*}$ is the least fixed point of $\textsf{R}_\textsf {\text {pref}}$.

Lemma 3.6

The function $\textsf{R}_\textsf {\text {pref}}$ is a refinement function.

Proof

It is an easy check that whenever $\tau \subseteq \tau '$, $\textsf{R}_\textsf {\text {pref}}(\tau ) \subseteq \textsf{R}_\textsf {\text {pref}}(\tau ')$. Now, assume that $\tau$ is Noetherian, it remains to prove that $\textsf{R}_\textsf {\text {pref}}(\tau )$ remains Noetherian. Consider a subset $E \subseteq \varSigma ^{*}$ and let us prove that E is compact in $\textsf{R}_\textsf {\text {pref}}(\tau )$.

For that, we consider an open cover $E \subseteq \bigcup _{i \in I} W_i$, where $W_i \in \textsf{R}_\textsf {\text {pref}}(\tau )$. Thanks to Alexander’s subbase lemma, we can assume without loss of generality that $W_i$ is a subbasic open set of $\textsf{R}_\textsf {\text {pref}}(\tau )$, that is, $W_i = U_i V_i$ with $U_i \subseteq \varSigma$ and $V_i \in \tau$.

Since $(\varSigma ^{*}, \tau ) \times (\varSigma ^{*}, \tau )$ is Noetherian (see Table 1), there exists a finite set $J \subseteq I$ such that $\bigcup _{i \in J} U_i \times V_i = \bigcup _{i \in I} U_i \times V_i$. This implies that $E \subseteq \bigcup _{i \in J} U_i V_i$, and provides a finite subcover of E.    $\square$

Fig. 1.

Iterating $\textsf{R}_\textsf {\text {pref}}$ over $\varSigma ^*$. On the left the trivial topology $\tau _{\text {triv}}$, followed by $\textsf{R}_\textsf {\text {pref}}$, and on the right $\textsf{R}_{\textsf {pref}}$ $^{2}$.

The sequence $\bigcup _{0 \le i \le k} a^ib\varSigma ^*$, for $k \in \mathbb {N}$, is a strictly increasing sequence of opens. Therefore, the prefix topology is not Noetherian. The terms $a^ib\varSigma ^*$ can be observed in Figure 1 as a diagonal of incomparable open sets.

Corollary 3.7

The topology $\textsf{lfp}_{\tau }.{\textsf{R}_\textsf {\text {pref}}(\tau )}$ is not Noetherian.

The prefix topology is not Noetherian, even when starting from a finite alphabet. However, we claimed in Section 1 that there is a natural generalisation of the subword embedding to topological spaces which is Noetherian. Before introducing this topology, let us write $[U_1, \dots , U_n]$ as a shorthand notation for the set $\varSigma ^* U_1 \varSigma ^* \dots \varSigma ^* U_n \varSigma ^*$.

Definition 3.8

(Subword topology [12, Definition 9.7.26]). Given a topological space $(\varSigma ,\tau )$, the space $\varSigma ^*$ of finite words over $\varSigma$ can be endowed with the subword topology, generated by the open sets $[U_1, \dots , U_n]$ when $U_i \in \tau$.

The topological Higman lemma [12, Theorem 9.7.33] states that the subword topology over $\varSigma ^{*}$ is Noetherian if and only if $\varSigma$ is Noetherian. Although the subword topology might seem ad-hoc, it can be validated as a generalisation of the subword embedding because the subword topology of $\textsf{alex}(\le )$ equals the Alexandroff topology of the subword ordering of $\le$, for every quasi-order $\le$ over $\varSigma$ [12, Exercise 9.7.30]. Let us now reverse engineer a refinement function whose least fixed point is the subword topology.

Definition 3.9

Let $(\varSigma , \theta )$ be a topological space. Let ${\mathsf {E_{\text {words}}^{\theta }}}$ be defined as mapping a topology $\tau$ over $\varSigma ^{*}$ to the topology generated by the following sets: $\uparrow _{\le _{*}}{UV}$ for $U,V \in \tau$; and $\uparrow _{\le _{*}}{W}$, for $W \in \theta$.

Lemma 3.10

Let $(\varSigma , \theta )$ be a topological space. The subword topology over $\varSigma ^{*}$ is the least fixed point of $\mathsf {E_{\text {words}}^{\theta }}$.

In order to show that $\mathsf {E_{\text {words}}^{\theta }}$ is a refinement function, we first claim that the two parts of the topology can be dealt with separately.

Lemma 3.11

([12, Proposition 9.7.18]). If $(\mathcal {X}, \tau )$ and $(\mathcal {X}, \tau ')$ are Noetherian, then $\mathcal {X}$ endowed with the topology generated by $\tau \cup \tau '$ is Noetherian.

Lemma 3.12

Let $(\varSigma , \theta )$ be a Noetherian topological space. The map $\mathsf {E_{\text {words}}^{\theta }}$ is a refinement function over $\varSigma$.

Proof

We leave the monotonicity of $\mathsf {E_{\text {words}}^{\theta }}$ as an exercice and focus on the proof that $\mathsf {E_{\text {words}}^{\theta }}(\tau )$ is Noetherian, whenever $\tau$ is. Thanks to Lemma 3.11, it suffices to prove that the topology generated by the sets $\uparrow _{\le _{*}}{UV}$ (U, V open in $\tau$), and the topology generated by the sets $\uparrow _{\le _{*}}{W}$ (W open in $\theta$) are Noetherian.

Let $(\uparrow _{\le _{*}}{U_i V_i})_{i \in \mathbb {N}}$ be a sequence of open sets. Because Noetherian topologies are closed under products (see Table 1), there exists k such that $\bigcup _{i \le k} U_i \times V_i = \bigcup _{i \in \mathbb {N}} U_i \times V_i$. Hence, $\bigcup _{i \le k} \uparrow _{\le _{*}}{U_i V_i}= \bigcup _{i \in \mathbb {N}} \uparrow _{\le _{*}}{U_i V_i}$

Let $\uparrow _{\le _{*}}{W_i}$ be a sequence of open sets. Because $\theta$ is Noetherian, there exists k such that $\bigcup _{i \le k} W_i = \bigcup _{i \in \mathbb {N}} W_i$, hence $\bigcup _{i \le k} \uparrow _{\le _{*}}{W_i} = \bigcup _{i \in \mathbb {N}} \uparrow _{\le _{*}}{W_i}$.    $\square$

We have designed two refinement functions$\textsf{R}_\textsf {\text {pref}}$ and $\mathsf {E_{\text {words}}^{\theta }}$ over $\varSigma ^{*}$. Fixing $\theta$ to be the discrete topology over $\varSigma$, the least fixed point of $\textsf{R}_\textsf {\text {pref}}$ is not Noetherian while the least fixed point of $\mathsf {E_{\text {words}}^{\theta }}$ is. We have depicted the result of iterating $\mathsf {E_{\text {words}}^{\theta }}$ twice over the trivial topology in Figure 2. As opposed to $\textsf{R}_\textsf {\text {pref}}$, the “diagonal” elements are comparable for inclusion.

Fig. 2.

The topology , with bold red arrows for the inclusions that were not present between the “analogous sets” in $\textsf{R}_{\textsf {pref}}$ $^{2}$ $(\tau _{\text {triv}})$. We have taken $\theta$ to be the discrete topology over $\varSigma$.

3.2 Well-behaved refinement functions

In this section, we will show how the behaviour of refinement function with respect to subsets will act as a sufficient condition to separate the well-behaved ones from the others. In order to make the idea of computing the refinement function directly over a subset precise, we will replace a subset with the induced topology by a “restricted” topology over the whole space.

Definition 3.13

Let $(\mathcal {X},\tau )$ be a topological space and H be a closed subset of $\mathcal {X}$. Define the subset restriction ${\tau }|{H}$ to be the topology generated by the open subsets $U \cap H$ where U ranges over $\tau$.

Let $\mathcal {X}$ be a topological space, and H be a proper closed subset of $\mathcal {X}$. The space $\mathcal {X}$ endowed with ${\tau }|{H}$ has a lattice of open sets that is isomorphic to the one of the space H endowed with the topology induced by $\tau$, except for the entire space $\mathcal {X}$ itself. As witnessed by Example 3.14, the two spaces are in general not homeomorphic.

Example 3.14

Let $\mathbb {R}$ be endowed with the usual metric topology. The set $\{ a \}$ is a closed set when $a \in \mathbb {R}$. The induced topology over $\{a\}$ is $\left\{ \emptyset , \{a\} \right\}$. The subset restriction of the topology to $\{a\}$ is $\tau _a :=\left\{ \emptyset , \{ a \}, \mathbb {R} \right\}$. Clearly, $(\mathbb {R}, \tau _a)$ and $(\{a\}, \tau _{\text {triv}})$ are not homeomorphic.

In order to build intuition, let us consider the special case of an Alexandroff topology over $\mathcal {X}$ and compute the specialisation preorder of ${\tau }|{H}$, where H is a downwards closed set.

Lemma 3.15

Let $\tau = \textsf{alex}(\le )$ over a set $\mathcal {X}$, and $x,y \in X$. Then, $x \mathrel {{\le }_{{\tau }|{H}}} y$ if and only if $x \mathrel {{\le }_{\tau }} y \wedge y \in H$ or $x \not \in H$. In other words, $H^c$ is collapsed to an equivalence class below H itself.

Definition 3.16

A topology expander is a refinement function $\textsf{E}$ that satisfies the following extra property: for every Noetherian topology $\tau$ satisfying $\tau \subseteq \textsf{E}(\tau )$, for all closed set H in $\tau$, ${\textsf{E}(\tau )}|{H} \subseteq {\textsf{E}({\tau }|{H})}|{H}$.

Lemma 3.17

The refinement function $\textsf{R}_\textsf {\text {pref}}$ is not a topology expander.

Proof

Let us consider $\tau :=\left\{ \emptyset , a\varSigma ^*, b\varSigma ^*, \varSigma ^* \right\}$. Remark that $H :=a\varSigma ^* \cup \left\{ \varepsilon \right\}$ is a closed subset because $\varSigma = \left\{ a, b \right\}$. It is an easy check that ${\textsf{R}_\textsf {\text {pref}}(\tau )}|{H} = \left\{ \emptyset , aa\varSigma ^*, ab \varSigma ^*, a \varSigma ^*, \varSigma ^* \right\} \ne \left\{ \emptyset , aa \varSigma ^*, a \varSigma ^*, \varSigma ^* \right\} = {\textsf{R}_\textsf {\text {pref}}({\tau }|{H})}|{H}$.

Lemma 3.18

When $\theta$ is Noetherian, $\mathsf {E_{\text {words}}^{\theta }}$ is a topology expander.

Proof

We have proven in Lemma 3.12 that $\mathsf {E_{\text {words}}^{\theta }}$ is a refinement function. Let us now prove that it is a topology expander.

Let $\tau$ be a Noetherian topology over $\varSigma ^{*}$, such that $\tau \subseteq \mathsf {E_{\text {words}}^{\theta }}(\tau )$. Let H be a closed subset of $(\varSigma ^{*}, \tau )$. Notice that as H is closed in $\tau$, and since $\tau \subseteq \mathsf {E_{\text {words}}^{\theta }}(\tau )$, H is downwards closed for $\le _{*}$. As a consequence, $(\uparrow _{\le _{*}}{UV}) \cap H = (\uparrow _{\le _{*}}{(U \cap H) (V\cap H)) \cap H}$. Hence, ${\mathsf {E_{\text {words}}^{\theta }}(\tau )}|{H} \subseteq {\mathsf {E_{\text {words}}^{\theta }}({\tau }|{H})}|{H}$.    $\square$

3.3 Iterating Expanders

Our goal is now to prove that topology expanders are refinement functions that can be safely iterated. For that, let us first define precisely what “iterating transfinitely” a refinement function means.

Definition 3.19

Let $(\mathcal {X},\tau )$ be a topological space, and $\textsf{E}$ be a topology expander. The limit topology $\textsf{E}^\alpha (\tau )$ is defined as: $\tau$ when $\alpha = 0$, $\textsf{E}(\textsf{E}^\beta (\tau ))$ when $\alpha = \beta + 1$, and as the join of the topologies $\textsf{E}^\beta (\tau )$ for all $\beta < \alpha$, when $\alpha$ is a limit ordinal.

We devote the rest of this section to proving our main theorem, which immediately implies that least fixed points of topology expanders are Noetherian. Notice that the theorem is trivial whenever $\alpha$ is a successor ordinal.

Proposition 3.20

Let $\alpha$ be an ordinal, $\tau$ be a topology, and $\textsf{E}$ be a topology expander. If $\textsf{E}^\beta (\tau )$ is Noetherian for all $\beta < \alpha$, and $\tau \subseteq \textsf{E}(\tau )$, then $\textsf{E}^\alpha (\tau )$ is Noetherian.

Theorem 3.21

(Main Result). Let $\mathcal {X}$ be a set and $\textsf{E}$ be a topology expander. The least fixed point of $\textsf{E}$ is a Noetherian topology over $\mathcal {X}$.

The topological minimal bad sequence argument. In order to prove Theorem 3.21, we will use a topological minimal bad sequence argument. To that end, let us first introduce a well-founded partial ordering over the elements of $\textsf{E}^{\alpha }(\tau )$. With an open set $U \in \textsf{E}^{\alpha }(\tau )$, we associate a depth $\textsf{depth}(U)$, defined as the smallest ordinal $\beta \le \alpha$ such that $U \in \textsf{E}^{\beta }(\tau )$. We then define $U \mathrel {\trianglelefteq }V$ to hold whenever $\textsf{depth}(U)\le \textsf{depth}(V)$, and $U \mathrel {\triangleleft }V$ whenever $\textsf{depth}(U) < \textsf{depth}(V)$. It is an easy check that this is a well-founded total quasi-order over $\textsf{E}^{\alpha }(\tau )$.

As a first step towards proving that $\textsf{E}^{\alpha }(\tau )$ is Noetherian for a limit ordinal $\alpha$, we first reduce the problem to open subsets of depth strictly less than $\alpha$ itself.

Lemma 3.22

Let $\alpha$ be a limit ordinal, and $\textsf{E}$ be a topology expander. The topology $\textsf{E}^\alpha (\tau )$ has a subbasis of elements of depth strictly below $\alpha$.

Let us recall the notion of topological bad sequence designed by Goubault-Larrecq [12, Lemma9.7.31] in the proof of the Topological Kruskal Theorem, adapted to our ordering of subbasic open sets.

Definition 3.23

Let $(\mathcal {X},\tau )$ be a topological space. A sequence $\mathcal {U}= {(U_i)}_{i \in \mathbb N}$ of open subsets is good if there exists $i \in \mathbb {N}$ such that $U_i \subseteq \bigcup _{j < i} U_j$. A sequence that is not good is called bad.

Lemma 3.24

Let $\alpha$ be a limit ordinal, and $\textsf{E}$ be a topology expander such that $\textsf{E}^\alpha (\tau )$ is not Noetherian. Then, there exists a bad sequence $\mathcal {U}$ of open subsets in $\textsf{E}^\alpha (\tau )$ of depth less than $\alpha$ that is lexicographically minimal for $\mathrel {\trianglelefteq }$. Such a sequence is called minimal bad.

We deduce that in a limit topology, minimal bad sequences are not allowed to use open subsets of arbitrary depth. This will then be leveraged via Lemma 3.27 to decrease the depth by one.

Lemma 3.25

Let $\alpha$ be a limit ordinal, $\tau$ be a topology and $\textsf{E}$ be a topology expander such that $\textsf{E}^{\beta }(\tau )$ is Noetherian for all $\beta < \alpha$. Assume that $\mathcal {U}= (U_i)_{i \in \mathbb N}$ is a minimal bad sequence of $\textsf{E}^\alpha (\tau )$. Then, for every $i \in \mathbb N$, $\textsf{depth}(U_i)$ is either 0 or a successor ordinal.

Definition 3.26

Let $\alpha$ be an ordinal, $\tau$ be a topology, $\textsf{E}$ be a topology expander such that $\tau \subseteq \textsf{E}(\tau )$, and let $U \in \textsf{E}^{\alpha }(\tau )$. The topology $\textsf{Down}(U)$ is generated by the open sets V such that $V \mathrel {\triangleleft }U$, where V ranges over $\textsf{E}^{\alpha }(\tau )$.

Lemma 3.27

Let $\alpha$ be an ordinal, $\textsf{E}$ be a topology expander and $U \in \textsf{E}^{\alpha }(\tau )$. If $\textsf{depth}(U)$ is a successor ordinal, then $U \in \textsf{E}(\textsf{Down}(U))$.

If $\mathcal {U}$ is a minimal bad sequence in $(X, \textsf{E}^{\alpha }(\tau ))$, then $U_i \not \subseteq \bigcup _{j < i} U_j :=V_i$, i.e., $U_i \cap V_i^c \ne \emptyset$. We can now use our subset restriction operator to devise a topology associated to this minimal bad sequence. Noticing that $H_i :=V_i^c$ is a closed set in $\textsf{E}^{\alpha }(\tau )$, hence we can build the subset restriction ${\textsf{Down}(U_i)}|{H_i}$.

Definition 3.28

Let $\alpha$ be an ordinal, $\tau$ be a topology, $\textsf{E}$ be a topology expander such that $\tau \subseteq \textsf{E}(\tau )$, and let $\mathcal {U}= (U_i)_{i \in \mathbb {N}}$ be a minimal bad sequence in $\textsf{E}^{\alpha }(\tau )$. Then, the minimal topology $\mathcal {U}(\textsf{E}^{\alpha }(\tau ))$ is generated by $\bigcup _{i \in \mathbb {N}} {\textsf{Down}(U_i)}|{H_i}$, where $H_i :=(\bigcup _{j < i} U_j)^c$.

Lemma 3.29

Let $\alpha$ be an ordinal, $\tau$ be a topology, $\textsf{E}$ be a topology expander such that $\tau \subseteq \textsf{E}(\tau )$, and let $\mathcal {U}= (U_i)_{i \in \mathbb {N}}$ be a minimal bad sequence in $\textsf{E}^{\alpha }(\tau )$. Then, the minimal topology$\mathcal {U}(\textsf{E}^{\alpha }(\tau ))$ is Noetherian.

Proof

Assume by contradiction that $\mathcal {U}(\textsf{E}^\alpha (\tau ))$ is not Noetherian. Let us define $V_i$ as $\bigcup _{j < i} U_j$, and $H_i$ as $V_i^c$.

Thanks to [12, Lemma 9.7.15] there exists a bad sequence$\mathcal {W} :=(W_i)_{i \in \mathbb {N}}$ of subbasic elements of $\mathcal {U}(\textsf{E}^\alpha (\tau ))$. By definition, $W_i$ is in some ${\textsf{Down}(U_j)}|{H_j}$. Let us select a mapping $\rho :\mathbb N \rightarrow \mathbb N$, such that $W_i \in {\textsf{Down}(U_{\rho (i)})}|{H_{\rho (i)}}$. This amounts to the existence of an open $T_{\rho (i)}$, such that $T_{\rho (i)} \mathrel {\triangleleft }U_{\rho (i)}$, and $W_i = T_{\rho (i)} \setminus V_{\rho (i)}$. Without loss of generality we assume that $\rho$ is monotonic.

Let us build the sequence $\mathcal Y$ defined by $Y_i :=U_i$ if $i < \rho (0)$ and $Y_i :=T_{\rho (i)}$ otherwise. This is a sequence of open sets in $\textsf{E}^\alpha (\tau )$ that is lexicographically smaller than $\mathcal {U}$, hence $\mathcal Y$ is a good sequence: there exists $i \in \mathbb {N}$ such that $Y_i \subseteq \bigcup _{j < i} Y_j$.

• If $i < \rho (0)$, then $U_i \subseteq \bigcup _{j < i} U_j$ contradicting that $\mathcal {U}$ is bad.

• If $i \ge \rho (0)$, let us write $Y_i = T_{\rho (i)} \subseteq \bigcup _{j< \rho (0)} U_j \cup \bigcup _{j < i} T_{\rho (j)}$. By taking the intersection with $H_{\rho (i)}$, we obtain $W_i \subseteq \bigcup _{j < i} W_j$, contradicting the fact that $\mathcal W$ is a bad sequence.    $\square$

We are now ready to leverage our knowledge of minimal topologies associated with minimal bad sequences to carry on the proof of our main theorem.

Proposition 3.20. Let $\alpha$ be an ordinal, $\tau$ be a topology, and $\textsf{E}$ be a topology expander. If $\textsf{E}^\beta (\tau )$ is Noetherian for all $\beta < \alpha$, and $\tau \subseteq \textsf{E}(\tau )$, then $\textsf{E}^\alpha (\tau )$ is Noetherian.

Proof

If $\alpha$ is a successor ordinal, then $\alpha = \beta + 1$ and $\textsf{E}^{\alpha } (\tau ) = \textsf{E}(\textsf{E}^\beta (\tau ))$. Because $\textsf{E}$ respects Noetherian topologies, we immediately conclude that $\textsf{E}^{\alpha }(\tau )$ is Noetherian. We are therefore only interested in the case where $\alpha$ is a limit ordinal.

Assume by contradiction that $\textsf{E}^\alpha (\tau )$ is not Noetherian, using Lemma 3.24 there exists a minimal bad sequence$\mathcal {U}:=(U_i)_{i \in \mathbb {N}}$. Let us write $d_i :=\textsf{depth}(U_i) < \alpha$. Thanks to Lemma 3.25, $d_i$ is either 0 or a successor ordinal.

Because $\textsf{E}^{\beta }(\tau )$ is Noetherian for $\beta < \alpha$, there are finitely many open subsets $U_i$ at depth $\beta$ for every ordinal $\beta < \alpha$. Indeed, if they were infinitely many, one would extract an infinite bad sequence of opens in $\textsf{E}^{\beta }(\tau )$, which is absurd.

Furthermore, the sequence $(d_i)_{i \in \mathbb {N}}$ must be monotonic, otherwise $\mathcal {U}$ would not be lexicographically minimal. We can therefore construct a strictly increasing map $\rho :\mathbb {N} \rightarrow \mathbb N$ such that $0 < \textsf{depth}(U_{\rho (j)})$ and $\textsf{depth}(U_{i}) < \textsf{depth}(U_{\rho (j)})$ whenever $0 \le i < \rho (j)$.

Let us consider some $i = \rho (n)$ for some $n \in \mathbb {N}$. Let us write $V_{i} :=\bigcup _{j < i} U_j$, and $H_{i} :=X \setminus V_i$. The set $V_i$ is open in $\textsf{Down}(U_i)$ by construction of $\rho$, hence $H_i$ is closed in $\textsf{Down}(U_i)$. As $\textsf{E}$ is a topology expander, we derive the following inclusions:

$$\begin{aligned} {\textsf{E}(\textsf{Down}(U_i))}|{H_i}&\subseteq {\textsf{E}({\textsf{Down}(U_i)}|{H_i})}|{H_i} \\&\subseteq {\textsf{E}(\mathcal {U}(\textsf{E}^\alpha (\tau )))}|{H_i} \end{aligned}$$

Recall that $U_{i} \in \textsf{E}(\textsf{Down}(U_{i}))$ thanks to Lemma 3.27. As a consequence, $U_i \setminus V_i = W_i \setminus V_i$ for some open set $W_i$ in $\textsf{E}(\mathcal {U}(\textsf{E}^\alpha (\tau )))$. Thanks to Lemma 3.29, and preservation of Noetherian topologies through topology expanders, the latter is a Noetherian topology. Therefore, $(W_{\rho (i)})_{i \in \mathbb {N}}$ is a good sequence. This provides an $i \in \mathbb N$ such that $W_{\rho (i)} \subseteq \bigcup _{\rho (j) < \rho (i)} W_{\rho (j)}$. In particular,

$$\begin{aligned} U_{\rho (i)} \setminus V_{\rho (i)}&= W_{\rho (i)} \setminus V_{\rho (i)} \subseteq \bigcup _{\rho (j)< \rho (i)} W_{\rho (j)} \setminus V_{\rho (i)} \subseteq \bigcup _{\rho (j)< \rho (i)} W_{\rho (j)} \setminus V_{\rho (j)} \\&\subseteq \bigcup _{\rho (j)< \rho (i)} U_{\rho (j)} \setminus V_{\rho (j)} \subseteq \bigcup _{j < \rho (i)} U_{j} = V_{\rho (i)} \end{aligned}$$

This proves that $U_{\rho (i)} \subseteq V_{\rho (i)}$, i.e. that $U_{\rho (i)} \subseteq \bigcup _{j < \rho (i)} U_j$. Finally, this contradicts the fact that $\mathcal {U}$ is bad.    $\square$

We have effectively proven that being well-behaved with respect to closed subspaces is enough to consider least fixed points of refinement functions. This behaviour should become clearer in the upcoming sections, where we illustrate how this property can be ensured both in the case of Noetherian spaces and well-quasi-orderings.

4 Applications of Topology Expanders

We now briefly explore topologies that can be proven to be Noetherian using Theorem 3.21. It should not be surprising that both the topological Higman lemma and the topological Kruskal theorem fit in the framework of topology expanders, as both were already proven using a minimal bad sequence argument. However, we will proceed to extend the use of topology expander to spaces for which the original proof did not use a minimal bad sequence argument, and illustrate how they can easily be used to define new Noetherian topologies.

Finite words and finite trees. As a first example, we can easily recover the topological Higman lemma [12, Theorem 9.7.33] because the subword topology is the least fixed point of $\mathsf {E_{\text {words}}^{\theta }}$, which is a topology expander (see Lemmas 3.10 and 3.18).

It does not require much effort to generalise this proof scheme to the case of the topological Kruskal theorem [12, Theorem 9.7.46]. As a shorthand notation, let us write $t \in \diamond U \langle V \rangle$ whenever there exists a subtree $t'$ of t whose root is labelled by an element of U and whose list of children belongs to V. Recall that we write $u \le _{*}v$ when u is a scattered subword of v, and $t \le _\textsf{tree}t'$ when t embeds in $t'$ as a tree (see page Page 2). As for the subword topology, the definition is ad-hoc but correctly generalises the tree embedding relation because the tree topology of $\textsf{alex}(\le )$ is the Alexandroff topology of $\le _\textsf{tree}$, for every ordering $\le$ over $\varSigma$ [12, Exercise 9.7.48].

Definition 4.1

([12, Definition 9.7.39]). Let $(\varSigma ,\theta )$ be a topological space. The space $\textsf{T}(\varSigma )$ of finite trees over $\varSigma$ can be endowed with the tree topology, the coarsest topology such that $\diamond U \langle V\rangle$ is open whenever U is an open set of $\varSigma$, and V is an open set of $\textsf{T}(\varSigma )^{*}$ in its subword topology.

Definition 4.2

Let $(\varSigma , \theta )$ be a topological space. Let $\mathsf {E_{{\text {tree}}}}^{\theta }$ be the function that maps a topology $\tau$ to the topology generated by the sets $\uparrow _{\le _\textsf{tree}}{U \langle V \rangle }$, for U open in $\theta$, V open in $\textsf{T}(\varSigma )^{*}$ with the subword topology of $\tau$.

Lemma 4.3

The tree topology is the least fixed point of $\mathsf {E_{{\text {tree}}}}^{\theta }$, which is a topology expander. Hence, the tree topology is Noetherian when $\theta$ is.

Ordinal words. Let us now demonstrate how Theorem 3.21 can be applied over spaces which are proved to be Noetherian without using a minimal bad sequence argument. For that, let us consider $\varSigma ^{< \alpha }$ the set of words of ordinal length less than $\alpha$, where $\alpha$ is a fixed ordinal. Since $\le _{*}$ is in general not a wqo on $\varSigma ^{<\alpha }$ when $\le$ is wqo on $\varSigma$, this also provides an example of a topological minimal bad sequence argument that has no counterpart in the realm of wqos.

Definition 4.4

([15]). Let $(\varSigma , \theta )$ be a topological space. The ordinal subword topology over $\varSigma ^{<\alpha }$ is the topology generated by the closed sets $F_1^{< \beta _1} \cdots F_n^{<\beta _n}$, for $n \in \mathbb {N}$, $F_i$ closed in $\theta$, $\beta _i < \alpha$, and where $F^{<\beta }$ is the set of words of length less than $\beta$ with all of their letters in F.

The ordinal subword topology is Noetherian [15], but the proof is quite technical and relies on the in-depth study of the possible inclusions between the subbasic closed sets. Before defining a suitable topology expander, given an ordinal $\beta$ and a set $U \subseteq \varSigma ^{<\alpha }$, let us write $w \in \beta \triangleright U$ if and only if $w_{> \gamma } \in U$ for all $0 \le \gamma < \beta$.

Definition 4.5

Let $(\varSigma , \theta )$ be a topological space, and $\alpha$ be an ordinal. The function maps a topology $\tau$ to the topology generated by the following sets: $\uparrow _{\le _{*}}{UV}$ for U, V opens in $\tau$; $\uparrow _{\le _{*}}{\beta \triangleright U}$, for U open in $\tau$, $\beta \le \alpha$; $\uparrow _{\le _{*}}{W}$, for W open in $\theta$.

Lemma 4.6

Given a Noetherian space $(\varSigma ,\theta )$, and an ordinal $\alpha$. The map is a topology expander, whose least fixed point contains the ordinal subword topology. Therefore, the ordinal subword topology is Noetherian.

Remark that Definitions 4.2, 4.5 and 3.9 all follow the same blueprint: new open sets are built as upwards closure for the corresponding quasi-order of the natural constructors associated to the space. We argue that this blueprint mitigates the canonicity issue and the complexity of Definitions 4.1, 4.4 and 3.8.

Ordinal branching trees. As an example of a new Noetherian topology derived using Theorem 3.21, we will consider $\alpha$-branching trees $\textsf{T}^{<\alpha }({\varSigma })$, i.e., the least fixed point of the constructor $X \mapsto \textbf{1}+ \varSigma \times X^{< \alpha }$ where $\alpha$ is a given ordinal. This example was not known to be Noetherian, and fails to be a well-quasi-order, and illustrates how Theorem 3.21 easily applies on inductively defined spaces.

Definition 4.7

Let $(\varSigma , \theta )$ be a Noetherian space. The ordinal tree topology over $\alpha$-branching trees is the least fixed point of , mapping a topology $\tau$ to the topology generated by the sets $\uparrow _{\le _\textsf{tree}}{U\langle V \rangle }$, where $U \in \theta$, V is open in $(\textsf{T}^{<\alpha }({\varSigma }))^{<\alpha }$ with the ordinal subword topology, and $U \langle V \rangle$ is the set of trees whose root is labelled by an element of U and list of children belongs to V.

Theorem 4.8

The $\alpha$-branching trees endowed with the ordinal tree topology forms a Noetherian space.

Proof

It suffices to prove that is a topology expander. It is clear that is monotone, and a closed set of is always downwards closed for $\le _\textsf{tree}$. As a consequence, if and H is closed in $\tau$, $t \in V :=(\uparrow _{\le _\textsf{tree}}{U\langle V \rangle }) \cap H$ if and only if $t \in H$ and every children of t belongs to H. Therefore, $(\uparrow _{\le _\textsf{tree}}{U\langle V \rangle }) \cap H = (\uparrow _{\le _\textsf{tree}}{U\langle V \cap H^{<\alpha } \rangle }) \cap H$. Notice that $H^{<\alpha } \cap V$ is an open of the ordinal subword topology over ${\tau }|{H}$. As a consequence, .

Let us now check that preserves Noetherian topologies. Let $W_i :=\uparrow _{\le _\textsf{tree}}{U_i \langle V_i \rangle }$ be a $\mathbb {N}$-indexed sequence of open sets in where $\tau$ is Noetherian. The product of the topology $\theta$ and the ordinal subword topology over $\tau$ is Noetherian thanks to Table 1 and Lemma 4.6. Hence, there exists a $i \in \mathbb {N}$ such that $U_i \times V_i \subseteq \bigcup _{j < i} U_j \times V_j$. As a consequence, $W_i \subseteq \bigcup _{j < i} W_j$. We have proven that is Noetherian.    $\square$

At this point, we have proven that the framework of topology expanders allows to build non-trivial Noetherian spaces. We argue that this bears several advantages over ad-hoc proofs: (i) the ad-hoc proofs are often tedious and error prone [12, 13, 15] (ii) the verification that $\textsf{E}$ is a topology expander on the other hand is quite simple (iii) reduces the canonicity issue of topologies to the choice of a suitable topology expander.

5 Consequences on inductive definitions

So far, the process of constructing Noetherian spaces has been the following: first build a set of points, then compute a topology that is Noetherian as a least fixed point. In the case where the set of points itself is inductively defined (such as finite words or finite trees), the second step might seem redundant, and getting rid of it provides a satisfactory answer to the canonicity concerns about Noetherian topologies.

Before studying inductive definition of topological spaces, the notion of least fixed-point in this setting has to be made precise. To that purpose, let us now introduce ome basic notions of category theory. In this paper only three categories will appear, the category $\textsf{Set}$ of sets and functions, the category $\textsf{Top}$ of topological spaces and continuous maps, and the category $\textsf{Ord}$ of quasi-ordered spaces and monotone maps. Using this language, a unary constructor G in the algebra of wqos defines an endofunctor from objects of the category $\textsf{Ord}$ to objects of the category $\textsf{Ord}$ preserving well-quasi-orderings.

Notation 5.1

Recall that in a category $\mathcal {C}$, $\textrm{Hom}(A,B)$ is used to denote the collection of morphisms from the object A to the object B in $\mathcal {C}$. Moreover, $\textrm{Aut}(A)$ denotes the set of automorphisms of A, i.e., invertible elements of $(\textrm{Hom}(A,A), \circ )$.

In our study of Noetherian spaces (resp. well-quasi-orderings), we will often see constructors $G'$ as first building a new set of structures, and then adapting the topology (resp. ordering) to this new set. In categorical terms, we are interested in endofunctors $G'$ that are U-lifts of endofunctors on $\textsf{Set}$, where U is the forgetful functor from $\textsf{Top}$ (resp. $\textsf{Ord}$) to $\textsf{Set}$.

5.1 Divisibility Topologies of Analytic Functors

The goal of this section is to introduce the categorical framework needed to formalise the automatic definition of a topology over an inductively defined datatype, and to compare this definition with the work that exists on well-quasi-orders by Hasegawa [17] and Freund [8]. We will avoid as much as possible the use of complex machinery related to analytic functors, and use as a definition an equivalent characterisation given by Hasegawa [17, Theorem 1.6]. For an introduction to analytic functors and combinatorial species, we redirect the reader to Joyal [20].

Notation 5.2

Given $\textsf{G}$ an endofunctor of $\textsf{Set}$, the category of elements $\textrm{el}(\textsf{G})$ has as objects pairs (E, a) with $a \in \textsf{G}(E)$, and as morphisms between (E, a) and $(E',a')$ maps $f :E \rightarrow E'$ such that $\textsf{G}_f (a) = a'$.

As an intuition to the unfamiliar reader, an element (E, a) in $\textrm{el}(\textsf{G})$ is a witness that a can be produced through $\textsf{G}$ by using elements of E. Morphisms of elements are witnessing how relations between elements of $\textsf{G}(E)$ and $\textsf{G}(E')$ arise from relations between E and $E'$. As a way to define a “smallest” set of elements E such that a can be found in $\textsf{G}(E)$, we rely on transitive objects. We recall that in a category $\mathcal {C}$, if X, A are two objects, the action of $\textrm{Aut}(X)$ on $\textrm{Hom}(X,A)$ is transitive when for every pair $f,g \in \textrm{Hom}(X,A)$, there exists a $h \in \textrm{Aut}(X)$ such that $f \circ h = g$.

Notation 5.3

A transitive object in a category $\mathcal {C}$ is an object X satisfying the following two conditions for every object A of $\mathcal {C}$: (a) the set $\textrm{Hom}(X, A)$ in $\mathcal {C}$ is non-empty; (b) the right action of $\textrm{Aut}(X)$ on $\textrm{Hom}(X, A)$ by composition is transitive.

Notation 5.4

Given an object A in a category $\mathcal {C}$, one can build the slice category ${\mathcal {C}}/{A}$ whose objects are elements of $\textrm{Hom}(B,A)$ when B ranges over objects of $\mathcal {C}$ and morphisms between $c_1 \in \textrm{Hom}(B_1,A)$ and $c_2 \in \textrm{Hom}(B_2, A)$ are maps $f :B_1 \rightarrow B_2$ such that $c_2 \circ f = c_1$.

This notion of slice category can be combined with the one of transitive object to build so-called “weak normal forms”.

Notation 5.5

A weak normal form of an object A in a category $\mathcal {C}$ is a transitive object in ${\mathcal {C}}/{A}$.

A category $\mathcal {C}$ has the weak normal form property whenever every object A has a weak normal form. We are now ready to formulate a definition of analytic functors through the existence of weak normal forms for objects in their category of elements.

Notation 5.6

An endofunctor $\textsf{G}$ of $\textsf{Set}$ is an analytic functor whenever its category of elements $\textrm{el}(\textsf{G})$ has the weak normal form property. Moreover; X is a finite set for every weak normal form $f \in \textrm{Hom}((X, x), (Y,y))$ in ${\textrm{el}(\textsf{G})}/{(Y,y)}$.

Example 5.7

The functor mapping X to $X^{*}$ is analytic, and the weak normal form of a word $(X^{*}, w)$ is $(\textrm{letters}(w), w)$ together with the canonical injection from $\textrm{letters}(w)$ to X. In this specific case, the weak normal forms are in fact initial objects.

Example 5.8

The functor mapping X to $X^{<\alpha }$ is not analytic when $\alpha \ge \omega$, because of the restriction that weak normal forms are defined using finite sets.

Let us now explain how these weak normal forms can be used to define a support associated to the analytic functor, which in turns allows us to build a notion of substructure ordering over initial algebras of analytic functors.

Definition 5.9

Let $\textsf{G}$ be an analytic functor, (X, x) be an element in $\textrm{el}(\textsf{G})$ and $f \in \textrm{Hom}((Y,y),(X,x))$ be a weak normal form in the slice category ${\textrm{el}(\textsf{G})}/{(X,x)}$. We define f(Y) as the support of x in X, written $\textrm{supp}_X(x)$.

Definition 5.10

Let $\textsf{G}$ be an analytic functor and $(\mu \textsf{G}, \delta )$ be an initial algebra of $\textsf{G}$. We say that $a \in \mu \textsf{G}$ is a child of $b \in \mu \textsf{G}$ whenever $a = b$ or $a \in \textrm{supp}_{\mu \textsf{G}}(\delta ^{-1}(b))$. The transitive closure of the children relation is called the substructure ordering of $\mu \textsf{G}$ and written $\mathrel {\sqsubseteq }$.

Example 5.11

The substructure ordering on $\mu \textsf{G}$ for $\textsf{G}(X) :=\textbf{1}+ \varSigma \times X$ is the suffix ordering of words.

We leverage the notion of substructure ordering to define a suitable topology expander over initial algebras of analytic functors. Note that this ordering appears implicitely in the construction of Hasegawa [17, Definition2.7].

Definition 5.12

Let $\textsf{G}':\textsf{Top}\rightarrow \textsf{Top}$ be a lifting of an analytic functor $\textsf{G}$, and $(\mu \textsf{G}, \delta )$ an initial algebra of $\textsf{G}$. We define $\mathsf {E_{\Diamond }}^{\textsf{G}'}$ that maps $\tau$ to the topology generated by $\uparrow _{\mathrel {\sqsubseteq }}{\delta (U)}$ where $U \in \textsf{G}'(\mu \textsf{G}, \tau )$.

We say that $\textsf{lfp}_{\tau }.{\mathsf {E_{\Diamond }}^{\textsf{G}'}}$ is the divisibility topology over $\mu \textsf{G}$.

Theorem 5.13

Let $\textsf{G}':\textsf{Top}\rightarrow \textsf{Top}$ be a lifting of an analytic functor $\textsf{G}$, and $(\mu \textsf{G}, \delta )$ an initial algebra of $\textsf{G}$. Moreover, we suppose that $\textsf{G}'$ preserves inclusions. The map $\mathsf {E_{\Diamond }}^{\textsf{G}'}$ is a topology expander, hence the divisibility topology is Noetherian.

As a sanity check, we can apply Theorem 5.13 to the sets of finite words and finite trees, and recover the subword topology and the tree topology that were obtained in an ad-hoc fashion in Section 4. In addition to validating the usefulness of Theorem 5.13, we believe that these are strong indicators that the topologies introduced prior to this work were the right generalisations of Higman’s word embedding and Kruskal’s tree embedding in a topological setting, and addresses the canonicity issue of the aforementioned topologies.

Lemma 5.14

The subword topology over $\varSigma ^{*}$, (resp. the tree topology over $\textsf{T}(\varSigma )$) is the divisibility topology associated to the inductive construction of finite words (resp. finite trees).

5.2 Divisibility Preorders

We are now going to prove that the divisibility topology correctly generalises the corresponding notions on quasi-orderings. In the case of finite words, this translates to the equation $\textsf{alex}(\le )^* = \textsf{alex}(\le ^*)$ [12, Exercise 9.7.30]. We relate the divisibility topology to the divisibility preorder introduced by Hasegawa [17, Definition 2.7].

Theorem 5.15

Let $\textsf{G}'$ the be the lift of an analytic functor respecting Alexandroff topologies, Noetherian spaces, and embeddings. Then, the divisibility topology of $\mu \textsf{G}$ is the Alexandroff topology of the divisibility preorder of $\mu \textsf{G}$, which is a well-quasi-ordering.

6 Outlook

We have provided a systematic way to place a Noetherian topology over an inductively defined datatype, which is correct with respect to its wqo counterpart whenever it exists. As a byproduct, we obtained a uniform framework that simplifies existing proofs, and serves as an indicator that the pre-existing topologies were the “right generalisations” of their quasi-order counterparts. Let us now briefly highlight some interesting properties of the underlying theory.

Differences with the existing categorical frameworks. The existing categorical frameworks are built around a specific kind of functors [8, 17], while the notion of topology expander only requires talking about one specific set. This allows proving that the ordinal subword topology and the $\alpha$-branching trees are Noetherian, while these escape both the realm of wqos, and of “well-behaved functors” having finite support functions.

Quasi-analytic functors. In fact, the proof of Theorem 5.13, never relies on the finiteness of the support of an element. This means that the definition of analytic functors can be loosened to allow non finite weak normal forms. We do not know whether this notion of “quasi-analytic functor” already exists in the literature.

Transfinite iterations. As the reader might have noticed, all of the least fixed points considered in this paper are obtained using at most $\omega$ steps. This is because the topology expanders that are presented in the paper are all Scott-continuous, i.e., they satisfy the equation $\textsf{E}(\sup _i \tau _i) = \sup _i \textsf{E}(\tau _i)$. While Theorem 3.21 does apply to non Scott-continuous topology expanders, we do not know any reasonable example of such expander.

Lack of ordinal invariants. Even though our proof that the ordinal subword topology is Noetherian is shorter than the original one, it actually provides less information. In particular, it does not provide a bound for ordinal rank of the lattice of closed sets (called the stature of $\varSigma ^{<\alpha }$), whereas a clear bound is provided by the previous approach Goubault-Larrecq et al. [15, Proposition 33]. This limitation already appears in the existing categorical frameworks [8, 17], and we believe that this is inherent to the use of minimal bad sequence arguments.