nLab finiteness space

Finiteness spaces

Finiteness spaces


A finiteness space is a set together with a collection of its subsets that behave, in certain ways, like the collection of finite subsets.


Given a set XX and a subset π’°βŠ†P(X)\mathcal{U} \subseteq P(X) of its power set, define

𝒰 βŠ₯={v∈P(X)∣u∩v is finite for all uβˆˆπ’°}.\mathcal{U}^\perp = \{ v \in P(X) \mid u \cap v \;\text{ is finite for all }\; u\in \mathcal{U} \}.

This defines a Galois connection on P(X)P(X).


A finiteness space is a set XX equipped with a π’°βŠ†P(X)\mathcal{U} \subseteq P(X) such that 𝒰=𝒰 βŠ₯βŠ₯\mathcal{U} = \mathcal{U}^{\perp\perp}.

We refer to the elements of 𝒰\mathcal{U} as finitary, and the elements of 𝒰 βŠ₯\mathcal{U}^\perp as cofinitary.


  • All finite subsets of XX belong to 𝒰 βŠ₯\mathcal{U}^\perp for any 𝒰\mathcal{U}. Thus, in a finiteness space all finite subsets are both finitary and cofinitary.

  • Any set of the form 𝒰 βŠ₯\mathcal{U}^\perp is down-closed, i.e. contains all subsets of its elements. Thus, any subset of a finitary subset is finitary, and any subset of a cofinitary subset is cofinitary.

  • Any set of the form 𝒰 βŠ₯\mathcal{U}^\perp is closed under finite unions. Thus, any finite union of finitary subsets is finitary, and any finite union of cofinitary subsets is cofinitary.


  • Taking 𝒰=\mathcal{U} = all finite subsets of XX gives a minimal finiteness structure on XX.

  • Dually, taking 𝒰=\mathcal{U}= all subsets of XX gives a maximal finiteness structure.

  • In fact, if (X,𝒰)(X,\mathcal{U}) is a finiteness space, so is (X,𝒰 βŠ₯)(X,\mathcal{U}^\perp), its dual. The maximal and minimal finiteness structures are dual.

  • We cannot obtain any other finiteness spaces purely by cardinality restriction. For instance, if all countable subsets of XX are finitary, then all cofinitary subsets must be finite, hence XX is maximal. Thus, to obtain finiteness spaces other than the minimal or maximal ones, we must invoke some other structure on XX.

  • Let XX be a poset and 𝒰\mathcal{U} the set of all subsets of XX that are noetherian, i.e. contain no infinite strictly increasing chains. Then this is a finiteness space. Its dual (at least, assuming the axiom of choice) consists of subsets that are artinian (contain no infinite strictly decreasing chains) and narrow (contain no infinite antichains).

  • Let XX be a linearly ordered set and let 𝒰\mathcal{U} the set of all left-finite subsets, i.e. those uu such that u∩{x∣x≀y}u\cap \{ x \mid x \le y\} is finite for all yy. Since this is of the form 𝒱 βŠ₯\mathcal{V}^\perp for 𝒱\mathcal{V} the set of subsets {x∣x≀y}\{x \mid x\le y\}, it is a finiteness structure.

Categories of finiteness spaces

A relation or morphism of finiteness spaces is a relation RR from XX to YY such that

  1. If uβŠ†Xu\subseteq X is finitary, then R[u]={y∈Yβˆ£βˆƒx∈u,xRy}R[u] = \{ y\in Y \mid \exists x\in u, x R y \} is finitary.
  2. If vβŠ†Yv\subseteq Y is cofinitary, then R βˆ’1[v]={x∈Xβˆ£βˆƒy∈v,xRy}R^{-1}[v] = \{ x\in X \mid \exists y\in v, x R y \} is cofinitary.

An equivalent way to say this is that

  • If uβŠ†Xu\subseteq X is finitary and vβŠ†Yv\subseteq Y is cofinitary, then the set {(x,y)∣x∈u∧y∈v∧xRy}βŠ†XΓ—Y\{ (x,y) \mid x\in u \wedge y\in v \wedge x R y \} \subseteq X \times Y has finite images under both projections XΓ—Yβ†’XX\times Y\to X and XΓ—Yβ†’YX\times Y\to Y.

Additionally, in the presence of condition (1), condition (2) is equivalent to its special case when vv is a singleton.

Let FinSp relFinSp_{rel} denote the category of finiteness spaces and relations, and FinSp parFinSp_{par} and FinSp funFinSp_{fun} its wide subcategories in which the morphisms are restricted to be partial functions or functions, respectively.

