Finitary $\mathcal{M}$-Adhesive Categories

Finitary \(\mathcal{M}\)-adhesive categories are \(\mathcal{M}\)-adhesive categories with finite objects only, where the notion \(\mathcal{M}\)-adhesive category is short for weak adhesive high-level replacement (HLR) category. We call an object finite if it has a finite number of \(\mathcal{M}\)-subobjects. In this paper, we show that in finitary \(\mathcal{M}\)-adhesive categories we do not only have all the well-known properties of \(\mathcal{M}\)-adhesive categories, but also all the additional HLR-requirements which are needed to prove the classical results for \(\mathcal{M}\)-adhesive systems. These results are the Local Church-Rosser, Parallelism, Concurrency, Embedding, Extension, and Local Confluence Theorems, where the latter is based on critical pairs. More precisely, we are able to show that finitary \(\mathcal{M}\)-adhesive categories have a unique \(\mathcal{E}\)-\(\mathcal{M}\) factorization and initial pushouts, and the existence of an \(\mathcal{M}\)-initial object implies in addition finite coproducts and a unique \(\mathcal{E'}\)-\(\mathcal{M'}\) pair factorization. Moreover, we can show that the finitary restriction of each \(\mathcal{M}\)-adhesive category is a finitary \(\mathcal{M}\)-adhesive category and finitariness is preserved under functor and comma category constructions based on \(\mathcal{M}\)-adhesive categories. This means that all the classical results are also valid for corresponding finitary \(\mathcal{M}\)-adhesive systems like several kinds of finitary graph and Petri net transformation systems. Finally, we discuss how some of the results can be extended to non-\(\mathcal{M}\)-adhesive categories.