nLab finiteness space

Redirected from "finiteness spaces".
Finiteness spaces

Finiteness spaces

1. Idea

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

2. Definition

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).

Definition. 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.

3. Properties

  • 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.

4. Examples

  • 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.

5. 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.

Theorem. 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).

Proof. 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.

6. Matrices

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.

7. Linearization

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}.

Examples

  • 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.

9. References

  • 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.