Note that a partial function lies in FinSp parFinSp_{par} if and only if the preimage of any cofinitary subset is cofinitary. For this is precisely the second condition above specialized to a partial function, while conversely if this holds then for any finitary uβŠ†Xu\subseteq X and cofinitary vβŠ†Yv\subseteq Y, we have a surjection u∩f βˆ’1(v)β†’f(u)∩vu\cap f^{-1}(v) \to f(u) \cap v so that finiteness of the former implies finiteness of the latter.

Monoidal structures

  • All three categories are symmetric monoidal and the inclusions FinSp funβ†ͺFinSp parβ†ͺFinSp relFinSp_{fun} \hookrightarrow FinSp_{par} \hookrightarrow FinSp_{rel} are strict symmetric monoidal.
  • FinSp relFinSp_{rel} is star-autonomous (see Ehrhard).
  • FinSp parFinSp_{par} is closed (see BCJS).

Initial and terminal structures

Let Set parSet_{par} denote the category of sets and partial functions. Note that Set parSet_{par} is equivalent to the category Set *Set_* of pointed sets, and hence in particular is complete and cocomplete.

The following theorem says that FinSp parFinSp_{par} and FinSp funFinSp_{fun} are almost topological concrete categories over Set parSet_{par} and SetSet respectively.


The (faithful) forgetful functors U par:FinSp parβ†’Set parU_{par}:FinSp_{par} \to Set_{par} and U fun:FinSp funβ†’SetU_{fun}:FinSp_{fun} \to Set have initial lifts for all (possibly large) sources {f i:X⇀U(S i)}\{ f_i : X \rightharpoonup U(S_i) \} having the property that for all x∈Xx\in X there exists an ii such that x∈dom(f i)x\in dom(f_i).


The functor U funU_{fun} is simply the pullback U parU_{par} along the inclusion Setβ†ͺSet parSet \hookrightarrow Set_{par}, so it suffices to consider the former, which we denote simply UU.

Let XX be a set and {f i:X⇀U(S i)}\{ f_i : X \rightharpoonup U(S_i) \} a UU-structured source satisfying the given condition, where each (S i,𝒱 i)(S_i,\mathcal{V}_i) is a finiteness space. Let 𝒱=(⋃ if i βˆ’1(𝒱 i βŠ₯)) βŠ₯\mathcal{V} = \big(\bigcup_i f_i^{-1}(\mathcal{V}_i^\perp)\big)^\perp, making XX a finiteness space for which uβŠ†Xu\subseteq X is finitary if and only if u∩f i βˆ’1(v)u \cap f_i^{-1}(v) is finite for all cofinitary vβŠ†S iv\subseteq S_i. Thus each f if_i becomes a morphism in FinSp parFinSp_{par}.

For universality, suppose given a finiteness space TT and a partial function g:U(T)⇀Xg:U(T)\rightharpoonup X such that each composite f i∘gf_i\circ g is a morphism in FinSp parFinSp_{par}. The latter means that (f i∘g) βˆ’1(v)(f_i\circ g)^{-1}(v) is cofinitary for all cofinitary vβŠ†S iv\subseteq S_i, which is to say u∩g βˆ’1(f i βˆ’1(v))u \cap g^{-1}(f_i^{-1}(v)) is finite for all finitary uβŠ†Tu\subseteq T. It follows that g(u)∩f i βˆ’1(v)g(u) \cap f_i^{-1}(v) is finite (being a surjective image of u∩g βˆ’1(f i βˆ’1(v))u \cap g^{-1}(f_i^{-1}(v))), hence g(u)g(u) is finitary, i.e. condition (1) in the definition of morphism holds.

Thus it remains to show that for any x∈Xx\in X the preimage g βˆ’1(x)g^{-1}(x) is cofinitary in TT. By assumption, there exists an ii such that x∈dom(f i)x\in dom(f_i), which is to say x∈f i βˆ’1(f i(x))x\in f_i^{-1}(f_i(x)). But then g βˆ’1(x)βŠ†g βˆ’1(f i βˆ’1(f i(x)))g^{-1}(x) \subseteq g^{-1}(f_i^{-1}(f_i(x))), hence is cofinitary.

In the case of U funU_{fun}, the extra condition reduces to the statement that if XX is inhabited then so is the set of indices ii. This condition is necessary: empty U funU_{fun}-structured sources on inhabited sets do not have initial lifts. The only candidate is the maximal finiteness structure in which all subsets are finitary and only finite sets are cofinitary, but not all functions into a maximal finiteness space are finiteness functions (only those with finite fibers).

