\documentclass[12pt,titlepage]{article} \usepackage{amsmath} \usepackage{mathrsfs} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsthm} \usepackage{mathtools} \usepackage{graphicx} \usepackage{color} \usepackage{ucs} \usepackage[utf8x]{inputenc} \usepackage{xparse} \usepackage{hyperref} %----Macros---------- % % Unresolved issues: % % \righttoleftarrow % \lefttorightarrow % % \color{} with HTML colorspec % \bgcolor % \array with options (without options, it's equivalent to the matrix environment) % Of the standard HTML named colors, white, black, red, green, blue and yellow % are predefined in the color package. Here are the rest. \definecolor{aqua}{rgb}{0, 1.0, 1.0} \definecolor{fuschia}{rgb}{1.0, 0, 1.0} \definecolor{gray}{rgb}{0.502, 0.502, 0.502} \definecolor{lime}{rgb}{0, 1.0, 0} \definecolor{maroon}{rgb}{0.502, 0, 0} \definecolor{navy}{rgb}{0, 0, 0.502} \definecolor{olive}{rgb}{0.502, 0.502, 0} \definecolor{purple}{rgb}{0.502, 0, 0.502} \definecolor{silver}{rgb}{0.753, 0.753, 0.753} \definecolor{teal}{rgb}{0, 0.502, 0.502} % Because of conflicts, \space and \mathop are converted to % \itexspace and \operatorname during preprocessing. % itex: \space{ht}{dp}{wd} % % Height and baseline depth measurements are in units of tenths of an ex while % the width is measured in tenths of an em. \makeatletter \newdimen\itex@wd% \newdimen\itex@dp% \newdimen\itex@thd% \def\itexspace#1#2#3{\itex@wd=#3em% \itex@wd=0.1\itex@wd% \itex@dp=#2ex% \itex@dp=0.1\itex@dp% \itex@thd=#1ex% \itex@thd=0.1\itex@thd% \advance\itex@thd\the\itex@dp% \makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}} \makeatother % \tensor and \multiscript \makeatletter \newif\if@sup \newtoks\@sups \def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}% \def\reset@sup{\@supfalse\@sups={}}% \def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else% \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}% \else \append@sup#2 \@suptrue \fi% \expandafter\mk@scripts\fi} \def\tensor#1#2{\reset@sup#1\mk@scripts#2_/} \def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2% \reset@sup\mk@scripts#3_/} \makeatother % \slash \makeatletter \newbox\slashbox \setbox\slashbox=\hbox{$/$} \def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$} \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa \copy\slashbox \kern-\@tempdima \box\@tempboxa} \def\slash{\protect\itex@pslash} \makeatother % math-mode versions of \rlap, etc % from Alexander Perlis, "A complement to \smash, \llap, and lap" % http://math.arizona.edu/~aprl/publications/mathclap/ \def\clap#1{\hbox to 0pt{\hss#1\hss}} \def\mathllap{\mathpalette\mathllapinternal} \def\mathrlap{\mathpalette\mathrlapinternal} \def\mathclap{\mathpalette\mathclapinternal} \def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}} \def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}} \def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}} % Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2} \let\oldroot\root \def\root#1#2{\oldroot #1 \of{#2}} \renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}} % Manually declare the txfonts symbolsC font \DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n} \SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n} \DeclareFontSubstitution{U}{txsyc}{m}{n} % Manually declare the stmaryrd font \DeclareSymbolFont{stmry}{U}{stmry}{m}{n} \SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n} % Manually declare the MnSymbolE font \DeclareFontFamily{OMX}{MnSymbolE}{} \DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n} \SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n} \DeclareFontShape{OMX}{MnSymbolE}{m}{n}{ <-6> MnSymbolE5 <6-7> MnSymbolE6 <7-8> MnSymbolE7 <8-9> MnSymbolE8 <9-10> MnSymbolE9 <10-12> MnSymbolE10 <12-> MnSymbolE12}{} % Declare specific arrows from txfonts without loading the full package \makeatletter \def\re@DeclareMathSymbol#1#2#3#4{% \let#1=\undefined \DeclareMathSymbol{#1}{#2}{#3}{#4}} \re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116} \re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116} \re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117} \re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117} \re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118} \re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118} \re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119} \re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119} \re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46} \re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121} \re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121} \re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12} \re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64} \re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6} \re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77} \re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77} \makeatother % \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE \makeatletter \def\Decl@Mn@Delim#1#2#3#4{% \if\relax\noexpand#1% \let#1\undefined \fi \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}} \def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}} \def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}} \Decl@Mn@Open{\llangle}{mnomx}{'164} \Decl@Mn@Close{\rrangle}{mnomx}{'171} \Decl@Mn@Open{\lmoustache}{mnomx}{'245} \Decl@Mn@Close{\rmoustache}{mnomx}{'244} \makeatother % Widecheck \makeatletter \DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}} \def\@widecheck#1#2{% \setbox\z@\hbox{\m@th$#1#2$}% \setbox\tw@\hbox{\m@th$#1% \widehat{% \vrule\@width\z@\@height\ht\z@ \vrule\@height\z@\@width\wd\z@}$}% \dp\tw@-\ht\z@ \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@ \setbox\tw@\hbox{% \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box \tw@}}}% {\ooalign{\box\tw@ \cr \box\z@}}} \makeatother % \mathraisebox{voffset}[height][depth]{something} \makeatletter \NewDocumentCommand\mathraisebox{moom}{% \IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{% \IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}% }{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}% \mathpalette\@temp{#4}} \makeatletter % udots (taken from yhmath) \makeatletter \def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.} \mkern2mu\raise4\p@\hbox{.}\mkern1mu \raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}} \makeatother %% Fix array \newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}} %% \itexnum is a noop \newcommand{\itexnum}[1]{#1} %% Renaming existing commands \newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}} \newcommand{\widevec}{\overrightarrow} \newcommand{\darr}{\downarrow} \newcommand{\nearr}{\nearrow} \newcommand{\nwarr}{\nwarrow} \newcommand{\searr}{\searrow} \newcommand{\swarr}{\swarrow} \newcommand{\curvearrowbotright}{\curvearrowright} \newcommand{\uparr}{\uparrow} \newcommand{\downuparrow}{\updownarrow} \newcommand{\duparr}{\updownarrow} \newcommand{\updarr}{\updownarrow} \newcommand{\gt}{>} \newcommand{\lt}{<} \newcommand{\map}{\mapsto} \newcommand{\embedsin}{\hookrightarrow} \newcommand{\Alpha}{A} \newcommand{\Beta}{B} \newcommand{\Zeta}{Z} \newcommand{\Eta}{H} \newcommand{\Iota}{I} \newcommand{\Kappa}{K} \newcommand{\Mu}{M} \newcommand{\Nu}{N} \newcommand{\Rho}{P} \newcommand{\Tau}{T} \newcommand{\Upsi}{\Upsilon} \newcommand{\omicron}{o} \newcommand{\lang}{\langle} \newcommand{\rang}{\rangle} \newcommand{\Union}{\bigcup} \newcommand{\Intersection}{\bigcap} \newcommand{\Oplus}{\bigoplus} \newcommand{\Otimes}{\bigotimes} \newcommand{\Wedge}{\bigwedge} \newcommand{\Vee}{\bigvee} \newcommand{\coproduct}{\coprod} \newcommand{\product}{\prod} \newcommand{\closure}{\overline} \newcommand{\integral}{\int} \newcommand{\doubleintegral}{\iint} \newcommand{\tripleintegral}{\iiint} \newcommand{\quadrupleintegral}{\iiiint} \newcommand{\conint}{\oint} \newcommand{\contourintegral}{\oint} \newcommand{\infinity}{\infty} \newcommand{\bottom}{\bot} \newcommand{\minusb}{\boxminus} \newcommand{\plusb}{\boxplus} \newcommand{\timesb}{\boxtimes} \newcommand{\intersection}{\cap} \newcommand{\union}{\cup} \newcommand{\Del}{\nabla} \newcommand{\odash}{\circleddash} \newcommand{\negspace}{\!} \newcommand{\widebar}{\overline} \newcommand{\textsize}{\normalsize} \renewcommand{\scriptsize}{\scriptstyle} \newcommand{\scriptscriptsize}{\scriptscriptstyle} \newcommand{\mathfr}{\mathfrak} \newcommand{\statusline}[2]{#2} \newcommand{\tooltip}[2]{#2} \newcommand{\toggle}[2]{#2} % Theorem Environments \theoremstyle{plain} \newtheorem{theorem}{Theorem} \newtheorem{lemma}{Lemma} \newtheorem{prop}{Proposition} \newtheorem{cor}{Corollary} \newtheorem*{utheorem}{Theorem} \newtheorem*{ulemma}{Lemma} \newtheorem*{uprop}{Proposition} \newtheorem*{ucor}{Corollary} \theoremstyle{definition} \newtheorem{defn}{Definition} \newtheorem{example}{Example} \newtheorem*{udefn}{Definition} \newtheorem*{uexample}{Example} \theoremstyle{remark} \newtheorem{remark}{Remark} \newtheorem{note}{Note} \newtheorem*{uremark}{Remark} \newtheorem*{unote}{Note} %------------------------------------------------------------------- \begin{document} %------------------------------------------------------------------- \section*{finiteness space} \hypertarget{finiteness_spaces}{}\section*{{Finiteness spaces}}\label{finiteness_spaces} \noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak \noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak \noindent\hyperlink{properties}{Properties}\dotfill \pageref*{properties} \linebreak \noindent\hyperlink{examples}{Examples}\dotfill \pageref*{examples} \linebreak \noindent\hyperlink{categories_of_finiteness_spaces}{Categories of finiteness spaces}\dotfill \pageref*{categories_of_finiteness_spaces} \linebreak \noindent\hyperlink{monoidal_structures}{Monoidal structures}\dotfill \pageref*{monoidal_structures} \linebreak \noindent\hyperlink{initial_and_terminal_structures}{Initial and terminal structures}\dotfill \pageref*{initial_and_terminal_structures} \linebreak \noindent\hyperlink{Matrices}{Matrices}\dotfill \pageref*{Matrices} \linebreak \noindent\hyperlink{linearization}{Linearization}\dotfill \pageref*{linearization} \linebreak \noindent\hyperlink{examples_2}{Examples}\dotfill \pageref*{examples_2} \linebreak \noindent\hyperlink{related_pages}{Related pages}\dotfill \pageref*{related_pages} \linebreak \noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak \hypertarget{idea}{}\subsection*{{Idea}}\label{idea} A \textbf{finiteness space} is a [[set]] together with a collection of its subsets that behave, in certain ways, like the collection of finite subsets. \hypertarget{definition}{}\subsection*{{Definition}}\label{definition} Given a set $X$ and a subset $\mathcal{U} \subseteq P(X)$ of its [[power set]], define \begin{displaymath} \mathcal{U}^\perp = \{ v \in P(X) \mid u \cap v \;\text{ is finite for all }\; u\in \mathcal{U} \}. \end{displaymath} This defines a [[Galois connection]] on $P(X)$. \begin{udefn} A \textbf{finiteness space} is a set $X$ equipped with a $\mathcal{U} \subseteq P(X)$ such that $\mathcal{U} = \mathcal{U}^{\perp\perp}$. \end{udefn} We refer to the elements of $\mathcal{U}$ as \textbf{finitary}, and the elements of $\mathcal{U}^\perp$ as \textbf{cofinitary}. \hypertarget{properties}{}\subsection*{{Properties}}\label{properties} \begin{itemize}% \item All finite subsets of $X$ belong to $\mathcal{U}^\perp$ for any $\mathcal{U}$. Thus, in a finiteness space all finite subsets are both finitary and cofinitary. \item 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. \item 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. \end{itemize} \hypertarget{examples}{}\subsection*{{Examples}}\label{examples} \begin{itemize}% \item Taking $\mathcal{U} =$ all finite subsets of $X$ gives a \textbf{minimal} finiteness structure on $X$. \item Dually, taking $\mathcal{U}=$ all subsets of $X$ gives a \textbf{maximal} finiteness structure. \item In fact, if $(X,\mathcal{U})$ is a finiteness space, so is $(X,\mathcal{U}^\perp)$, its \textbf{dual}. The maximal and minimal finiteness structures are dual. \item We cannot obtain any other finiteness spaces purely by cardinality restriction. For instance, if all countable subsets of $X$ are finitary, then all cofinitary subsets must be finite, hence $X$ is maximal. Thus, to obtain finiteness spaces other than the minimal or maximal ones, we must invoke some other structure on $X$. \item Let $X$ be a [[poset]] and $\mathcal{U}$ the set of all subsets of $X$ that are \emph{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 \emph{artinian} (contain no infinite strictly decreasing chains) and \emph{narrow} (contain no infinite [[antichains]]). \item Let $X$ be a [[linearly ordered set]] and let $\mathcal{U}$ the set of all \emph{left-finite} subsets, i.e. those $u$ such that $u\cap \{ x \mid x \le y\}$ is finite for all $y$. Since this is of the form $\mathcal{V}^\perp$ for $\mathcal{V}$ the set of subsets $\{x \mid x\le y\}$, it is a finiteness structure. \end{itemize} \hypertarget{categories_of_finiteness_spaces}{}\subsection*{{Categories of finiteness spaces}}\label{categories_of_finiteness_spaces} A \textbf{relation} or \textbf{morphism} of finiteness spaces is a [[relation]] $R$ from $X$ to $Y$ such that \begin{enumerate}% \item If $u\subseteq X$ is finitary, then $R[u] = \{ y\in Y \mid \exists x\in u, x R y \}$ is finitary. \item If $v\subseteq Y$ is cofinitary, then $R^{-1}[v] = \{ x\in X \mid \exists y\in v, x R y \}$ is cofinitary. \end{enumerate} An equivalent way to say this is that \begin{itemize}% \item If $u\subseteq X$ is finitary and $v\subseteq Y$ is cofinitary, then the set $\{ (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\times Y\to X$ and $X\times Y\to Y$. \end{itemize} Additionally, in the presence of condition (1), condition (2) is equivalent to its special case when $v$ is a [[singleton]]. Let $FinSp_{rel}$ denote the category of finiteness spaces and relations, and $FinSp_{par}$ and $FinSp_{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_{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\subseteq X$ and cofinitary $v\subseteq Y$, we have a surjection $u\cap f^{-1}(v) \to f(u) \cap v$ so that finiteness of the former implies finiteness of the latter. \hypertarget{monoidal_structures}{}\subsubsection*{{Monoidal structures}}\label{monoidal_structures} \begin{itemize}% \item All three categories are [[symmetric monoidal category|symmetric monoidal]] and the inclusions $FinSp_{fun} \hookrightarrow FinSp_{par} \hookrightarrow FinSp_{rel}$ are strict symmetric monoidal. \item $FinSp_{rel}$ is [[star-autonomous]] (see \hyperlink{Ehrhard05}{Ehrhard}). \item $FinSp_{par}$ is [[closed monoidal category|closed]] (see \hyperlink{BCJS18}{BCJS}). \end{itemize} \hypertarget{initial_and_terminal_structures}{}\subsubsection*{{Initial and terminal structures}}\label{initial_and_terminal_structures} Let $Set_{par}$ denote the category of sets and [[partial functions]]. Note that $Set_{par}$ is equivalent to the category $Set_*$ of [[pointed sets]], and hence in particular is complete and cocomplete. The following theorem says that $FinSp_{par}$ and $FinSp_{fun}$ are \emph{almost} [[topological concrete categories]] over $Set_{par}$ and $Set$ respectively. \begin{utheorem} The ([[faithful functor|faithful]]) forgetful functors $U_{par}:FinSp_{par} \to Set_{par}$ and $U_{fun}:FinSp_{fun} \to Set$ have [[initial lifts]] for all (possibly large) [[sink|sources]] $\{ f_i : X \rightharpoonup U(S_i) \}$ having the property that for all $x\in X$ there exists an $i$ such that $x\in dom(f_i)$. \end{utheorem} \begin{proof} The functor $U_{fun}$ is simply the pullback $U_{par}$ along the inclusion $Set \hookrightarrow Set_{par}$, so it suffices to consider the former, which we denote simply $U$. Let $X$ be a set and $\{ f_i : X \rightharpoonup U(S_i) \}$ a $U$-structured [[sink|source]] satisfying the given condition, where each $(S_i,\mathcal{V}_i)$ is a finiteness space. Let $\mathcal{V} = \big(\bigcup_i f_i^{-1}(\mathcal{V}_i^\perp)\big)^\perp$, making $X$ a finiteness space for which $u\subseteq X$ is finitary if and only if $u \cap f_i^{-1}(v)$ is finite for all cofinitary $v\subseteq S_i$. Thus each $f_i$ becomes a morphism in $FinSp_{par}$. For universality, suppose given a finiteness space $T$ and a partial function $g:U(T)\rightharpoonup X$ such that each composite $f_i\circ g$ is a morphism in $FinSp_{par}$. The latter means that $(f_i\circ g)^{-1}(v)$ is cofinitary for all cofinitary $v\subseteq S_i$, which is to say $u \cap g^{-1}(f_i^{-1}(v))$ is finite for all finitary $u\subseteq T$. It follows that $g(u) \cap f_i^{-1}(v)$ is finite (being a surjective image of $u \cap g^{-1}(f_i^{-1}(v))$), hence $g(u)$ is finitary, i.e. condition (1) in the definition of morphism holds. Thus it remains to show that for any $x\in X$ the preimage $g^{-1}(x)$ is cofinitary in $T$. By assumption, there exists an $i$ such that $x\in dom(f_i)$, which is to say $x\in f_i^{-1}(f_i(x))$. But then $g^{-1}(x) \subseteq g^{-1}(f_i^{-1}(f_i(x)))$, hence is cofinitary. \end{proof} In the case of $U_{fun}$, the extra condition reduces to the statement that if $X$ is inhabited then so is the set of indices $i$. This condition is necessary: empty $U_{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_{fun}$ does not have a terminal object, though it does have all inhabited limits, and the forgetful functor $FinSp_{fun} \to Set$ is a Grothendieck fibration. A similar argument shows that $FinSp_{par}$ has all inhabited limits. (The above is essentially the argument given for this in \hyperlink{BCJS18}{BCJS}, unraveled into an explicit construction of limits in $Set_{par}$ in terms of the equivalence to $Set_*$.) But $FinSp_{par}$ also has a terminal object, namely the empty set with its unique finiteness structure, so it is a [[complete category]]. In fact, $FinSp_{par}$ is also a [[cocomplete category]], as shown in \hyperlink{BCJS18}{BCJS}. But its coequalizers are not preserved by $U_{par}$, and in particular not constructed as final lifts of $U_{par}$-structured sinks. \hypertarget{Matrices}{}\subsection*{{Matrices}}\label{Matrices} Let $R$ be any [[semiring]]; we can define a category $FMat(R)$ as follows: \begin{itemize}% \item Its objects are finiteness spaces. \item Its morphisms $X\to Y$ are functions $M:X\times Y \to R$ whose support $\{ (x,y) \mid M(x,y) \neq 0 \}$ is a morphism $X\to Y$ in $FinSp_{rel}$. We write this morphism in $FinSp_{rel}$ as $supp(M):X\to Y$. \end{itemize} The composite of $M:X\to Y$ and $N:Y\to Z$ is defined by \begin{displaymath} (N M)(x,z) = \sum_{M(x,y)\neq 0 \neq N(y,z)} N(y,z) \cdot M(x,y). \end{displaymath} To see that this is well-defined, first note that by assumption, for any $x$ the set $\{ y \mid M(x,y)\neq 0 \}$ is finitary, and for any $z$ the set $\{ 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 $N M$ is indeed a morphism $X\to Y$ in $FMat(R)$, note that if $(N M)(x,z)\neq 0$ it must be that there exists a $y$ such thath $M(x,y)\neq 0 \neq N(y,z)$, and therefore $(supp(N) \circ supp(M))(x,z)$ holds. In other words, $supp(N M) \subseteq supp(N) \circ supp(M)$, and therefore $supp(N M)$ is also a morphism in $FinSp_{rel}$. It is straightforward to check associativity and unitality, so we have a category $FMat(R)$. We note the following properties: \begin{itemize}% \item $FMat(R)$ is enriched over abelian monoids (abelian groups if $R$ is a ring), and indeed over $R$-modules. \item $FMat(R)$ has a [[zero object]] (the empty finiteness space) and finite [[biproducts]] (disjoint unions of finiteness spaces). \item Any [[distributive lattice]] is a semiring with [[join]] as addition and [[meet]] as multiplication. In the case $R= \{\bot,\top\}$ the set of [[truth values]], we have $FMat(R) = FinSp_{rel}$. \item The proof above that $supp(N M) \subseteq supp(N) \circ supp(M)$, plus a simpler argument in the unary case, shows that for any $R$ we have an identity-on-objects [[colax functor]] $supp: FMat(R) \to FinSp_{rel}$. (For general $R$, $FMat(R)$ is not a 2-category, but it is when $R$ is a distributive lattice, including the case of $FinSp_{rel}$; thus this makes sense.) \item For general $R$, the category $FMat(R)$ is [[star-autonomous]], and the functor $supp: FMat(R) \to FinSp_{rel}$ preserves this structure strictly. \item Any morphism $H : X\to Y$ in $FinSp_{rel}$ induces a morphism $\hat{H}:X\to Y$ in $Mat(R)$ by setting $\hat{H}(x,y) = 1$ if $H(x,y)$ and $0$ otherwise. However, this does not define a functor $FinSp_{rel} \to FMat(R)$ since morphisms of the form $\hat{H}$ need not be closed under composition, as the composite of two such might involve a finite sum of copies of $1$. There are two cases when this does work: when $1$ is an additive idempotent in $R$ (such as when $R$ is a distributive lattice), and when we restrict the domain to $FinSp_{par}$. In particular, we have a strict symmetric monoidal functor $\chi : FinSp_{par} \to FMat(R)$ for any $R$ that is a partial section of $supp$. \end{itemize} \hypertarget{linearization}{}\subsection*{{Linearization}}\label{linearization} Let $(X,\mathcal{U})$ be a finiteness space and $A$ an [[abelian group]] (or more generally an abelian [[monoid]]), and define \begin{displaymath} A \langle X\rangle = \{ f : X\to A \mid supp(f) \in \mathcal{U} \} \end{displaymath} where $supp(f) = \{ x\in X \mid f(x)\neq 0 \}$ is the [[support]] of $f$. Then $A\langle X\rangle$ is an abelian group called the \textbf{linearization} of $X$ (with coefficients in $A$). Note that if $A=\{\bot,\top\}$, then $A\langle X\rangle$ is just the set $\mathcal{U}$ of finitary subsets of $X$. It is shown in \hyperlink{BCJS18}{BCJS} that if $X$ is a partial finiteness monoid (i.e. a monoid in $FinSp_{par}$) and $R$ a [[ring]], then $R\langle X\rangle$ is also a ring with \begin{displaymath} (f\cdot g)(m) = \sum_{(m_1,m_2)\in X_m(f,g)} f(m_1)\cdot g(m_2) \end{displaymath} where $X_m(f,g)$ is the set of pairs $(m_1,m_2)\in supp(f) \times supp(g)$ such that $m_1 \cdot m_2 = m$. In fact $R$ need only be a semiring (in which case so is $R\langle X\rangle$). If $X$ is merely a monoid in $FinSp_{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\langle X\rangle = FMat(R)(1,X)$, where $1$ is the one-element finiteness space (the monoidal unit, which is terminal in $FinSp_{fun}$ but not in any of the other categories of finitenes spaces). Thus, $R\langle X\rangle$ inherits a multiplicative monoid structure as soon as $X$ is a monoid object in $FMat(R)$. As noted above, we have a monoidal functor $\chi : FinSp_{par} \to FMat(R)$, which therefore preserves monoids; but no such functor whose domain is $FinSp_{rel}$. \hypertarget{examples_2}{}\subsubsection*{{Examples}}\label{examples_2} \begin{itemize}% \item If $X$ is a minimal finiteness space, then the linearization $A\langle X\rangle$ is then the [[copower]] of $A$ by the set $X$ in [[Ab]]. Any monoid (or partial monoid) $M$ is a finiteness monoid with the minimal finiteness structure, and when $R$ is a ring the resulting ring structure on $R\langle M\rangle$ is induced on the basis elements by the multiplication of $M$. When $M$ is a group $G$, this is the [[group algebra]] $R[G]$. \item If $X$ 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 $X$ with coefficients in $R$ (see \hyperlink{BCJS18}{BCJS}). Thus, this includes rings of [[formal power series]], [[formal Laurent series]], [[polynomials]], [[Laurent polynomials]], and [[Hahn series]]. \item If $X$ is a linearly ordered abelian group and the finitary subsets are the left-finite ones, then its linearization is the corresponding [[Novikov field]]. \item As shown in \hyperlink{BCJS18}{BCJS}, other examples include [[Puiseux series]], formal power series over a free monoid, and polynomials of bounded degree. \end{itemize} \hypertarget{related_pages}{}\subsection*{{Related pages}}\label{related_pages} \begin{itemize}% \item 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. \end{itemize} \hypertarget{references}{}\subsection*{{References}}\label{references} \begin{itemize}% \item T. Ehrhard, \emph{Finiteness spaces}, Mathematical Structures in Computer Science 15, pp. 615--646 (2005) \end{itemize} \begin{itemize}% \item Richard Blute, Robin Cockett, Pierre-Alain Jacqmin, and Philip Scott, \emph{Finiteness spaces and generalized power series}, Electronic Notes in Theoretical Computer Science, 341 (2018), 5-22, \href{https://doi.org/10.1016/j.entcs.2018.11.002}{doi}, \href{https://arxiv.org/abs/1805.09836}{arXiv:1805.09836} \end{itemize} [[!redirects finiteness spaces]] \end{document}