Finiteness spaces and generalized power series

TL;DR

This paper generalizes Ribenboim's construction of rings of generalized power series using finiteness spaces, providing a categorical framework that includes examples like Puiseux and formal power series.

Contribution

It introduces a categorical model of finiteness spaces with partial functions, extending Ribenboim's power series construction within this framework.

Findings

Category of finiteness spaces is symmetric monoidal closed, complete, and cocomplete.

Constructs rings of generalized power series from internal monoids and rings in this category.

Includes examples such as Puiseux series and formal power series from free monoids.

Abstract

We consider Ribenboim's construction of rings of generalized power series. Ribenboim's construction makes use of a special class of partially ordered monoids and a special class of their subsets. While the restrictions he imposes might seem conceptually unclear, we demonstrate that they are precisely the appropriate conditions to represent such monoids as internal monoids in an appropriate category of Ehrhard's finiteness spaces. Ehrhard introduced finiteness spaces as the objects of a categorical model of classical linear logic, where a set is equipped with a class of subsets to be thought of as finitary. Morphisms are relations preserving the finitary structure. The notion of finitary subset allows for a sharper analysis of computational structure than is available in the relational model. For example, fixed point operators fail to be finitary. In the present work, we take morphisms to be partial functions preserving the finitary structure rather than relations. The resulting category is symmetric monoidal closed, complete and cocomplete. Any pair of an internal monoid in this category and a ring induces a ring of generalized power series by an extension of the Ribenboim construction based on Ehrhard's notion of linearization of a finiteness space. We thus further generalize Ribenboim's constructions. We give several examples of rings which arise from this construction, including the ring of Puiseux series and the ring of formal power series generated by a free monoid.