In particular, FinSp funFinSp_{fun} does not have a terminal object, though it does have all inhabited limits, and the forgetful functor FinSp fun→SetFinSp_{fun} \to Set is a Grothendieck fibration.

A similar argument shows that FinSp parFinSp_{par} has all inhabited limits. (The above is essentially the argument given for this in BCJS, unraveled into an explicit construction of limits in Set parSet_{par} in terms of the equivalence to Set *Set_*.) But FinSp parFinSp_{par} also has a terminal object, namely the empty set with its unique finiteness structure, so it is a complete category.

In fact, FinSp parFinSp_{par} is also a cocomplete category, as shown in BCJS. But its coequalizers are not preserved by U parU_{par}, and in particular not constructed as final lifts of U parU_{par}-structured sinks.


Let RR be any semiring; we can define a category FMat(R)FMat(R) as follows:

  • Its objects are finiteness spaces.
  • Its morphisms Xβ†’YX\to Y are functions M:XΓ—Yβ†’RM:X\times Y \to R whose support {(x,y)∣M(x,y)β‰ 0}\{ (x,y) \mid M(x,y) \neq 0 \} is a morphism Xβ†’YX\to Y in FinSp relFinSp_{rel}. We write this morphism in FinSp relFinSp_{rel} as supp(M):Xβ†’Ysupp(M):X\to Y.

The composite of M:X→YM:X\to Y and N:Y→ZN:Y\to Z is defined by

(NM)(x,z)=βˆ‘ M(x,y)β‰ 0β‰ N(y,z)N(y,z)β‹…M(x,y). (N M)(x,z) = \sum_{M(x,y)\neq 0 \neq N(y,z)} N(y,z) \cdot M(x,y).

To see that this is well-defined, first note that by assumption, for any xx the set {y∣M(x,y)β‰ 0}\{ y \mid M(x,y)\neq 0 \} is finitary, and for any zz the set {y∣N(y,z)β‰ 0}\{ y \mid N(y,z)\neq 0 \} is cofinitary. Thus their intersection is finite, so the above sum is finite and thus makes sense. Now to check that NMN M is indeed a morphism Xβ†’YX\to Y in FMat(R)FMat(R), note that if (NM)(x,z)β‰ 0(N M)(x,z)\neq 0 it must be that there exists a yy such thath M(x,y)β‰ 0β‰ N(y,z)M(x,y)\neq 0 \neq N(y,z), and therefore (supp(N)∘supp(M))(x,z)(supp(N) \circ supp(M))(x,z) holds. In other words, supp(NM)βŠ†supp(N)∘supp(M)supp(N M) \subseteq supp(N) \circ supp(M), and therefore supp(NM)supp(N M) is also a morphism in FinSp relFinSp_{rel}.

It is straightforward to check associativity and unitality, so we have a category FMat(R)FMat(R). We note the following properties:

  • FMat(R)FMat(R) is enriched over abelian monoids (abelian groups if RR is a ring), and indeed over RR-modules.

  • FMat(R)FMat(R) has a zero object (the empty finiteness space) and finite biproducts (disjoint unions of finiteness spaces).

  • Any distributive lattice is a semiring with join as addition and meet as multiplication. In the case R={βŠ₯,⊀}R= \{\bot,\top\} the set of truth values, we have FMat(R)=FinSp relFMat(R) = FinSp_{rel}.

  • The proof above that supp(NM)βŠ†supp(N)∘supp(M)supp(N M) \subseteq supp(N) \circ supp(M), plus a simpler argument in the unary case, shows that for any RR we have an identity-on-objects colax functor supp:FMat(R)β†’FinSp relsupp: FMat(R) \to FinSp_{rel}. (For general RR, FMat(R)FMat(R) is not a 2-category, but it is when RR is a distributive lattice, including the case of FinSp relFinSp_{rel}; thus this makes sense.)

  • For general RR, the category FMat(R)FMat(R) is star-autonomous, and the functor supp:FMat(R)β†’FinSp relsupp: FMat(R) \to FinSp_{rel} preserves this structure strictly.

  • Any morphism H:Xβ†’YH : X\to Y in FinSp relFinSp_{rel} induces a morphism H^:Xβ†’Y\hat{H}:X\to Y in Mat(R)Mat(R) by setting H^(x,y)=1\hat{H}(x,y) = 1 if H(x,y)H(x,y) and 00 otherwise. However, this does not define a functor FinSp relβ†’FMat(R)FinSp_{rel} \to FMat(R) since morphisms of the form H^\hat{H} need not be closed under composition, as the composite of two such might involve a finite sum of copies of 11. There are two cases when this does work: when 11 is an additive idempotent in RR (such as when RR is a distributive lattice), and when we restrict the domain to FinSp parFinSp_{par}. In particular, we have a strict symmetric monoidal functor Ο‡:FinSp parβ†’FMat(R)\chi : FinSp_{par} \to FMat(R) for any RR that is a partial section of suppsupp.


Let (X,𝒰)(X,\mathcal{U}) be a finiteness space and AA an abelian group (or more generally an abelian monoid), and define

A⟨X⟩={f:Xβ†’A∣supp(f)βˆˆπ’°} A \langle X\rangle = \{ f : X\to A \mid supp(f) \in \mathcal{U} \}

where supp(f)={x∈X∣f(x)β‰ 0}supp(f) = \{ x\in X \mid f(x)\neq 0 \} is the support of ff. Then A⟨X⟩A\langle X\rangle is an abelian group called the linearization of XX (with coefficients in AA).

Note that if A={βŠ₯,⊀}A=\{\bot,\top\}, then A⟨X⟩A\langle X\rangle is just the set 𝒰\mathcal{U} of finitary subsets of XX.

It is shown in BCJS that if XX is a partial finiteness monoid (i.e. a monoid in FinSp parFinSp_{par}) and RR a ring, then R⟨X⟩R\langle X\rangle is also a ring with

(fβ‹…g)(m)=βˆ‘ (m 1,m 2)∈X m(f,g)f(m 1)β‹…g(m 2) (f\cdot g)(m) = \sum_{(m_1,m_2)\in X_m(f,g)} f(m_1)\cdot g(m_2)

where X m(f,g)X_m(f,g) is the set of pairs (m 1,m 2)∈supp(f)Γ—supp(g)(m_1,m_2)\in supp(f) \times supp(g) such that m 1β‹…m 2=mm_1 \cdot m_2 = m. In fact RR need only be a semiring (in which case so is R⟨X⟩R\langle X\rangle).

If XX is merely a monoid in FinSp relFinSp_{rel}, then the above multiplication is still defined, but may not be associative or unital. This can be explained more abstractly as follows. We have R⟨X⟩=FMat(R)(1,X)R\langle X\rangle = FMat(R)(1,X), where 11 is the one-element finiteness space (the monoidal unit, which is terminal in FinSp funFinSp_{fun} but not in any of the other categories of finitenes spaces). Thus, R⟨X⟩R\langle X\rangle inherits a multiplicative monoid structure as soon as XX is a monoid object in FMat(R)FMat(R). As noted above, we have a monoidal functor Ο‡:FinSp parβ†’FMat(R)\chi : FinSp_{par} \to FMat(R), which therefore preserves monoids; but no such functor whose domain is FinSp relFinSp_{rel}.


  • If XX is a minimal finiteness space, then the linearization A⟨X⟩A\langle X\rangle is then the copower of AA by the set XX in Ab. Any monoid (or partial monoid) MM is a finiteness monoid with the minimal finiteness structure, and when RR is a ring the resulting ring structure on R⟨M⟩R\langle M\rangle is induced on the basis elements by the multiplication of MM. When MM is a group GG, this is the group algebra R[G]R[G].

  • If XX is a poset whose finitary subsets are the artinian and narrow ones, and whose multiplication preserves the strict order on each side, then it is a finitenes monoid, and its linearization is the ring of Ribenboim power series from XX with coefficients in RR (see BCJS). Thus, this includes rings of formal power series, formal Laurent series?, polynomials, Laurent polynomials, and Hahn series.

  • If XX is a linearly ordered abelian group and the finitary subsets are the left-finite ones, then its linearization is the corresponding Novikov field.

  • As shown in BCJS, other examples include Puiseux series, formal power series over a free monoid, and polynomials of bounded degree.

  • Finiteness spaces were defined by analogy to coherence spaces in which the property β€œis finite” is replaced by β€œis a subsingleton”. Thus, both are special cases of arity spaces for two different sets of arities.


  • T. Ehrhard, Finiteness spaces, Mathematical Structures in Computer Science 15, pp. 615–646 (2005)
  • Richard Blute, Robin Cockett, Pierre-Alain Jacqmin, and Philip Scott, Finiteness spaces and generalized power series, Electronic Notes in Theoretical Computer Science, 341 (2018), 5-22, doi, arXiv:1805.09836

Last revised on July 24, 2019 at 17:24:45. See the history of this page for a list of all contributions to it.