# Lovász-Type Theorems and Game Comonads

Anuj Dawar and Tomáš Jakl  Department of Computer Science and Technology
University of Cambridge, UK<EMAIL_ADDRESS><EMAIL_ADDRESS>and
Luca Reggio  Department of Computer Science
University of Oxford, UK<EMAIL_ADDRESS>
###### Abstract.

Lovász (1967) showed that two finite relational structures $A$ and $B$ are
isomorphic if, and only if, the number of homomorphisms from $C$ to $A$ is the
same as the number of homomorphisms from $C$ to $B$ for any finite structure
$C$. Soon after, Pultr (1973) proved a categorical generalisation of this
fact. We propose a new categorical formulation, which applies to any locally
finite category with pushouts and a proper factorisation system. As special
cases of this general theorem, we obtain two variants of Lovász’ theorem: the
result by Dvořák (2010) that characterises equivalence of graphs in the
$k$-dimensional Weisfeiler–Leman equivalence by homomorphism counts from
graphs of tree-width at most $k$, and the result of Grohe (2020)
characterising equivalence with respect to first-order logic with counting and
quantifier depth $k$ in terms of homomorphism counts from graphs of tree-depth
at most $k$. The connection of our categorical formulation with these results
is obtained by means of the game comonads of Abramsky et al. We also present a
novel application to homomorphism counts in modal logic.

###### Key words and phrases:

Game comonads, homomorphism counting, $k$-Weisfeiler-Leman equivalence, tree
depth, tree width, modal logic

Research supported in part by the EPSRC grant EP/T007257/1, and by the
European Union’s Horizon 2020 research and innovation programme under the
Marie Skłodowska-Curie grant agreement No 837724.
To appear in the Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in
Computer Science (LICS 2021)

##  1\. Introduction

Over fifty years ago, Lovász [20] proved that two finite graphs (or, more
generally, any two finite relational structures) $A$ and $B$ are isomorphic
if, and only if, for every finite graph $C$, the number of homomorphisms from
$C$ to $A$ is the same as the number of homomorphisms from $C$ to $B$. While
one direction of this equivalence is obvious, the other direction establishes
that the isomorphism type of a finite graph $A$ is characterised by an
infinite integer vector $V$ indexed by $\mathcal{F}$, the collection of
(isomorphism classes of) finite graphs, where for $C\in\mathcal{F}$, $V_{C}$
is the number of homomorphisms from $C$ to $A$. This seminal result has led to
extensions and investigations in many different directions. One that concerns
us is that by restricting the collection $\mathcal{F}$ to a natural sub-
collection, we can often obtain characterisations of natural coarsenings of
the relation of isomorphism. For any subclass $\mathcal{F}^{\prime}$ of
$\mathcal{F}$, say that a pair of graphs $G$ and $H$ is
$\mathcal{F}^{\prime}$-homomorphism equivalent if for any $K$ in
$\mathcal{F}^{\prime}$ the number of homomorphisms from $K$ to $G$ is the same
as the number of homomorphisms from $K$ to $H$.

For instance, Dvořák [11] shows that for any $k$, if we consider the
collection $\mathcal{T}_{k}$ of all graphs of tree-width at most $k$, then a
pair of graphs are $\mathcal{T}_{k}$-homomorphism equivalent if, and only if,
they are equivalent with respect to the $k$-dimensional Weisfeiler–Leman
($k$-WL) equivalence. The $k$-WL equivalence relations are a widely studied
family of approximations of the graph isomorphism relation (see [17] for a
recent exposition) with many equivalent characterisations in terms of
combinatorics, logic, algebra and linear optimisation. From our point of view,
one important such characterisation is the fact that two graphs $G$ and $H$
are $k$-WL equivalent if, and only if, they are not distinguished by any
sentence of $\mathcal{C}^{k+1}$—first-order logic with counting quantifiers
restricted to no more than $k+1$ distinct variables [9]. This logical
formulation of the equivalence extends naturally to finite structures over any
relational vocabulary.

Dvořák’s result offers yet another characterisation of $k$-WL equivalence,
this time in terms of homomorphism counts from the equally widely studied
class of graphs $\mathcal{T}_{k}$. An important special case is that of $k=1$.
Since $\mathcal{T}_{1}$ is the class of finite forests, and $1$-WL equivalence
is the same as _fractional isomorphism_ (see [27]), the result also provides
an elegant characterisation of equivalence of graphs with respect to the
number of homomorphisms from trees. It is also known that two graphs are co-
spectral if, and only if, they are $\mathrm{Cyc}$-homomorphism equivalent,
where $\mathrm{Cyc}$ is the class of simple cycles, and that two graphs are
_quantum isomorphic_ if, and only if, they are $\mathcal{P}$-homomorphism
equivalent for the class $\mathcal{P}$ of planar graphs [23]. Another recent
addition to this collection of results is that of Grohe [14]. He shows that,
if $\mathcal{D}_{n}$ is the collection of graphs of _tree-depth_ at most $n$,
then two graphs are $\mathcal{D}_{n}$-homomorphism equivalent if, and only if,
they are not distinguished by any sentence of $\mathcal{C}_{n}$—first-order
logic with counting with quantifier depth at most $n$.

This variety of results relating homomorphism counts over restricted classes
to approximations of isomorphism, often proved with very different methods,
calls for the development of a more general theory. In the present paper we
develop a general categorical result which yields, as example applications,
the results of Lovász, Dvořák and Grohe mentioned above. The connection
between our categorical result and the results of Dvořák and Grohe is
established using the game comonads of Abramsky et al. [1, 3]. Specifically,
in [1] the graded pebbling comonad $\mathbb{P}_{k}$ on the category of
$\sigma$-structures (for a finite relational signature $\sigma$) is introduced
and it is shown that the coalgebras for this comonad correspond in a natural
way with certain tree decompositions of width at most $k-1$. In particular, a
finite $\sigma$-structure admits a coalgebra structure for this comonad if,
and only if, it has tree-width at most $k-1$. At the same time, it is shown
that isomorphism in the Kleisli category corresponding to the comonad (or
equivalently in the Eilenberg–Moore category) is exactly indistinguishability
in $\mathcal{C}^{k}$. This brings together in one categorical construction the
essential elements of Dvořák’s theorem. In an exactly analogous fashion, the
Ehrenfeucht–Fraïssé comonad $\mathbb{E}_{n}$ of [3] captures, at the level of
coalgebras, the structures of tree-depth at most $n$ and yields a notion of
isomorphism corresponding to equivalence in $\mathcal{C}_{n}$. These
categorical formulations of the combinatorial parameters tree-width and tree-
depth on the one hand, and the logical equivalences with respect to
$\mathcal{C}^{k}$ and $\mathcal{C}_{n}$ on the other, are what enable us to
give a single result generalising the three theorems of Lovász, Dvořák and
Grohe.

Our general result states that in any locally finite category with pushouts
and a proper factorisation system, two objects $m$ and $n$ are isomorphic if,
and only if, the number of morphisms from $k$ to $m$ is the same as that from
$k$ to $n$ for any object $k$. This is proved in Section 3. In Section 4, we
use the game comonads to derive the theorems of Dvořák and Grohe from this
general result and also a combination of the two characterising equivalence in
$\mathcal{C}^{k}_{n}$—first-order logic with counting with quantifier depth
$n$ and $k$ variables. In Section 5, we apply the machinery we have developed
to another game comonad: the graded modal comonad $\mathbb{M}_{k}$. This gives
a new Lovász-style result for pointed Kripke structures, relating homomorphism
counts from synchronization trees of bounded height to equivalence in a modal
logic with counting. Finally, in Section 6 we draw some conclusions from this
about certain normal forms for first-order logic with counting.

### Related work

Other categorical generalisations of Lovász’ theorem have been obtained by
Pultr [26] and Isbell [15]. Cf. also Lovász’ paper [21]. In modern terms,
Pultr works with a finitely well-powered, locally finite category with
(extremal epi, mono) factorisations and Isbell requires the category to be
locally finite with a special type of factorisation system (which he calls
“bicategory”). Unlike the results in op. cit., our Theorem 5 does not hinge on
a combinatorial counting argument, but rather on an application of the
inclusion-exclusion principle, and appears to be better suited for
applications to game comonads.

##  2\. Preliminaries on Game Comonads

In this section, we recall the necessary material on (game) comonads and their
coalgebras.

###  2.1. Categories

We briefly recall some basic notions of category theory. For a more thorough
introduction, see e.g. [5] or [22].

Let $\mathcal{A}$ be a category, and $f\colon A\to B$ and $g\colon A\to C$ two
arrows in $\mathcal{A}$. The _pushout_ of $f$ and $g$, if it exists, consists
of two arrows $h\colon C\to D$ and $i\colon B\to D$ such that $i\circ f=h\circ
g$ and the following universal property is satisfied: For any two arrows
$i^{\prime}\colon B\to E$ and $h^{\prime}\colon C\to E$ with $i^{\prime}\circ
f=h^{\prime}\circ g$, there is a unique arrow $\xi\colon D\to E$ satisfying
$\xi\circ i=i^{\prime}$ and $\xi\circ h=h^{\prime}$.

${A}$${B}$${C}$${D}$${E}$$\scriptstyle{f}$$\scriptstyle{g}$$\scriptstyle{i}$$\scriptstyle{i^{\prime}}$$\scriptstyle{h}$$\scriptstyle{h^{\prime}}$$\scriptstyle{\xi}$

The _pullback_ of two arrows $f\colon A\to C$ and $g\colon B\to C$ in
$\mathcal{A}$, if it exists, is the pushout of $f$ and $g$ in the opposite
category $\mathcal{A}^{\mathrm{op}}$ obtained by reversing the direction of
the arrows in $\mathcal{A}$.

Pushouts and pullbacks are special instances of the concepts of colimits and
limits of diagrams, respectively. For example, the pushout of $f\colon A\to B$
and $g\colon A\to C$ coincides with the colimit of the diagram

${B}$${A}$${C.}$$\scriptstyle{f}$$\scriptstyle{g}$

For arbitrary colimits, we consider diagrams of any shape.

A functor $F\colon\mathcal{A}\to\mathcal{B}$ is _faithful_ if, given any two
parallel arrows $f,g\colon A\to A^{\prime}$ in $\mathcal{A}$, $Ff=Fg$ implies
$f=g$. Further, $F$ is _full_ if, for any two objects $A$ and $A^{\prime}$ of
$\mathcal{A}$, each arrow $FA\to FA^{\prime}$ is of the form $Ff$ for some
$f\colon A\to A^{\prime}$. A subcategory $\mathcal{A}$ of a category
$\mathcal{B}$ is said to be _full_ if the inclusion functor
$\mathcal{A}\to\mathcal{B}$ is full.

A fundamental notion of category theory is that of an adjunction. Let
$F\colon\mathcal{A}\to\mathcal{B}$ and $G\colon\mathcal{B}\to\mathcal{A}$ be
any two functors between categories. We say that $F$ is _left adjoint_ to $G$
(equivalently, $G$ is _right adjoint_ to $F$), and write $F\dashv G$, provided
that for each object $B\in\mathcal{B}$ there is a morphism
$\varepsilon_{B}\colon FGB\to B$ satisfying the following universal property:
For every $A\in\mathcal{A}$ and morphism $f\colon FA\to B$ in $\mathcal{B}$,
there exists a unique morphism $g\colon A\to GB$ in $\mathcal{A}$ such that
$\varepsilon_{B}\circ Fg=f$.

${FGB}$${B}$${FA}$$\scriptstyle{\varepsilon_{B}}$$\scriptstyle{f}$$\scriptstyle{Fg}$

###  2.2. Comonads

A _comonad_ (_in Kleisli form_) on a category $\mathcal{A}$ is given by:

  * •

an object map $\mathbb{C}\colon\mathcal{A}\to\mathcal{A}$;

  * •

a morphism $\varepsilon_{A}\colon\mathbb{C}(A)\to A$ for every
$A\in\mathcal{A}$;

  * •

a _coextension operation_ associating with any morphism
$f\colon\mathbb{C}(A)\to B$ a morphism
$f^{*}\colon\mathbb{C}(A)\to\mathbb{C}(B)$.

These data must satisfy the following equations for all morphisms
$f\colon\mathbb{C}(A)\to B$ and $g\colon\mathbb{C}(B)\to C$:

$\varepsilon_{A}^{*}={\rm id}_{\mathbb{C}(A)},\ \ \varepsilon_{B}\circ
f^{*}=f,\ \ (g\circ f^{*})^{*}=g^{*}\circ f^{*}.$

In particular, we can extend $\mathbb{C}$ to a functor
$\mathcal{A}\to\mathcal{A}$ by setting
$\mathbb{C}(f)\coloneqq(f\circ\varepsilon_{A})^{*}$ for every morphism
$f\colon A\to B$.111It is easy to see that, setting $\delta_{A}\coloneqq{\rm
id}_{\mathbb{C}(A)}^{*}$ for every $A\in\mathcal{A}$, the tuple
$(\mathbb{C},\varepsilon,\delta)$ is a comonad in the more traditional sense,
where $\varepsilon$ is the counit and $\delta$ the comultiplication. In fact,
these two formulations are equivalent.

We recall next some examples of comonads that play an important role in this
paper. Let $\sigma$ be an arbitrary relational signature. The category
$\Sigma$ has as objects $\sigma$-structures (denoted $A,B,\dots$) and as
morphisms _$\sigma$ -homomorphisms_ (sometimes simply called _homomorphisms_),
i.e. functions $f\colon A\to B$ such that, for all relation symbols
${R\in\sigma}$, $f(R^{A})\subseteq R^{B}$ where $R^{A}$ and $R^{B}$ are the
interpretations of $R$ in $A$ and $B$, respectively.

For each positive integer $n$, the _Ehrenfeucht–Fraïssé_ comonad
$\mathbb{E}_{n}$ on $\Sigma$ (cf. [3]) is defined as follows. For any
$A\in\Sigma$, the universe of $\mathbb{E}_{n}(A)$ is the set $A^{\leq n}$ of
all non-empty sequences of length at most $n$. Before defining the
interpretations of the relation symbols, let us define the map

$\varepsilon_{A}\colon A^{\leq n}\to A,\ \
\varepsilon_{A}[a_{1},\ldots,a_{l}]\coloneqq a_{l}.$

With this notation, for each $R\in\sigma$ of arity $j$, we define
$R^{\mathbb{E}_{n}(A)}$ to be the set of those tuples $(s_{1},\ldots,s_{j})$
of sequences which are pairwise comparable in the prefix order, and such that
$(\varepsilon_{A}(s_{1}),\dots,\varepsilon_{A}(s_{j}))\in R^{A}$. The
coextension operation sends a $\sigma$-homomorphism
$f\colon\mathbb{E}_{n}(A)\to B$ to the $\sigma$-homomorphism

$f^{*}\colon\mathbb{E}_{n}(A)\to\mathbb{E}_{n}(B),\ \
f^{*}[a_{1},\dots,a_{j}]\coloneqq[b_{1},\dots,b_{j}]$

where $b_{i}\coloneqq f[a_{1},\dots,a_{i}]$ for all $1\leq i\leq j$. It is not
difficult to see that these data define a comonad on the category $\Sigma$.

From the viewpoint of model-comparison games, the elements of $A^{\leq n}$
represent the plays in the $\sigma$-structure $A$ of length at most $n$, and a
$\sigma$-homomorphism $\mathbb{E}_{n}(A)\to B$ is a strategy for Duplicator in
the Ehrenfeucht–Fraïssé game with $n$ rounds, where Spoiler plays always in
$A$ and Duplicator responds in $B$. For more details, cf. [3, 4]. Next we
recall from [1] another comonad on $\Sigma$, which models pebble games.

For each positive integer $k$, set $\mathbf{k}\coloneqq\\{1,\dots,k\\}$. Given
a $\sigma$-structure $A$, we consider the set $(\mathbf{k}\times A)^{+}$ of
all non-empty sequences of elements of $\mathbf{k}\times A$. We call a pair
$(p,a)\in{\mathbf{k}\times A}$ a _move_. Whenever
$[(p_{1},a_{1}),\dots,(p_{l},a_{l})]$ is a sequence of moves, $p_{i}$ is
called the _pebble index_ of the move $(p_{i},a_{i})$. As with
$\mathbb{E}_{n}$, define the map

$\varepsilon_{A}\colon(\mathbf{k}\times A)^{+}\to A,\ \
\varepsilon_{A}[(p_{1},a_{1}),\dots,(p_{l},a_{l})]\coloneqq a_{l}$

sending a play to its last move. We let $\mathbb{P}_{k}(A)$ be the
$\sigma$-structure with universe $(\mathbf{k}\times A)^{+}$ and such that, for
every relation $R\in\sigma$ of arity $j$, its interpretation
$R^{\mathbb{P}_{k}(A)}$ consists of those tuples of sequences
$(s_{1},\ldots,s_{j})$ such that: (i) the $s_{i}$ are pairwise comparable in
the prefix order; (ii) whenever $s_{i}$ is a prefix of $s_{i^{\prime}}$, the
pebble index of the last move in $s_{i}$ does not appear in the suffix of
$s_{i}$ in $s_{i^{\prime}}$; and (iii)
${(\varepsilon_{A}(s_{1}),\dots,\varepsilon_{A}(s_{j}))\in R^{A}}$. Finally,
the coextension operation is the same, mutatis mutandis, as with
$\mathbb{E}_{n}$. Again, it is not difficult to see that these data define a
comonad $\mathbb{P}_{k}$ on $\Sigma$, called the _pebbling comonad_.

The Ehrenfeucht–Fraïssé comonad $\mathbb{E}_{n}$ can be “combined” with the
pebbling comonad $\mathbb{P}_{k}$ to obtain a new comonad $\mathbb{P}_{k,n}$
on $\Sigma$, cf. [25]. For every $A\in\Sigma$, the universe of
$\mathbb{P}_{k,n}(A)$ is the set $(\mathbf{k}\times A)^{\leq n}$ of all non-
empty sequences of length at most $n$ (this corresponds to bounding the length
of plays in pebble games). The homomorphisms $\varepsilon_{A}$ and the
coextension operation for $\mathbb{P}_{k,n}$ are defined as the restrictions
of the corresponding concepts for the pebbling comonad $\mathbb{P}_{k}$.

###  2.3. Coalgebras

Let $\mathbb{C}$ be a comonad (in Kleisli form) on a category $\mathcal{A}$. A
_coalgebra_ for $\mathbb{C}$ is a pair
$(A,A\xrightarrow{\alpha}\mathbb{C}(A))$ such that $A\in\mathcal{A}$, $\alpha$
is a morphism in $\mathcal{A}$, and the following diagrams commute:

${A}$${\mathbb{C}(A)}$${A}$$\scriptstyle{{\rm
id}_{A}}$$\scriptstyle{\alpha}$$\scriptstyle{\varepsilon_{A}}$${A}$${\mathbb{C}(A)}$${\mathbb{C}(A)}$${\mathbb{C}(\mathbb{C}(A))}$$\scriptstyle{\alpha}$$\scriptstyle{\alpha}$$\scriptstyle{{\rm
id}_{\mathbb{C}(A)}^{*}}$$\scriptstyle{\mathbb{C}(\alpha)}$

We refer to $\alpha$ as a _coalgebra structure_ for $A$. In the case of the
game comonads $\mathbb{E}_{n},\mathbb{P}_{k}$, and $\mathbb{P}_{k,n}$, the
$\sigma$-structures admitting a coalgebra structure can be characterised in an
elegant way in terms of key combinatorial parameters, as we now explain.

Let $(F,\leq)$ be any poset. For all $x,y\in F$, we write $x{\,\uparrow\,}y$
whenever $x$ and $y$ are comparable, i.e. either $x\leq y$ or $y\leq x$, and
let ${\downarrow\,}x\coloneqq\\{y\in F\mid y\leq x\\}$. A _forest_ is a poset
$(F,\leq)$ such that, for all $x\in F$, the set ${\downarrow\,}x$ is finite
and totally ordered. The _height_ of $(F,\leq)$ is $\sup_{x\in
F}{|{\downarrow\,}x|}$.

If $G=(V,\frown)$ is a graph (where $V$ is the set of vertices and $\frown$
the adjacency relation), a _forest cover_ of $G$ consists of a forest
$(F,\leq)$ and an injective function $f\colon V\to F$ such that
$v{\,\frown\,}v^{\prime}$ entails $f(v){\,\uparrow\,}f(v^{\prime})$ for all
$v,v^{\prime}\in V$.

Finally, recall that the _Gaifman graph_ of a $\sigma$-structure $A$ is
$\mathcal{G}_{A}\coloneqq(A,\frown)$ where $a{\,\frown\,}a^{\prime}$ if $a\neq
a^{\prime}$ and there exist $R\in\sigma$ and a tuple $(a_{1},\dots,a_{l})\in
R^{A}$ such that $a=a_{i}$ and $a^{\prime}=a_{j}$ for some
$i,j\in\\{1,\dots,l\\}$. A $\sigma$-structure $A$ has _tree-depth at most $n$_
if there is a forest cover $(F,\leq)$ of $\mathcal{G}_{A}$ of height
${\leq\,}n$.

The following is a direct consequence of [3, Theorem 17]:

######  Proposition 1.

A $\sigma$-structure $A$ admits a coalgebra structure $\alpha\colon
A\to\mathbb{E}_{n}(A)$ if, and only if, it has tree-depth at most $n$.

In the same way as $\sigma$-structures that admit a coalgebra structure for
$\mathbb{E}_{n}$ can be characterised in terms of tree-depth, the existence of
a coalgebra structure for the pebbling comonad $\mathbb{P}_{k}$ corresponds to
tree-width. We recall the relevant definitions.

Note that, if $(F,\leq)$ is a forest cover of a graph $G=(V,\frown)$, with
injective map $f\colon V\to F$, we can assume without loss of generality that
$F=V$ and $f={\rm id}_{V}$. We shall assume this for the remainder of this
section. A _k-pebble forest cover_ of a graph $G=(V,\frown)$ consists of a
forest cover $(V,\leq)$ of $G$ and a pebbling function $p\colon
V\to\mathbf{k}$ such that, whenever $v{\,\frown\,}v^{\prime}$ with $v\leq
v^{\prime}$, we have $p(v)\neq p(w)$ for all $v<w\leq v^{\prime}$.

A $\sigma$-structure $A$ has _tree-width at most $k-1$_ if its Gaifman graph
$\mathcal{G}_{A}$ admits a $k$-pebble forest cover.222It is customary in graph
theory to use $k-1$, instead of $k$, so that trees have tree-width $1$. The
following result is a consequence of [1, Proposition 22].

######  Proposition 2.

A $\sigma$-structure $A$ admits a coalgebra structure $\alpha\colon
A\to\mathbb{P}_{k}(A)$ if, and only if, it has tree-width at most $k-1$.

######  Remark 3.

The tree-width of a graph is usually defined in terms of tree decompositions.
The definition given above is an equivalent reformulation. For a proof of the
fact that a finite graph admits a tree decomposition of width ${<\,}k$ if, and
only if, it admits a $k$-pebble forest cover, see [3, Theorem 19].

In the same spirit, in the case of the comonad $\mathbb{P}_{k,n}$ we have the
following characterisation, cf. [25, Theorem 2.14].

######  Proposition 4.

A $\sigma$-structure $A$ admits a coalgebra structure $\alpha\colon
A\to\mathbb{P}_{k,n}(A)$ if, and only if, it has a $k$-pebble forest cover of
height ${\leq\,}n$.

Finally, recall that coalgebras for a comonad $\mathbb{C}$ on $\mathcal{A}$
form themselves a category $\mathrm{EM}(\mathbb{C})$, the _Eilenberg–Moore
category_ of $\mathbb{C}$. The objects of $\mathrm{EM}(\mathbb{C})$ are the
coalgebras $(A,\alpha)$ for $\mathbb{C}$, and morphisms
$(A,\alpha)\to(B,\beta)$ in $\mathrm{EM}(\mathbb{C})$ are morphisms $h\colon
A\to B$ in $\mathcal{A}$ such that $\mathbb{C}(h)\circ\alpha=\beta\circ h$.
There is an obvious forgetful functor

$U^{\mathbb{C}}\colon\mathrm{EM}(\mathbb{C})\to\mathcal{A}$

which sends a coalgebra $(A,\alpha)$ to $A$. This functor has a right adjoint

$F^{\mathbb{C}}\colon\mathcal{A}\to\mathrm{EM}(\mathbb{C})$

defined as follows: for any $A\in\mathcal{A}$,
$F^{\mathbb{C}}(A)\coloneqq(\mathbb{C}(A),\delta_{A})$ where
$\delta_{A}\coloneqq{\rm id}_{\mathbb{C}(A)}^{*}$. Further, if $h$ is a
morphism in $\mathcal{A}$, we set $F^{\mathbb{C}}(h)\coloneqq\mathbb{C}(h)$.

${\mathrm{EM}(\mathbb{C})}$$\top$${\mathcal{A}}$$\scriptstyle{U^{\mathbb{C}}}$$\scriptstyle{F^{\mathbb{C}}}$

##  3\. A Categorical Lovász-Type Theorem

A category is _locally finite_ if there are only finitely many morphisms
between any two of its objects. A locally finite category $\mathcal{A}$ is
said to be _combinatorial_ if, for all $m,n\in\mathcal{A}$,

$m\cong n\ \Longleftrightarrow\
|\hom_{\mathcal{A}}(k,m)|=|\hom_{\mathcal{A}}(k,n)|\ \ \forall
k\in\mathcal{A}.$

Thus, Lovász’ theorem [20] states that, for any finite relational signature
$\sigma$, the category $\Sigma_{f}$ of finite $\sigma$-structures with
homomorphisms is combinatorial. The aim of this section is to prove the
following generalisation of Lovász’ result.

######  Theorem 5.

Let $\mathcal{A}$ be a locally finite category. If $\mathcal{A}$ has pushouts
and a proper factorisation system, then it is combinatorial.

###  3.1. Proper factorisation systems

We start by recalling the notion of weak factorisation system. Given morphisms
$e$ and $m$ in $\mathcal{A}$, we say that $e$ has the _left lifting property_
with respect to $m$, or that $m$ has the _right lifting property_ with respect
to $e$ if, for every commutative square as on the left-hand side below,

${{\bullet}}$${{\bullet}}$${{\bullet}}$${{\bullet}}$$\scriptstyle{e}$$\scriptstyle{m}$
${{\bullet}}$${{\bullet}}$${{\bullet}}$${{\bullet}}$$\scriptstyle{e}$$\scriptstyle{d}$$\scriptstyle{m}$

there is a (not necessarily unique) _diagonal filler_ , i.e. an arrow $d$ such
that the right-hand diagram above commutes. If this is the case, we write
$e{\,\pitchfork\,}m$. For any class $\mathcal{F}$ of morphisms in
$\mathcal{A}$, let ${}^{\pitchfork}\mathcal{F}$ (respectively
$\mathcal{F}^{\pitchfork}$) be the class of morphisms having the left
(respectively right) lifting property with respect to every morphism in
$\mathcal{F}$.

######  Definition 6.

A pair of classes of morphisms $(\mathcal{E},\mathcal{M})$ in a category
$\mathcal{A}$ is a _weak factorisation system_ provided it satisfies the
following conditions:

  1. (1)

every morphism $f$ in $\mathcal{A}$ can be written as $f=m\circ e$ with
$e\in\mathcal{E}$ and $m\in\mathcal{M}$;

  2. (2)

$\mathcal{E}={}^{\pitchfork}\mathcal{M}$ and
$\mathcal{M}=\mathcal{E}^{\pitchfork}$.

A _proper factorisation system_ is a weak factorisation system
$(\mathcal{E},\mathcal{M})$ such that all morphisms in $\mathcal{E}$ are
epimorphisms and all morphisms in $\mathcal{M}$ are monomorphisms.333It is an
easy observation that any proper factorisation system is an _orthogonal_
factorisation system, meaning that the diagonal fillers are unique.

We describe two different proper factorisation systems in the category
$\Sigma$ of $\sigma$-structures, for a fixed relational signature $\sigma$.
Each homomorphism of $\sigma$-structures $f\colon A\to B$ factors, as a
function, through its set-theoretic image $\widetilde{A}$:

$A\to\widetilde{A}\to B.$

There are two natural ways to turn $\widetilde{A}$ into a $\sigma$-structure:
we can equip it with the structure induced by either $B$, or $A$. In the first
case, for every $R\in\sigma$ of arity $n$, we set $R^{\widetilde{A}}\coloneqq
R^{B}\cap\widetilde{A}^{n}$ and, in the second, we set
$R^{\widetilde{A}}\coloneqq f(R^{A})\cap\widetilde{A}^{n}$.

These two ways of turning $\widetilde{A}$ into a $\sigma$-structure yield two
different weak factorisation systems $(\mathcal{E},\mathcal{M})$ in the
category $\Sigma$.444These are the (epi, regular mono) and (regular epi, mono)
factorisation systems, respectively. Cf. [6, pp. 200–201]. For example, the
first one yields the weak factorisation system where
$\mathcal{E}=\\{\text{surjective homomorphisms}\\}$ and
$\mathcal{M}=\\{\text{strong/induced embeddings}\\}$. Both factorisation
systems are proper. Moreover, since the image of a finite $\sigma$-structure
under a homomorphism is also finite, these factorisation systems restrict to
the locally finite category $\Sigma_{f}$ of finite $\sigma$-structures.

The category $\Sigma$ also has pushouts. Given two homomorphisms of
$\sigma$-structures $f\colon A\to B$ and $g\colon A\to C$, their pushout $D$
is computed as the quotient of the disjoint sum of $\sigma$-structures $B+C$
by the least equivalence relation $\sim$ such that $f(a)\sim g(a)$ for every
$a\in A$. Equivalently, $D$ is obtained by equipping $D^{\prime}$, the pushout
of the functions $f$ and $g$ in the category of sets, depicted in the
following diagram,

${A}$${B}$${C}$${D^{\prime}}$$\scriptstyle{f}$$\scriptstyle{g}$$\scriptstyle{f^{\prime}}$$\scriptstyle{g^{\prime}}$

with the smallest relational structure that turns $f^{\prime}$ and
$g^{\prime}$ into homomorphisms. Using the same idea, it is not difficult to
see that $\Sigma$ is cocomplete, i.e. it has all colimits, cf. [6, p. 201].

By the previous description of pushouts, it is clear that the pushout in
$\Sigma$ of finite $\sigma$-structures is again a finite $\sigma$-structure.
It follows that $\Sigma_{f}$ has all pushouts, and thus it satisfies the
assumptions of Theorem 5. This justifies our claim that the latter result is a
generalisation of Lovász’ theorem.

We state next some well known properties of weak and proper factorisation
systems (cf., e.g., [12] or [28]):

######  Lemma 7.

Let $(\mathcal{E},\mathcal{M})$ be a weak factorisation system in
$\mathcal{A}$. The following hold:

  1. (a)

$\mathcal{E}$ and $\mathcal{M}$ are closed under compositions;

  2. (b)

$\mathcal{E}\cap\mathcal{M}=\\{\text{isomorphisms}\\}$;

  3. (c)

the pushout in $\mathcal{A}$ of an $\mathcal{E}$-morphism along any morphism,
if it exists, is again in $\mathcal{E}$.

Moreover, if $(\mathcal{E},\mathcal{M})$ is proper, the following hold:

  1. (d)

$g\circ f\in\mathcal{E}$ implies $g\in\mathcal{E}$;

  2. (e)

$g\circ f\in\mathcal{M}$ implies $f\in\mathcal{M}$.

###  3.2. Proof of Theorem 5

For the remainder of this section, we fix a category $\mathcal{A}$ admitting a
proper factorisation system $(\mathcal{E},\mathcal{M})$.
$\mathcal{M}$-morphisms will be denoted by $\rightarrowtail$, and
$\mathcal{E}$-morphisms by $\twoheadrightarrow$.

An _$\mathcal{E}$ -pushout square_ in $\mathcal{A}$ is a pushout square
consisting entirely of $\mathcal{E}$-morphisms. We are interested in functors
$\mathcal{A}^{\mathrm{op}}\to\mathbf{FinSet}$, where $\mathbf{FinSet}$ is the
category of finite sets and functions between them, that turn
$\mathcal{E}$-pushout squares in $\mathcal{A}$ into pullbacks in
$\mathbf{FinSet}$. Recall that pullbacks in $\mathbf{FinSet}$ admit the
following explicit description: a commutative square in $\mathbf{FinSet}$ is a
pullback if, and only if,

$\leavevmode\hbox to57.64pt{\vbox
to46.41pt{\pgfpicture\makeatletter\hbox{\hskip 28.82079pt\lower-23.2526pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{\offinterlineskip{}{}{{{}}{{}}{{}}{{}}}{{{}}}{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-28.82079pt}{-23.15276pt}\pgfsys@invoke{
}\hbox{\vbox{\halign{\pgf@matrix@init@row\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding&&\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding\cr\hfil\hskip
8.05554pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.75pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${A}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
8.05554pt\hfil&\hfil\hskip 32.3489pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-4.0434pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${B}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
8.34894pt\hfil\cr\vskip 18.00005pt\cr\hfil\hskip
8.23679pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.93124pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${C}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
8.23679pt\hfil&\hfil\hskip 32.58398pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-4.27847pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${D}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
8.58401pt\hfil\cr}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}{{{{}}}{{}}{{}}{{}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} {}{ {}{}{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-12.32846pt}{11.50003pt}\pgfsys@lineto{11.28787pt}{11.50003pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{11.48785pt}{11.50003pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.4106pt}{15.2139pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{f}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-20.584pt}{5.14032pt}\pgfsys@lineto{-20.584pt}{-12.05977pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{-20.584pt}{-12.25975pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-26.52667pt}{-4.4861pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{g}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{20.23677pt}{5.14032pt}\pgfsys@lineto{20.23677pt}{-12.05977pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{20.23677pt}{-12.25975pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{22.58954pt}{-5.96803pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{i}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-12.14722pt}{-20.65276pt}\pgfsys@lineto{11.0528pt}{-20.65276pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{11.25278pt}{-20.65276pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.36378pt}{-18.29999pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{h}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\ \ \ \ \
\pbox{18em}{\forall b\in B,\forall c\in C,\ \text{if}\ i(b)=h(c)\
\text{then}\\\ \exists!a\in A.\ (f(a)=b\text{ and }g(a)=c).}$

If $h$ and $i$ are injective then, by identifying $B$ and $C$ with subsets of
$D$, the pullback $A$ can be identified with $B\cap C$.

The following lemma shows that the hom-functors involved in the homomorphism
counting theorem send pushout squares to pullbacks. (This is a consequence of
the more general fact that representable functors preserve all limits that
exist in their domain, cf. [22, pp. 116-117], but we provide here also a
direct elementary proof.) Recall that, for any object $n$ of a locally finite
category $\mathcal{B}$, the functor
$\hom_{\mathcal{B}}(-,n)\colon\mathcal{B}^{\mathrm{op}}\to\mathbf{FinSet}$
sends a morphism $f\colon a\to b$ in $\mathcal{B}$ to the function $-\circ
f\colon\hom_{\mathcal{B}}(b,n)\to\hom_{\mathcal{B}}(a,n)$.

######  Lemma 8.

For any locally finite category $\mathcal{B}$ and $n\in\mathcal{B}$, the
functor

$\hom_{\mathcal{B}}(-,n)\colon\mathcal{B}^{\mathrm{op}}\to\mathbf{FinSet}$

sends all pushout squares that exist in $\mathcal{B}$ to pullbacks in
$\mathbf{FinSet}$.

###### Proof.

Just observe that, given a pushout square in $\mathcal{B}$ and the
corresponding diagram in $\mathbf{FinSet}$, as displayed below,

${a}$${b}$${c}$${d}$$\scriptstyle{g}$$\scriptstyle{f}$$\scriptstyle{i}$$\scriptstyle{h}$${\hom_{\mathcal{B}}(d,n)}$${\hom_{\mathcal{B}}(b,n)}$${\hom_{\mathcal{B}}(c,n)}$${\hom_{\mathcal{B}}(a,n)}$$\scriptstyle{-\circ
i}$$\scriptstyle{-\circ h}$$\scriptstyle{-\circ f}$$\scriptstyle{-\circ g}$

if $\alpha\in\hom_{\mathcal{B}}(b,n)$ and $\beta\in\hom_{\mathcal{B}}(c,n)$
are such that $\alpha\circ f=\beta\circ g$ then, by the universal property of
the pushout, there is a unique $\gamma\in\hom_{\mathcal{B}}(d,n)$ satisfying
$\gamma\circ i=\alpha$ and $\gamma\circ h=\beta$. ∎

######  Lemma 9.

If a functor $F\colon\mathcal{A}^{\mathrm{op}}\to\mathbf{FinSet}$ sends
$\mathcal{E}$-pushout squares in $\mathcal{A}$ to pullbacks, then it sends
$\mathcal{E}$-morphisms to injections.

###### Proof.

Let $e\colon n\twoheadrightarrow m$ be an $\mathcal{E}$-morphism in the
category $\mathcal{A}$. Because $e$ is an epimorphism, it follows directly
that the square on the left-hand side below is a pushout square in
$\mathcal{A}$.

${n}$${m}$${m}$${m}$$\scriptstyle{e}$$\scriptstyle{e}$$\scriptstyle{{\rm
id}}$$\scriptstyle{{\rm
id}}$${F(m)}$${F(m)}$${F(m)}$${F(n)}$$\scriptstyle{{\rm
id}}$$\scriptstyle{{\rm id}}$$\scriptstyle{F(e)}$$\scriptstyle{F(e)}$

Since identities are $\mathcal{E}$-morphisms, the square on the right-hand
side above is a pullback in $\mathbf{FinSet}$. In turn, this is equivalent to
$F(e)$ being an injection. ∎

#### Generic and degenerate elements

The key step in the proof of the classical Lovász’ theorem consists in showing
that, if $|\hom_{\Sigma_{f}}(C,A)|=|\hom_{\Sigma_{f}}(C,B)|$ for all $C$ in
$\Sigma_{f}$, then also
$|\operatorname{inj}_{\Sigma_{f}}(C,A)|=|\operatorname{inj}_{\Sigma_{f}}(C,B)|$
for all $C$ in $\Sigma_{f}$, where $\operatorname{inj}_{\Sigma_{f}}(C,A)$ is
the set of all injective homomorphisms $C\hookrightarrow A$, and similarly for
$\operatorname{inj}_{\Sigma_{f}}(C,B)$. We aim to show the analogous fact in
our setting, where injective homomorphisms are replaced by
$\mathcal{M}$-morphisms.

The intuition behind the following definition is that a $\sigma$-homomorphism
$f\colon C\to A$ is non-injective precisely when there exist an onto non-
injective $\sigma$-homomorphism $e\colon C\twoheadrightarrow C^{\prime}$ and a
$\sigma$-homomorphism $g\colon C^{\prime}\to A$ such that $f=g\circ e$. In
terms of the hom-functor $E\coloneqq\hom_{\Sigma_{f}}(-,A)$, $f\in E(C)$ is
non-injective if, and only if, $f=E(e)(g)$ for some onto non-injective
$\sigma$-homomorphism $e\colon C\twoheadrightarrow C^{\prime}$ and $g\in
E(C^{\prime})$.

######  Definition 10.

A _strict quotient_ in $\mathcal{A}$ is an $\mathcal{E}$-morphism which is not
an isomorphism. (Equivalently, by Lemma 7(b), a strict quotient is an arrow in
$\mathcal{E}\setminus\mathcal{M}$.)

Further, consider a functor
$E\colon\mathcal{A}^{\mathrm{op}}\to\mathbf{FinSet}$. For every
$k\in\mathcal{A}$, we say that $s\in E(k)$ is _degenerate_ if there exist a
strict quotient $f\colon k\twoheadrightarrow l$ and $t\in E(l)$ such that
${E(f)(t)=s}$. Otherwise, $s$ is called _generic_. The subset of $E(k)$
consisting of the generic elements is denoted by ${E}\llbracket k\rrbracket$.

The next lemma shows that this definition matches our intuition for hom-
functors on $\mathcal{A}$.

######  Lemma 11.

Let $E=\hom_{\mathcal{A}}(-,n)$ for some $n\in\mathcal{A}$. For any
$k\in\mathcal{A}$, ${E}\llbracket k\rrbracket$ is the set of all
$\mathcal{M}$-morphisms $k\to n$.

###### Proof.

Let $f$ be an arbitrary element of $E(k)=\hom_{\mathcal{A}}(k,n)$. Assume $f$
is generic, and take its $(\mathcal{E},\mathcal{M})$ factorisation:

${k}$${l}$${n}$$\scriptstyle{f}$$\scriptstyle{g}$$\scriptstyle{h}$

Then $E(g)(h)=f$, and so $g$ must be an $\mathcal{M}$-morphism. By Lemma 7(a),
$f=h\circ g$ is also an $\mathcal{M}$-morphism.

Conversely, suppose $f$ is an $\mathcal{M}$-morphism and pick an
$\mathcal{E}$-morphism $g\colon k\twoheadrightarrow l$ and $h\in E(l)$ such
that $E(g)(h)=f$, i.e. $h\circ g=f$. By Lemma 7(e), $g$ is an
$\mathcal{M}$-morphism, so it is not a strict quotient. That is, $f$ is
generic. ∎

The following is the main technical lemma of this section, and it ultimately
relies on an application of the inclusion-exclusion principle.

######  Lemma 12.

Assume $\mathcal{A}$ has pushouts, and let $E$ and $F$ be functors
$\mathcal{A}^{\mathrm{op}}\to\mathbf{FinSet}$ sending $\mathcal{E}$-pushout
squares in $\mathcal{A}$ to pullbacks. If $E(k)\cong F(k)$ for all
$k\in\mathcal{A}$, then ${E}\llbracket k\rrbracket\cong{F}\llbracket
k\rrbracket$ for all $k\in\mathcal{A}$.

###### Proof.

Let $E,F$ be as in the statement, and suppose that $E(k)\cong F(k)$ for all
$k\in\mathcal{A}$. We must show that, for every $k\in\mathcal{A}$,
${E}\llbracket k\rrbracket\cong{F}\llbracket k\rrbracket$. Equivalently, we
show that the set ${E}\llparenthesis k\rrparenthesis$ of degenerate elements
of $E(k)$ is in bijection with the set ${F}\llparenthesis k\rrparenthesis$ of
degenerate elements of $F(k)$.

Observe that ${E}\llparenthesis k\rrparenthesis$ coincides with

$\bigcup{\\{\operatorname{Im}(E(f))\mid f\colon k\twoheadrightarrow l\
\text{is a strict quotient in $\mathcal{A}$}\\}}\subseteq E(k),$

and similarly for ${F}\llparenthesis k\rrparenthesis$. Since $E(k)$ and $F(k)$
are finite, there are finite sets $\mathcal{S}_{1},\mathcal{S}_{2}$ of strict
quotients of $k$ such that

$\displaystyle{E}\llparenthesis k\rrparenthesis$
$\displaystyle=\bigcup{\\{\operatorname{Im}(E(f))\mid
f\in\mathcal{S}_{1}\\}},$ $\displaystyle{F}\llparenthesis k\rrparenthesis$
$\displaystyle=\bigcup{\\{\operatorname{Im}(F(f))\mid
f\in\mathcal{S}_{2}\\}}.$

Let $\mathcal{S}\coloneqq\mathcal{S}_{1}\cup\mathcal{S}_{2}$. By the
inclusion-exclusion principle,

$|{E}\llparenthesis
k\rrparenthesis|=\sum_{J\subseteq\mathcal{S},J\neq\emptyset}(-1)^{|J|+1}\enspace\big{|}\\!\bigcap_{f\in
J}\operatorname{Im}(E(f))\big{|}$

and similarly for $|{F}\llparenthesis k\rrparenthesis|$. Therefore, to prove
${E}\llparenthesis k\rrparenthesis\cong{F}\llparenthesis k\rrparenthesis$ it
suffices to show that $\big{|}\\!\bigcap_{f\in
J}\operatorname{Im}(E(f))\big{|}=\big{|}\\!\bigcap_{f\in
J}\operatorname{Im}(F(f))\big{|}$ for any non-empty $J\subseteq\mathcal{S}$.
To this end, fix such a $J$ and consider the _wide pushout_ in $\mathcal{A}$
of the strict quotients in $J$, i.e. the diagram obtained by taking
consecutive pushouts of the elements of $J$, as shown in the diagram on the
left-hand side below.

${k}$${l_{u}}$${l_{3}}$${l_{2}}$${l_{1}}$${p}$${\mathinner{\mkern 1.0mu\raise
1.0pt\vbox{\kern 7.0pt\hbox{.}}\mkern 2.0mu\raise 4.0pt\hbox{.}\mkern
2.0mu\raise 7.0pt\hbox{.}\mkern
1.0mu}}$${E(k)}$${E(l_{u})}$${E(l_{3})}$${E(l_{2})}$${E(l_{1})}$${E(p)}$${\mathinner{\mkern
1.0mu\raise 1.0pt\vbox{\kern 7.0pt\hbox{.}}\mkern 2.0mu\raise
4.0pt\hbox{.}\mkern 2.0mu\raise 7.0pt\hbox{.}\mkern 1.0mu}}$

By Lemma 7(c), all arrows in this diagram are $\mathcal{E}$-morphisms. Hence,
by Lemma 9, the diagram obtained by applying the functor $E$, depicted on the
right-hand side above, consists of injections. Since $E$ sends
$\mathcal{E}$-pushouts to pullbacks, the diagram on the right is a wide
pullback of injections in $\mathbf{FinSet}$, and so $E(p)\cong\bigcap_{f\in
J}\operatorname{Im}(E(f))$. Similarly, $F(p)\cong\bigcap_{f\in
J}\operatorname{Im}(F(f))$. As $E(p)\cong F(p)$ by assumption, we get
$\big{|}\\!\bigcap_{f\in
J}\operatorname{Im}(E(f))\big{|}=\big{|}\\!\bigcap_{f\in
J}\operatorname{Im}(F(f))\big{|}$, thus concluding the proof. ∎

We are now in a position to prove the main result of this section:

###### Proof of Theorem 5.

Fix arbitrary objects $m,n\in\mathcal{A}$. For the non-trivial direction,
assume $|\hom_{\mathcal{A}}(k,m)|=|\hom_{\mathcal{A}}(k,n)|$ for all
$k\in\mathcal{A}$. Let $E$ and $F$ denote, respectively, the functors
$\hom_{\mathcal{A}}(-,m)\colon\mathcal{A}^{\mathrm{op}}\to\mathbf{FinSet}$ and
$\hom_{\mathcal{A}}(-,n)\colon\mathcal{A}^{\mathrm{op}}\to\mathbf{FinSet}$.
These functors send $\mathcal{E}$-pushout squares in $\mathcal{A}$ to
pullbacks by Lemma 8. Thus, by Lemma 12, ${E}\llbracket
k\rrbracket\cong{F}\llbracket k\rrbracket$ for all $k\in\mathcal{A}$.
According to Lemma 11, there is a bijection

$\\{\text{$\mathcal{M}$-morphisms}\ k\rightarrowtail
m\\}\enspace{\cong}\enspace\\{\text{$\mathcal{M}$-morphisms}\ k\rightarrowtail
n\\}.$

Setting $k=m$, the existence of an $\mathcal{M}$-morphism $m\rightarrowtail m$
(namely the identity) entails the existence of an $\mathcal{M}$-morphism
$i\colon m\rightarrowtail n$. Similarly, there exists an
$\mathcal{M}$-morphism $j\colon n\rightarrowtail m$. A standard argument then
shows that $m\cong n$ (see e.g. [26]). We briefly sketch a proof. The set $L$
of all $\mathcal{M}$-morphisms $m\rightarrowtail m$ is a monoid with respect
to composition and contains $j\circ i$. Since all $\mathcal{M}$-morphisms are
monos, $L$ satisfies the left cancellation law $ab=ac\Rightarrow b=c$. But
every finite monoid satisfying the left cancellation law is a group, hence
$j\circ i$ has an inverse. It follows from Lemma 7(b),(d) that $j$ is an
isomorphism. ∎

######  Remark 13.

Direct inspection of the preceding proofs shows that Theorem 5 can be slightly
strengthened by requiring only the existence of pushouts of
$\mathcal{E}$-morphisms along $\mathcal{E}$-morphisms.

###  3.3. Specialising to finite coalgebras

To conclude this section, we show that Theorem 5 can be used to lift Lovász’
homomorphism counting result from $\Sigma_{f}$ to categories of finite
coalgebras for comonads on $\Sigma$. This result is then applied in Sections
4–5 to obtain homomorphism counting results in finite model theory and modal
logic, respectively.

Given a comonad $\mathbb{C}$ on $\Sigma$, we say that a coalgebra $(A,\alpha)$
for $\mathbb{C}$ is _finite_ if $A$ is a finite $\sigma$-structure. The full
subcategory of $\mathrm{EM}(\mathbb{C})$ defined by the finite coalgebras is
denoted $\mathrm{EM}_{f}(\mathbb{C})$.

######  Corollary 14.

Let $\mathbb{C}$ be any comonad on $\Sigma$. Then
$\mathrm{EM}_{f}(\mathbb{C})$, the category of finite coalgebras for
$\mathbb{C}$, is combinatorial.

In order to prove the previous result, we need the following notions. Recall
that, for any category $\mathcal{A}$ and object $A\in\mathcal{A}$, two
epimorphisms $f\colon A\to B$ and $g\colon A\to C$ are _equivalent_ , written
$f\sim g$, if there exists an isomorphism $h\colon B\to C$ such that $h\circ
f=g$. It is not difficult to see that $\sim$ is an equivalence relation on the
collection of epimorphisms with domain $A$. The category $\mathcal{A}$ is said
to be _well-copowered_ if, for each $A\in\mathcal{A}$, the collection of all
$\sim$-equivalence classes of epimorphisms with domain $A$ is a set (as
opposed to a proper class). Any cocomplete category that is well-copowered
admits a proper factorisation system, see e.g. [8, Propositions 4.4.2, 4.4.3]
and [5, Proposition 14.7].

Moreover, recall that a functor $F\colon\mathcal{A}\to\mathcal{B}$ _creates
colimits_ if, for every diagram $\mathcal{D}$ in $\mathcal{A}$ such that
$F(\mathcal{D})$ admits a colimit $B$ in $\mathcal{B}$, there exists a colimit
$A$ of $\mathcal{D}$ in $\mathcal{A}$ with $F(A)\cong B$. In particular, if
$\mathcal{B}$ is cocomplete and $F$ creates colimits, then $\mathcal{A}$ is
also cocomplete and the functor $F$ preserves colimits. Further, $F$ _creates
isomorphisms_ if, whenever $h\colon B\to F(A)$ is an isomorphism in
$\mathcal{B}$, there exists an isomorphism $h^{\prime}\colon A^{\prime}\to A$
in $\mathcal{A}$ such that $F(h^{\prime})=h$. It is a well known fact that,
for any comonad $\mathbb{C}$ on $\mathcal{A}$, the forgetful functor
$U^{\mathbb{C}}\colon\mathrm{EM}(\mathbb{C})\to\mathcal{A}$ creates colimits
and isomorphisms (see e.g. [5, Proposition 20.12] for a proof of the dual
statement).

###### Proof of Corollary 14.

We show that the category $\mathrm{EM}_{f}(\mathbb{C})$ satisfies the
hypotheses of Theorem 5. The forgetful functor
$U^{\mathbb{C}}\colon\mathrm{EM}(\mathbb{C})\to\Sigma$ is faithful and
restricts to a functor $\mathrm{EM}_{f}(\mathbb{C})\to\Sigma_{f}$. Thus, for
all $(A,\alpha),(B,\beta)\in\mathrm{EM}_{f}(\mathbb{C})$, there is an
injection
$\hom_{\mathrm{EM}_{f}(\mathbb{C})}((A,\alpha),(B,\beta))\hookrightarrow\hom_{\Sigma_{f}}(A,B)$.
Because the latter set is finite, so is the former. Therefore,
$\mathrm{EM}_{f}(\mathbb{C})$ is locally finite.

We prove next that $\mathrm{EM}_{f}(\mathbb{C})$ has all pushouts. Because the
inclusion $\mathrm{EM}_{f}(\mathbb{C})\hookrightarrow\mathrm{EM}(\mathbb{C})$
is full and faithful, it suffices to prove that the pushout in
$\mathrm{EM}(\mathbb{C})$ of finite coalgebras exists and is a finite
coalgebra. Since $\Sigma$ is cocomplete (cf. the discussion following
Definition 6) and $U^{\mathbb{C}}\colon\mathrm{EM}(\mathbb{C})\to\Sigma$
creates colimits, the category $\mathrm{EM}(\mathbb{C})$ is cocomplete and the
forgetful functor $U^{\mathbb{C}}\colon\mathrm{EM}(\mathbb{C})\to\Sigma$
preserves all colimits. In particular, the pushout of finite coalgebras exists
in $\mathrm{EM}(\mathbb{C})$ and is a finite coalgebra.

The functor $U^{\mathbb{C}}\colon\mathrm{EM}(\mathbb{C})\to\Sigma$ preserves
colimits, and in particular epimorphisms. Using the fact that $U^{\mathbb{C}}$
is faithful and creates isomorphisms, it is not difficult to see that
$\mathrm{EM}(\mathbb{C})$ is well-copowered because so is $\Sigma$. Thus,
$\mathrm{EM}(\mathbb{C})$ admits a proper factorisation system
$(\mathcal{E},\mathcal{M})$. Now, consider a morphism $(A,\alpha)\to(B,\beta)$
in $\mathrm{EM}_{f}(\mathbb{C})$ and its
$(\mathcal{E},\mathcal{M})$-factorisation in $\mathrm{EM}(\mathbb{C})$:

${(A,\alpha)}$${(\widetilde{A},\widetilde{\alpha})}$${(B,\beta)}$$\scriptstyle{e}$$\scriptstyle{m}$

Since $U^{\mathbb{C}}$ preserves epimorphisms, $U(e)\colon A\to\widetilde{A}$
is an epimorphism in $\Sigma$, that is a surjective homomorphism. It follows
that $\widetilde{A}$ is a finite $\sigma$-structure and so
$(\widetilde{A},\widetilde{\alpha})\in\mathrm{EM}_{f}(\mathbb{C})$.

The fact that $\mathrm{EM}_{f}(\mathbb{C})$ admits a proper factorisation
system is then a consequence of the following easy observation: Let
$\mathcal{A}$ be any category equipped with a proper factorisation system
$(\mathcal{E},\mathcal{M})$, and $\mathcal{B}$ a full subcategory of
$\mathcal{A}$. Assume that, whenever $A\to B$ is a morphism in $\mathcal{B}$
and $A\to\widetilde{A}\to B$ is its $(\mathcal{E},\mathcal{M})$-factorisation
in $\mathcal{A}$, also $\widetilde{A}\in\mathcal{B}$. Then
$(\mathcal{E}\cap\mathcal{B},\mathcal{M}\cap\mathcal{B})$ is a proper
factorisation system in $\mathcal{B}$. ∎

######  Remark 15.

If $\mathbb{C}$ is a comonad on $\Sigma$ that restricts to a comonad
$\mathbb{C}^{\prime}$ on $\Sigma_{f}$, then $\mathrm{EM}(\mathbb{C}^{\prime})$
is isomorphic to $\mathrm{EM}_{f}(\mathbb{C})$ and thus
$\mathrm{EM}(\mathbb{C}^{\prime})$ is combinatorial by Corollary 14. Also,
note that the same proof as for Corollary 14 applies, mutatis mutandis, if
$\Sigma$ is replaced by the category of _pointed $\sigma$-structures_, having
as objects the pairs $(A,a)$ with $A\in\Sigma$ and $a\in A$, and as morphisms
the $\sigma$-homomorphisms preserving the distinguished points. This will be
needed in Section 5 for applications in the setting of modal logic.

More generally, it is not difficult to see that we may replace $\Sigma$ and
$\Sigma_{f}$ by any category $\mathcal{A}$, and full subcategory
$\mathcal{A}_{f}$ of $\mathcal{A}$, respectively, such that:

  1. (1)

$\mathcal{A}$ is cocomplete and well-copowered;

  2. (2)

$\mathcal{A}_{f}$ is locally finite, closed under finite colimits in
$\mathcal{A}$ and, if $A\to B$ is an epimorphism in $\mathcal{A}$ with
$A\in\mathcal{A}_{f}$, then $B\in\mathcal{A}_{f}$.

##  4\. Applications to Finite Model Theory

In this section, we apply Corollary 14 to the game comonads introduced in
Section 2 to give new proofs of results of Grohe and Dvořák connecting
homomorphism counts and indistinguishability in appropriate logic fragments.
We start by establishing a general result (Theorem 16) and then proceed to
show how Grohe’s and Dvořák’s theorems follow from it.

Before stating this general result, we illustrate the underlying idea for a
generic game comonad $\mathbb{C}$. In Section 2 we have recalled how game
comonads capture combinatorial parameters of $\sigma$-structures. On the other
hand, they can also express equivalence with respect to appropriate logic
fragments. For this, we need to extend the signature to account for equality
in the logic. Let $\sigma^{+}\coloneqq\sigma\cup\\{I\\}$ be the relational
signature obtained by adding a binary relation symbol $I$ to $\sigma$, and let
$\Sigma^{+}$ be the category of $\sigma^{+}$-structures with homomorphisms.
There is an _embedding_ , i.e. a full and faithful functor,

$J\colon\Sigma\to\Sigma^{+}$

which sends a $\sigma$-structure $A$ to the $\sigma^{+}$-structure $J(A)$
where $I$ is interpreted as the identity.

As the comonad $\mathbb{C}$ on $\Sigma$ is defined for arbitrary relational
signatures, we have a corresponding comonad $\mathbb{C}^{+}$ on $\Sigma^{+}$.
Typically, it turns out that, for an appropriate logic fragment $\mathcal{L}$,

$A\equiv_{\mathcal{L}}B\ \ \Longleftrightarrow\ \
F^{\mathbb{C}^{+}}(J(A))\cong F^{\mathbb{C}^{+}}(J(B))$

for all $A,B\in\Sigma_{f}$, where $U^{\mathbb{C}^{+}}\dashv
F^{\mathbb{C}^{+}}\colon\Sigma^{+}\to\mathrm{EM}(\mathbb{C}^{+})$ is the
adjunction associated with $\mathbb{C}^{+}$, cf. Section 2.3.

Provided that $\mathbb{C}^{+}$ sends finite structures to finite structures,
we can apply Corollary 14 to translate the isomorphism
$F^{\mathbb{C}^{+}}(J(A))\cong F^{\mathbb{C}^{+}}(J(B))$ into a statement
about homomorphism counts for $J(A)$ and $J(B)$ in $\Sigma_{f}^{+}$. It then
remains to go back to $\sigma$-structures to obtain a statement about
homomorphism counts for $A$ and $B$ in $\Sigma_{f}$. To this end, note that
the functor $J\colon\Sigma\to\Sigma^{+}$ has a left adjoint

$H\colon\Sigma^{+}\to\Sigma$

sending a $\sigma^{+}$-structure $D$ to $D^{-}/{\sim}$, where $D^{-}$ is the
$\sigma$-reduct of $D$ and $\sim$ is the equivalence relation generated by
$I^{D}$ (for a proof of this fact, see Lemma 25).

We now state the general result (whose proof is deferred to Section 4.3) from
which Grohe’s and Dvořák’s theorems will be derived in Sections 4.1 and 4.2,
respectively. Let us write $\mathrm{im}(U^{\mathbb{C}})$ for the full
subcategory of $\Sigma$ consisting of the objects of the form
$U^{\mathbb{C}}(A,\alpha)=A$ for $(A,\alpha)\in\mathrm{EM}(\mathbb{C})$, and
similarly for $\mathrm{im}(U^{\mathbb{C}^{+}})$.

######  Theorem 16.

Let $\mathbb{C}$ and $\mathbb{C}^{+}$ be comonads on $\Sigma$ and
$\Sigma^{+}$, respectively, and $\mathcal{L}$ a logic fragment. Suppose the
following conditions are satisfied:

  1. (1)

for all $A,B\in\Sigma_{f}$, $A\equiv_{\mathcal{L}}B$ if, and only if,
$F^{\mathbb{C}^{+}}(J(A))\cong F^{\mathbb{C}^{+}}(J(B))$;

  2. (2)

$\mathbb{C}^{+}$ sends finite $\sigma^{+}$-structures to finite
$\sigma^{+}$-structures;

  3. (3)

the embedding $J\colon\Sigma\to\Sigma^{+}$ and its left adjoint $H$ restrict
to $\Sigma_{f}\cap\mathrm{im}(U^{\mathbb{C}})$ and
$\Sigma_{f}^{+}\cap\mathrm{im}(U^{\mathbb{C}^{+}})$.

Then, for any finite $\sigma$-structures $A$ and $B$,

$A\equiv_{\mathcal{L}}B\ \text{ if, and only if, }\
|\hom_{\Sigma_{f}}(C,A)|=|\hom_{\Sigma_{f}}(C,B)|$

for every finite $\sigma$-structure $C$ in $\mathrm{im}(U^{\mathbb{C}})$.

######  Remark 17.

The proofs of Grohe’s and Dvořák’s theorems essentially reduce to showing that
the assumptions of Theorem 16 are satisfied for the appropriate comonads. The
“combinatorial core” of these results, which requires a specific argument for
each comonad, corresponds to verifying that the functor $H$ restricts to
$\Sigma_{f}^{+}\cap\mathrm{im}(U^{\mathbb{C}^{+}})\to\Sigma_{f}\cap\mathrm{im}(U^{\mathbb{C}})$.
This amounts to saying that the operation $D\mapsto D^{-}/{\sim}$ does not
increase the tree-depth or tree-width of $D$, and can be understood as an
equality elimination result (cf. Section 6).

###  4.1. Bounded tree-depth

Let $\mathcal{C}$ be the extension of first-order logic obtained by adding,
for each natural number $i$, a counting quantifier $\exists_{{\geq}i}$. The
semantics of these quantifiers is the following: for any structure $A$, we
have $A\models\exists_{{\geq}i}x.\,\varphi$ if, and only if,
$A\models\varphi[a/x]$ holds for at least $i$ distinct elements $a\in A$. Let
$\mathcal{C}_{n}$ be the fragment of $\mathcal{C}$ consisting of formulas of
quantifier depth ${\leq\,}n$.

The aim of this section is to use Theorem 16 to give a new proof of a recent
result of Grohe [14]:555Grohe proved this result for undirected vertex-
coloured graphs, but pointed out that his proof can be extended to arbitrary
$\sigma$-structures.

######  Theorem 18.

For any $A,B$ finite $\sigma$-structures,

$A\equiv_{\mathcal{C}_{n}}B\quad\text{if, and only
if,}\quad|\hom_{\Sigma_{f}}(C,A)|=|\hom_{\Sigma_{f}}(C,B)|$

for every finite $\sigma$-structure $C$ with tree-depth at most $n$.

Let $\mathbb{E}_{n}^{+}$ be the Ehrenfeucht–Fraïssé comonad on $\Sigma^{+}$,
and $U^{\mathbb{E}_{n}^{+}}\dashv
F^{\mathbb{E}_{n}^{+}}\colon\Sigma^{+}\to\mathrm{EM}(\mathbb{E}_{n}^{+})$ the
associated adjunction (cf. Section 2.3). By Proposition 1, a
$\sigma$-structure has tree-depth at most $n$ precisely when it belongs to
$\mathrm{im}(U^{\mathbb{E}_{n}})$. Thus, to prove Theorem 18, it suffices to
show that the assumptions of Theorem 16 are satisfied for
$\mathbb{C}=\mathbb{E}_{n}$, $\mathbb{C}^{+}=\mathbb{E}_{n}^{+}$, and
$\mathcal{L}=\mathcal{C}_{n}$.

Item 1 in Theorem 16 is a consequence of [3, Theorem 12]:

######  Proposition 19.

For any two $\sigma$-structures $A,B$, we have $A\equiv_{\mathcal{C}_{n}}B$
if, and only if, $F^{\mathbb{E}_{n}^{+}}(J(A))\cong
F^{\mathbb{E}_{n}^{+}}(J(B))$.

Item 2 holds because the comonad $\mathbb{E}_{n}^{+}$ restricts to finite
$\sigma^{+}$-structures, and item 3 is a consequence of the following
proposition—which concludes the proof of Grohe’s theorem.

######  Proposition 20.

The embedding $J\colon\Sigma\to\Sigma^{+}$ and its left adjoint $H$ restrict
to the full subcategories consisting of finite structures with tree-depth at
most $n$.

###### Proof.

Clearly, if $A$ is a (finite) $\sigma$-structure with tree-depth at most $n$,
then $J(A)$ has tree-depth at most $n$. It remains to prove that, for any
$D\in\Sigma_{f}^{+}$, if $D$ has tree-depth at most $n$ then so does $H(D)$.
To improve readability, set $C\coloneqq H(D)$.

Suppose $(F,\leq)$ is a forest of height ${\leq\,}n$ and $f\colon D\to F$ an
injective map such that $f(d_{1}){\,\uparrow\,}f(d_{2})$ whenever
$d_{1}{\,\frown\,}d_{2}$ in the Gaifman graph $\mathcal{G}_{D}$. Recall from
the definition of $H$ that, at the level of sets, $C=D/{\sim}$ where $\sim$ is
the equivalence relation generated by $I^{D}$. If $d\in D$, let $[d]$ denote
its $\sim$-equivalence class. For each $d\in D$, set

$\xi(d)\coloneqq\min{\\{f(d^{\prime})\mid d^{\prime}\in[d]\\}}.$

This minimum exists because $\\{f(d^{\prime})\mid d^{\prime}\in[d]\\}$ is a
connected subset of $F$. (Alternatively, note that $\xi(d)$ coincides with the
minimum of $\\{f(d^{\prime})\mid d^{\prime}\in[d]\\}\cap{\downarrow\,}f(d)$,
which is a finite non-empty totally ordered set.) Define

$g\colon C\to F,\ \ g([d])\coloneqq\xi(d).$

Clearly, $g$ is well-defined and it is injective because so is $f$. It remains
to prove that, for all $d_{1},d_{2}\in D$, $[d_{1}]{\,\frown\,}[d_{2}]$ in
$\mathcal{G}_{C}$ entails $g([d_{1}]){\,\uparrow\,}g([d_{2}])$, for then it
follows that $(F,\leq)$, along with the map $g$, is a forest cover of
$\mathcal{G}_{C}$.

If $[d_{1}]{\,\frown\,}[d_{2}]$, there are $d^{\prime}_{1}\in[d_{1}]$ and
$d^{\prime}_{2}\in[d_{2}]$ satisfying
$d^{\prime}_{1}{\,\frown\,}d^{\prime}_{2}$, and so
$f(d^{\prime}_{1}){\,\uparrow\,}f(d^{\prime}_{2})$. Assume
$f(d^{\prime}_{1})\leq f(d^{\prime}_{2})$. Since $g([d_{1}])\leq
f(d^{\prime}_{1})$ and $g([d_{2}])\leq f(d^{\prime}_{2})$, it follows that
both $g([d_{1}])$ and $g([d_{2}])$ belong to
${\downarrow\,}f(d^{\prime}_{2})$, which is totally ordered. Therefore,
$g([d_{1}]){\,\uparrow\,}g([d_{2}])$. Reasoning in a similar manner, we see
that $f(d^{\prime}_{2})\leq f(d^{\prime}_{1})$ implies
$g([d_{1}]){\,\uparrow\,}g([d_{2}])$. ∎

###  4.2. Bounded tree-width

Let $\mathcal{C}^{k}$ be the $k$-variable fragment of $\mathcal{C}$—first-
order logic with counting quantifiers. In this section, we show how to derive
from Theorem 16 the following variant of Dvořák’s theorem [11]:666Dvořák’s
result is for undirected graphs without loops. For a discussion of how his
result can be recovered in our framework, see Remark 24.

######  Theorem 21.

For any $A,B$ finite $\sigma$-structures,

$A\equiv_{\mathcal{C}^{k}}B\quad\text{if, and only
if,}\quad|\hom_{\Sigma_{f}}(C,A)|=|\hom_{\Sigma_{f}}(C,B)|$

for every finite $\sigma$-structure $C$ with tree-width at most $k-1$.

The $k$-variable counting logic $\mathcal{C}^{k}$ appearing in Theorem 21 is
captured by the pebbling comonad $\mathbb{P}_{k}^{+}$ on $\Sigma^{+}$. In
fact, it follows directly from [1, Theorem 18] that, whenever $A,B$ are finite
$\sigma$-structures, $F^{\mathbb{P}_{k}^{+}}(J(A))\cong
F^{\mathbb{P}_{k}^{+}}(J(B))$ if, and only if, $A\equiv_{\mathcal{C}^{k}}B$.
However, the comonad $\mathbb{P}_{k}^{+}$ does not satisfy item 2 in Theorem
16, because $\mathbb{P}_{k}^{+}(A)$ is infinite even when
$A\in\Sigma^{+}_{f}$.

To circumvent this problem, we consider the comonads $\mathbb{P}_{k,n}^{+}$,
which do restrict to finite $\sigma^{+}$-structures. Again by (the proof of)
[1, Theorem 18], for any finite $\sigma$-structures $A,B$,

$A\equiv_{\mathcal{C}^{k}_{n}}B\ \ \Longleftrightarrow\ \
F^{\mathbb{P}_{k,n}^{+}}(J(A))\cong F^{\mathbb{P}_{k,n}^{+}}(J(B))$

where $\mathcal{C}_{n}^{k}$ consists of the formulas that are simultaneously
in $\mathcal{C}_{n}$ and $\mathcal{C}^{k}$. Thus, items 1 and 2 in Theorem 16
are satisfied for $\mathbb{C}=\mathbb{P}_{k,n}$,
$\mathbb{C}^{+}=\mathbb{P}_{k,n}^{+}$, and $\mathcal{L}=\mathcal{C}_{n}^{k}$.

Assume for a moment that item 3 is also satisfied. Then, combining Theorem 16
with Proposition 4, we obtain that

$A\equiv_{\mathcal{C}^{k}_{n}}B\ \text{ if, and only if, }\
|\hom_{\Sigma_{f}}(C,A)|=|\hom_{\Sigma_{f}}(C,B)|$

for all finite $\sigma$-structures $C$ whose Gaifman graph $\mathcal{G}_{C}$
admits a $k$-pebble forest cover of height ${\leq\,}n$. Observe next that (i)
${A\equiv_{\mathcal{C}^{k}}B}$ precisely when $A\equiv_{\mathcal{C}^{k}_{n}}B$
for all $n$, and (ii) a finite $\sigma$-structure $C$ has tree-width at most
$k-1$ if, and only if, $\mathcal{G}_{C}$ admits a $k$-pebble forest cover of
height ${\leq\,}n$ for some $n$. Therefore, $A\equiv_{\mathcal{C}^{k}}B$ if,
and only if,

$|\hom_{\Sigma_{f}}(C,A)|=|\hom_{\Sigma_{f}}(C,B)|$

for all finite $\sigma$-structures $C$ with tree-width at most $k-1$, thus
settling Theorem 21.

In the remainder of this section, we prove that item 3 in Theorem 16 is indeed
satisfied. As mentioned already,
$\Sigma_{f}\cap\mathrm{im}(U^{\mathbb{P}_{k,n}})$ consists of the finite
$\sigma$-structures that admit a $k$-pebble forest cover of height
${\leq\,}n$, and similarly for
$\Sigma^{+}_{f}\cap\mathrm{im}(U^{\mathbb{P}_{k,n}^{+}})$. To improve
readability, let us denote these categories by $\mathcal{T}_{k,n}$ and
$\mathcal{T}_{k,n}^{+}$, respectively. Note that
$J\colon\Sigma_{f}\to\Sigma_{f}^{+}$ restricts to a functor
$\mathcal{T}_{k,n}\to\mathcal{T}_{k,n}^{+}$. It remains to show that its left
adjoint $H$ restricts to $\mathcal{T}_{k,n}^{+}\to\mathcal{T}_{k,n}$.

Recall from Section 2.3 that a forest cover of a $\sigma$-structure $A$ can be
identified with a forest order $\leq$ on $A$ that is _compatible_ , in the
sense that $a{\,\uparrow\,}a^{\prime}$ whenever $a{\,\frown\,}a^{\prime}$ in
$\mathcal{G}_{A}$. Suppose that $A$ is equipped with a forest order $\leq$ and
let $p\colon A\to\mathbf{k}$ be any function. We define a relation $\bowtie$
on $A$ as follows: $a\bowtie a^{\prime}$ (read as _$a$ sees $a^{\prime}$_) if
$a{\,\uparrow\,}a^{\prime}$ and

$\min(a,a^{\prime})<z\leq\max(a,a^{\prime})\ \Longrightarrow\ p(z)\neq
p(\min(a,a^{\prime}))$

for all $z\in A$. With this notation, a $k$-pebble forest cover of $A$ can be
identified with a triple $(A,\leq,p)$ where $\leq$ is a forest order on $A$
and $p\colon A\to\mathbf{k}$ is such that $a{\,\frown\,}a^{\prime}$ implies
$a\bowtie a^{\prime}$ for all $a,a^{\prime}\in A$. Just observe that $\leq$ is
a compatible forest order since $a\bowtie a^{\prime}$ entails
$a{\,\uparrow\,}a^{\prime}$.

Saying that $H$ restricts to $\mathcal{T}_{k,n}^{+}\to\mathcal{T}_{k,n}$ means
that, whenever a finite $\sigma^{+}$-structure $A$ admits a $k$-pebble forest
cover of height ${\leq\,}n$, then so does the quotient $A^{-}/{\sim}$ where
$A^{-}$ is the $\sigma$-reduct of $A$ and $\sim$ is the least equivalence
relation containing $I^{A}$. The difficulty in showing this consists in
defining the pebbling function on $A^{-}/{\sim}$. We do this by considering
consecutive one-step quotients (inspired by equality elimination from Section
6), where at each step a new pair of distinct elements in $I^{A}$ is
identified. As $A$ is finite, this construction terminates after finitely many
steps and yields the quotient $A^{-}/{\sim}$.

Let $\mathbb{A}\coloneqq(A,\leq,p)$ be a finite $\sigma^{+}$-structure
together with a $k$-pebble forest cover of height ${\leq\,}n$. Suppose that
there is a pair $(u,v)\in I^{A}$ such that $u\neq v$. Then $u{\,\uparrow\,}v$,
and we can assume without loss of generality that $u<v$. The one-step quotient
$\mathbb{A}/_{u\sim v}\coloneqq(A^{\prime},\leq^{\prime},p^{\prime})$ of
$\mathbb{A}$ is defined as follows:

  * •

the carrier of $\mathbb{A}/_{u\sim v}$ is the set $A^{\prime}\coloneqq
A\setminus\\{v\\}$;

  * •

the forest order $\leq^{\prime}$ is the restriction of $\leq$ to $A^{\prime}$;

  * •

for each $R\in\sigma\cup\\{I\\}$, the relation $R^{A^{\prime}}$ is obtained by
replacing all occurrences of $v$ by $u$ in each tuple of $R^{A}$.

  * •

the pebbling function $p^{\prime}\colon A^{\prime}\to\mathbf{k}$ is defined by

$w\mapsto\begin{cases}p(u)&\text{if }v\leq w,\ p(w)=p(v),\ \text{and
}u\not\bowtie w_{\min}\\\ p(v)&\text{if }v\leq w,\ p(w)=p(u),\ \text{and
}v\bowtie w_{\min}\\\ p(w)&\text{otherwise}\end{cases}$

where $w_{\min}\coloneqq\min\\{w^{\prime}\in A\mid v<w^{\prime}\leq w\text{
and }p(w^{\prime})=p(w)\\}$.

Clearly, $\leq^{\prime}$ is a forest order of height ${\leq\,}n$ on
$A^{\prime}$. Further, $a{\,\frown\,}a^{\prime}$ implies $a\bowtie a^{\prime}$
for all $a,a^{\prime}\in A^{\prime}$. This follows from the next lemma, which
is proved by a careful case analysis.

######  Lemma 22.

Let $w,w^{\prime}\in A\setminus\\{v\\}$. Then the following hold:

  1. (1)

$v\bowtie w$ in $\mathbb{A}$ implies $u\bowtie w$ in $\mathbb{A}/_{u\sim v}$;

  2. (2)

$w\bowtie w^{\prime}$ in $\mathbb{A}$ implies $w\bowtie w^{\prime}$ in
$\mathbb{A}/_{u\sim v}$.

###### Proof.

(1) Suppose $w\in A\setminus\\{v\\}$ and $v\bowtie w$ in $\mathbb{A}$. There
are two possibilities, either $v<w$ or $w<v$. In both cases we have that
$w{\,\uparrow\,}u$ and so we only need to check the condition on the pebbling
function $p^{\prime}$. Assume that $v<w$. As $(u,v)\in I^{A}$, we know that
$u{\,\frown\,}v$ and so $u\bowtie v$ in $\mathbb{A}$. Because
$p^{\prime}(z)=p(z)$ whenever $v\not\leq z$, to show that $u\bowtie w$ in
$\mathbb{A}/_{u\sim v}$ we only need to check that

$\forall z\in A,\ \ v<z\leq w\ \Longrightarrow\
p^{\prime}(z)\not=p^{\prime}(u).$ (1)

Observe that $p^{\prime}(u)=p(u)$. Also, by definition of $p^{\prime}$, for
any $z$ such that $v<z\leq w$ the equality $p^{\prime}(z)=p(u)$ is satisfied
if, and only if, either $p(z)=p(v)$ and $u\not\bowtie z_{\min}$, or
$p(z)=p(u)$ and $v\not\bowtie z_{\min}$. However, none of these two scenarios
can occur because $v\bowtie w$ implies $p(z)\neq p(v)$ and $v\bowtie
z_{\min}$. Hence, the condition in (1) is satisfied.

On the other hand, assume that $w<v$. Then $u{\,\uparrow\,}w$. If $u<w$ then
$u\bowtie v$ implies $u\bowtie w$ in $\mathbb{A}$. Similarly, if $w\leq u$
then $v\bowtie w$ entails $u\bowtie w$ in $\mathbb{A}$. Therefore, $u\bowtie
w$ in $\mathbb{A}/_{u\sim v}$ because $p(z)=p^{\prime}(z)$ for every $z$ such
that $v\not\leq z$.

(2) Let $w,w^{\prime}\in A\setminus\\{v\\}$ be such that $w\bowtie w^{\prime}$
in $\mathbb{A}$. We can assume without loss of generality that $w\leq
w^{\prime}$. If $v\not\leq w^{\prime}$ then $p(z)=p^{\prime}(z)$ for every $z$
such that $w\leq z\leq w^{\prime}$, and so $w\bowtie w^{\prime}$ in
$\mathbb{A}/_{u\sim v}$. Thus, suppose $v\leq w^{\prime}$. It follows that
$v{\,\uparrow\,}w$ and so either $v<w$ or $w<v$.

First we assume $v<w\leq w^{\prime}$. Note that, for any $z$ such that
$w<z\leq w^{\prime}$, if $p^{\prime}(z)=p^{\prime}(w)$ and
$p(z)\notin\\{p(u),p(v)\\}$, then by definition of $p^{\prime}$ we must have
$p(z)=p(w)$, contradicting the fact that $w\bowtie w^{\prime}$ in
$\mathbb{A}$. So, we only have to take care of the case where either
$p(z)=p(u)$ or $p(z)=p(v)$. Set

$\displaystyle U\coloneqq\\{x\in A\mid v<x\leq w^{\prime}\text{ and
}p(x)=p(u)\\}$ $\displaystyle V\coloneqq\\{x\in A\mid v<x\leq w^{\prime}\text{
and }p(x)=p(v)\\}.$

Suppose $U$ and $V$ are non-empty and so they admit minimal elements
$\overline{u}$ and $\overline{v}$, respectively. Then, either
$\overline{u}<\overline{v}$ or $\overline{v}<\overline{u}$. If
$\overline{u}<\overline{v}$ then any $z\geq\overline{u}$ such that $p(z)=p(u)$
satisfies $v\bowtie z_{\min}$ (because $z_{\min}=\overline{u}$) and so
$p^{\prime}(z)=p(v)$, and similarly any $z\geq\overline{u}$ such that
$p(z)=p(v)$ satisfies $u\not\bowtie z_{\min}$ (because
$z_{\min}=\overline{v}$) and so $p^{\prime}(z)=p(u)$. On the other hand, if
$\overline{v}<\overline{u}$ then $p^{\prime}(z)=p(z)$ for any
$z\geq\overline{v}$. Either way, for any $z$ between $w$ and $w^{\prime}$,
$p^{\prime}(z)=p^{\prime}(w)$ implies $p(z)=p(w)$. Hence, $w\bowtie
w^{\prime}$ in $\mathbb{A}$ entails $w\bowtie w^{\prime}$ in
$\mathbb{A}/_{u\sim v}$. A similar reasoning applies, mutatis mutandis, when
$U=\emptyset$ or $V=\emptyset$.

Suppose next that $w<v<w^{\prime}$. Then $p^{\prime}(w)=p(w)$ and, as
$w\bowtie w^{\prime}$ in $\mathbb{A}$, it follows that $p(w)\not=p(v)$. If
$p(w)\not=p(u)$ then we conclude that $w\bowtie w^{\prime}$ in
$\mathbb{A}/_{u\sim v}$ because $p^{\prime}(z)=p^{\prime}(w)$ entails
$p(z)=p(w)$ for any element $z$ between $w$ and $w^{\prime}$. To conclude the
proof, suppose towards a contradiction that $p(w)=p(u)$ and there exists a
$z\in A\setminus\\{v\\}$ such that $w<z\leq w^{\prime}$ and
$p^{\prime}(z)=p^{\prime}(w)$. Then, $p^{\prime}(z)=p(u)$. Since $w\bowtie
w^{\prime}$ in $\mathbb{A}$, we get $p(z)\not=p(u)$ and so $v<z$, $p(z)=p(v)$
and $u\not\bowtie z_{\min}$ in $\mathbb{A}$. As $u\bowtie v$ in $\mathbb{A}$,
there must exist an $x$ such that

$w<v<x\leq z_{\min}\leq z\leq w^{\prime}$

and $p(x)=p(u)$, contradicting the fact that $w\bowtie w^{\prime}$ in
$\mathbb{A}$. ∎

Applying this construction iteratively, we obtain the following analogue of
Proposition 20, which concludes the proof of Dvořák’s theorem.

######  Proposition 23.

The functor $H$ restricts to $\mathcal{T}_{k,n}^{+}\to\mathcal{T}_{k,n}$.

###### Proof.

Let $\mathbb{A}_{0}=(A,\leq,p)$ be a finite $\sigma^{+}$-structure together
with a $k$-pebble forest cover of height ${\leq\,}n$. Then we have a sequence
$\mathbb{A}_{0},\mathbb{A}_{1},\mathbb{A}_{2},\dots$ such that
$\mathbb{A}_{i+1}$ is defined as $\mathbb{A}_{i}/_{u\sim v}$ for some pair of
distinct elements $(u,v)\in I^{A_{i}}$, where $A_{i}$ is the
$\sigma^{+}$-structure underlying $\mathbb{A}_{i}$. This is iterated as long
as such a pair $(u,v)$ can be found. Let $\mathbb{A}_{n}$ be the last element
of the sequence. Note that, by construction, the $\sigma$-reduct of $A_{n}$ is
isomorphic to $H(A)$. Because $A_{n}$ admits a $k$-pebble forest cover of
height ${\leq\,}n$ witnessed by $\mathbb{A}_{n}$—by repeatedly applying Lemma
22—so does $H(A)$. ∎

######  Remark 24.

An advantage of the categorical approach to homomorphism counting is that it
specialises to any full subcategory $\mathcal{A}$ of $\Sigma$, provided the
game comonad in question restricts to $\mathcal{A}$. For example, let $\sigma$
consist of a single binary relation symbol, so that $\Sigma$ is the category
of (directed) graphs and graph homomorphisms. As the pebbling comonad
$\mathbb{P}_{k}$ restricts to the full subcategory of $\Sigma$ defined by
undirected graphs without loops, we obtain an analogue of Theorem 21 where
$A,B,C$ range over the class of finite undirected graphs without loops. A
similar observation applies to the Ehrenfeucht–Fraïssé comonad
$\mathbb{E}_{n}$, yielding a variant of Theorem 18 for undirected graphs
without loops.

###  4.3. A proof of Theorem 16

We start by showing that the functor $H\colon\Sigma^{+}\to\Sigma$ sending $D$
to $D^{-}/{\sim}$, where $D^{-}$ is the $\sigma$-reduct of $D$ and $\sim$ is
the equivalence relation generated by $I^{D}$, is left adjoint to $J$.

######  Lemma 25.

$H\colon\Sigma^{+}\to\Sigma$ is left adjoint to the embedding $J$.

###### Proof.

It suffices to show that for every $D\in\Sigma^{+}$, the unique
$\sigma^{+}$-homomorphism $e_{D}\colon D\to JH(D)$ extending the quotient map
$D^{-}\twoheadrightarrow H(D)$ satisfies the following universal property: For
every $\sigma^{+}$-homomorphism $j\colon D\to J(C)$, there exists a unique
$\sigma$-homomorphism $h\colon H(D)\to C$ making the following diagram
commute.

${D}$${JH(D)}$${J(C)}$$\scriptstyle{e_{D}}$$\scriptstyle{j}$$\scriptstyle{J(h)}$

Pick an arbitrary $\sigma^{+}$-homomorphism $j\colon D\to J(C)$. Since $j$
preserves the relation $I$, $d_{1}{\sim}d_{2}$ entails $j(d_{1})=j(d_{2})$ for
all $d_{1},d_{2}\in D$. Hence, the following map is well defined

$h\colon H(D)\to C,\ \ h([d])\coloneqq j(d)$

where $[d]$ denotes the $\sim$-equivalence class of $d$. Moreover, $h$ is a
$\sigma$-homomorphism. Just observe that, for any relation symbol $R\in\sigma$
of arity $n$, if $([d_{1}],\ldots,[d_{n}])\in R^{H(D)}$ then there are
$d^{\prime}_{1}\sim d_{1},\ldots,d^{\prime}_{n}\sim d_{n}$ such that
$(d^{\prime}_{1},\ldots,d^{\prime}_{n})\in R^{D}$. Thus,
$(h([d_{1}]),\ldots,h([d_{n}]))=(j(d^{\prime}_{1}),\ldots,j(d^{\prime}_{n}))\in
R^{C}$. Further, $j=J(h)\circ e_{D}$ by construction. To conclude, note that
$h$ is unique with this property because $e_{D}$ is surjective. ∎

######  Remark 26.

Since both $J$ and $H$ send finite structures to finite structures, they
restrict to an adjunction $H\dashv J\colon\Sigma_{f}\to\Sigma_{f}^{+}$.

Before proceeding to the proof of Theorem 16, we make the following easy
observation.

######  Lemma 27.

Assume that $J$ and $H$ restrict to full subcategories
$\mathcal{A}\subseteq\Sigma_{f}$ and $\mathcal{A}^{+}\subseteq\Sigma_{f}^{+}$.
Then, for any $A,B\in\Sigma_{f}$, the following are equivalent:

  1. (1)

$\hom_{\Sigma_{f}}(C,A)\cong\hom_{\Sigma_{f}}(C,B)\ \ \forall
C\in\mathcal{A}$;

  2. (2)

$\hom_{\Sigma_{f}^{+}}(C^{\prime},J(A))\cong\hom_{\Sigma_{f}^{+}}(C^{\prime},J(B))\
\ \forall C^{\prime}\in\mathcal{A}^{+}$.

###### Proof.

Assume item 1 holds. For any $C^{\prime}\in\mathcal{A}^{+}$,

$\displaystyle\hom_{\Sigma_{f}^{+}}(C^{\prime},J(A))$
$\displaystyle\cong\hom_{\Sigma_{f}}(H(C^{\prime}),A)$ ($H\dashv J$)
$\displaystyle\cong\hom_{\Sigma_{f}}(H(C^{\prime}),B)$
($H(C^{\prime})\in\mathcal{A}$)
$\displaystyle\cong\hom_{\Sigma_{f}^{+}}(C^{\prime},J(B)).$ ($H\dashv J$)

Conversely, suppose item 2 holds. Then, for any $C\in\mathcal{A}$,

$\displaystyle\hom_{\Sigma_{f}}(C,A)$
$\displaystyle\cong\hom_{\Sigma_{f}^{+}}(J(C),J(A))$ ($J$ embedding)
$\displaystyle\cong\hom_{\Sigma_{f}^{+}}(J(C),J(B))$
($J(C)\in\mathcal{A}^{+}$) $\displaystyle\cong\hom_{\Sigma_{f}}(C,B).$ ($J$
embedding)

This concludes the proof. ∎

###### Proof of Theorem 16.

For convenience of notation, let
$\mathrm{EM}_{f}^{+}\coloneqq\mathrm{EM}_{f}(\mathbb{C}^{+})$. Combining item
1 with Corollary 14 applied to the comonad $\mathbb{C}^{+}$, we see that, for
all $A,B\in\Sigma_{f}$, $A\equiv_{\mathcal{L}}B$ if, and only if,

$|\hom_{\mathrm{EM}_{f}^{+}}(D,F^{\mathbb{C}^{+}}(J(A)))|=|\hom_{\mathrm{EM}_{f}^{+}}(D,F^{\mathbb{C}^{+}}(J(B)))|$
(2)

for all finite coalgebras $D\in\mathrm{EM}_{f}^{+}$. Note that here we used
the fact that, by item 2, $F^{\mathbb{C}^{+}}(D^{\prime})$ is a finite
coalgebra whenever $D^{\prime}$ is a finite $\sigma^{+}$-structure. In view of
the adjunction $U^{\mathbb{C}^{+}}\dashv F^{\mathbb{C}^{+}}$, the condition in
equation (2) is equivalent to

$|\hom_{\Sigma^{+}_{f}}(U^{\mathbb{C}^{+}}(D),J(A))|=|\hom_{\Sigma^{+}_{f}}(U^{\mathbb{C}^{+}}(D),J(B))|$

for all $D\in\mathrm{EM}_{f}^{+}$. Finally, by item 3, an application of Lemma
27 with $\mathcal{A}\coloneqq\Sigma_{f}\cap\mathrm{im}(U^{\mathbb{C}})$ and
$\mathcal{A}^{+}\coloneqq\Sigma_{f}^{+}\cap\mathrm{im}(U^{\mathbb{C}^{+}})$
yields the desired statement. ∎

##  5\. Homomorphism Counting in Modal Logic

In this section we prove a new homomorphism counting result for (multi-)modal
logic. This is derived by applying the categorical framework from Section 3 to
a game comonad for modal logic defined on the category of pointed Kripke
structures. Since there is no equality in the logic, this time we can dispense
with the extra relation $I$. This considerably simplifies the proofs, compared
to the previous section.

Let $\sigma$ be a signature consisting of relation symbols of arity at most
$2$. Each unary relation symbol $P$ yields a propositional variable $p$, and
each binary relation symbol $R_{\alpha}$ yields modalities $\Box_{\alpha}$ and
$\Diamond_{\alpha}$. We can think of a $\sigma$-structure $A$ as a Kripke
structure for this multi-modal logic, where $P^{A}$ gives the valuation for
the propositional variable $p$, and $R_{\alpha}^{A}$ gives the accessibility
relation for the modalities $\Box_{\alpha}$ and $\Diamond_{\alpha}$.

Each formula $\varphi$ in this modal logic admits a translation into a first-
order formula $\llbracket\varphi\rrbracket_{x}$ in one free variable $x$; this
is known as the _standard translation_ , see e.g. [7, §2.4]. We let
$\llbracket p\rrbracket_{x}\coloneqq P(x)$ and let $\llbracket\
\rrbracket_{x}$ commute with Boolean connectives. Further, set
$\llbracket\Box_{\alpha}\varphi\rrbracket_{x}\coloneqq\forall
y.\,R_{\alpha}(x,y)\to\llbracket\varphi\rrbracket_{y}$ and
$\llbracket\Diamond_{\alpha}\varphi\rrbracket_{x}\coloneqq\exists
y.\,R_{\alpha}(x,y)\wedge\llbracket\varphi\rrbracket_{y}$ where $y$ is a fresh
variable. Consider a _pointed Kripke structure_ , that is a pair $(A,a)$ where
$A$ is a $\sigma$-structure and $a\in A$. Then $A,a\models\varphi$ according
to Kripke semantics if, and only if,
$A\models\llbracket\varphi\rrbracket_{x}[a/x]$ in the standard model-theoretic
sense.

Henceforth, we assume all Kripke structures under consideration are pointed.
Let $\mathsf{Kri}$ be the category of Kripke structures and
$\sigma$-homomorphisms preserving the distinguished element. For every natural
number $k$, there is a _modal comonad_ $\mathbb{M}_{k}$ on $\mathsf{Kri}$, see
[3]. For any Kripke structure $(A,a)$, the carrier of $\mathbb{M}_{k}(A,a)$ is
the set of all paths of length ${\leq\,}k$ starting from $a$:

$a\xrightarrow{R_{1}}a_{1}\xrightarrow{R_{2}}a_{2}\to\cdots\xrightarrow{R_{n}}a_{n}$

where $R_{1},\dots,R_{n}$ are binary relations from $\sigma$. The
distinguished element of the Kripke structure $\mathbb{M}_{k}(A,a)$ is the
trivial path $(a)$ of length $0$. If $P\in\sigma$ is unary then
$P^{\mathbb{M}_{k}(A,a)}$ is defined as the set of paths $p$ such that the
last element $a_{n}$ of $p$ belongs to $P^{A}$. For a binary relation symbol
$R\in\sigma$, let $R^{\mathbb{M}_{k}(A,a)}$ be the set of pairs of paths
$(p,p^{\prime})$ such that $p^{\prime}$ is obtained by extending $p$ by one
step along $R$. The morphism
$\varepsilon_{(A,a)}\colon\mathbb{M}_{k}(A,a)\to(A,a)$ sends a path to its
last element; for the definition of the coextension operation, see [3, §2.3].

The comonad $\mathbb{M}_{k}$ captures a well known combinatorial parameter of
Kripke structures, as we now recall. Let us say that a Kripke structure
$(A,a)$ is _rooted_ if, for any $a^{\prime}\in A$, there is a path from $a$ to
$a^{\prime}$. If we further require that this path be unique, then $(A,a)$ is
a _synchronization tree_. A synchronization tree $(A,a)$ has _height
${\leq\,}k$_ if, for each $a^{\prime}\in A$, the length of the unique path
from $a$ to $a^{\prime}$ is at most $k$. For a proof of the following result,
see [4, Proposition 6.6].

######  Proposition 28.

A rooted Kripke structure $(A,a)$ admits a coalgebra structure
$(A,a)\to\mathbb{M}_{k}(A,a)$ if, and only if, $(A,a)$ is a synchronization
tree of height ${\leq\,}k$.

On the other hand, the modal comonad $\mathbb{M}_{k}$ characterises logical
equivalence with respect to an appropriate modal logic. Let us extend the
multi-modal logic introduced above by adding, for every positive integer $n$
and binary relation symbol $R_{\alpha}\in\sigma$, _graded modalities_
$\Box_{\alpha}^{n}$ and $\Diamond_{\alpha}^{n}$ defining
$A,a\models\Diamond_{\alpha}^{n}\varphi$ if there are at least $n$ distinct
$R_{\alpha}$-successors of $a$ that satisfy $\varphi$ (and
$\Box_{\alpha}^{n}\varphi=\neg\Diamond_{\alpha}^{n}\neg\varphi$). A formula in
this graded modal logic has _modal depth ${\leq\,}k$_ if it contains at most
$k$ nested modalities. Let $\mathcal{C}^{\mathrm{ML}}_{k}$ be the image of the
standard translation of formulas with graded modalities that have modal depth
${\leq\,}k$. The following result is a special case of [3, Theorem 16].

######  Proposition 29.

For finite Kripke structures $(A,a)$ and $(B,b)$,

$(A,a)\equiv_{\mathcal{C}^{\mathrm{ML}}_{k}}(B,b)\quad\text{iff}\quad
F^{\mathbb{M}_{k}}(A,a)\,\cong\,F^{\mathbb{M}_{k}}(B,b).$

We aim to exploit the two preceding propositions to obtain a characterisation
of the equivalence relation $\equiv_{\mathcal{C}^{\mathrm{ML}}_{k}}$ over
finite Kripke structures in terms of homomorphism counts from finite
synchronization trees of height ${\leq\,}k$ (Theorem 31 below).

To this end, let $\mathsf{Kri}_{f}$ and $\mathsf{RKri}_{f}$ be the full
subcategories of $\mathsf{Kri}$ consisting, respectively, of the finite Kripke
structures, and finite rooted Kripke structures. Note that $\mathbb{M}_{k}$
restricts to a comonad on $\mathsf{Kri}_{f}$, that we denote again by
$\mathbb{M}_{k}$. Further, as $\mathbb{M}_{k}(A,a)$ is a finite
synchronization tree whenever $(A,a)$ is a finite Kripke structure,
$\mathbb{M}_{k}$ restricts to a comonad $\mathbb{M}_{k}^{*}$ on the category
$\mathsf{RKri}_{f}$.

######  Lemma 30.

The following statements hold:

  1. (1)

the inclusion $\mathsf{RKri}_{f}\hookrightarrow\mathsf{Kri}_{f}$ has a right
adjoint $R$;

  2. (2)

$R$ lifts to a functor
$\overline{R}\colon\mathrm{EM}(\mathbb{M}_{k})\to\mathrm{EM}(\mathbb{M}_{k}^{*})$
making the following diagram commute.

${\mathrm{EM}(\mathbb{M}_{k})}$${\mathrm{EM}(\mathbb{M}_{k}^{*})}$${\mathsf{Kri}_{f}}$${\mathsf{RKri}_{f}}$$\scriptstyle{\overline{R}}$$\scriptstyle{F^{\mathbb{M}_{k}}}$$\scriptstyle{R}$$\scriptstyle{F^{\mathbb{M}_{k}^{*}}}$

###### Proof.

(1) For any finite Kripke structure $(A,a)$, let $R(A,a)$ be the substructure
of $(A,a)$ consisting of the elements accessible from $a$. To show that this
assignment extends to a functor $R$ that is a right adjoint to the inclusion
$\mathsf{RKri}_{f}\hookrightarrow\mathsf{Kri}_{f}$, it is enough to observe
that, for any $(A,a)\in\mathsf{Kri}_{f}$, $(B,b)\in\mathsf{RKri}_{f}$, and
homomorphism $h\colon(B,b)\to(A,a)$, there exists a unique homomorphism
$h^{\prime}\colon(B,b)\to R(A,a)$ such that $h=e\circ h^{\prime}$, where
$e\colon R(A,a)\to(A,a)$ is the substructure embedding.

(2) Let $\overline{R}$ be the functor sending a coalgebra
$\alpha\colon(A,a)\to\mathbb{M}_{k}(A,a)$ to its restriction
$\alpha_{\restriction R(A,a)}\colon R(A,a)\to\mathbb{M}_{k}^{*}R(A,a)$. Then
$\overline{R}F^{\mathbb{M}_{k}}(A,a)$ coincides with
$F^{\mathbb{M}_{k}^{*}}R(A,a)$, for any $(A,a)$ in $\mathsf{Kri}_{f}$, because
the carrier of $F^{\mathbb{M}_{k}}(A,a)=(\mathbb{M}_{k}(A,a),\delta_{A})$ is
rooted and consists only of paths of length ${\leq\,}k$ that start at $a$. The
equality on morphisms holds for the same reason. ∎

We are now ready to prove a Lovász-type theorem for graded modal logic.

######  Theorem 31.

Let $(A,a)$ and $(B,b)$ be finite (pointed) Kripke structures. Then
$(A,a)\equiv_{\mathcal{C}^{\mathrm{ML}}_{k}}(B,b)$ if, and only if,

$|\hom_{\mathsf{Kri}_{f}}((C,c),(A,a))|\,=\,|\hom_{\mathsf{Kri}_{f}}((C,c),(B,b))|$

for every finite synchronization tree $(C,c)$ of height ${\leq\,}k$.

###### Proof.

Let $\mathbb{A}\coloneqq(A,a)$ and $\mathbb{B}\coloneqq(B,b)$. For the purpose
of this proof, write $V\colon\mathsf{RKri}_{f}\hookrightarrow\mathsf{Kri}_{f}$
for the inclusion functor and let
$\mathrm{EM}^{*}\coloneqq\mathrm{EM}(\mathbb{M}_{k}^{*})$. By Proposition 28,
the statement about homomorphism counts is equivalent to

$|\hom_{\mathsf{Kri}_{f}}(V(U^{\mathbb{M}_{k}^{*}}(\mathbb{D})),\mathbb{A})|\,=\,|\hom_{\mathsf{Kri}_{f}}(V(U^{\mathbb{M}_{k}^{*}}(\mathbb{D})),\mathbb{B})|$

for all coalgebras $\mathbb{D}$ in $\mathrm{EM}^{*}$. In turn, by virtue of
the adjunctions $V\dashv R$ and $U^{\mathbb{M}_{k}^{*}}\dashv
F^{\mathbb{M}_{k}^{*}}$, this is equivalent to

$|\hom_{\mathrm{EM}^{*}}(\mathbb{D},F^{\mathbb{M}_{k}^{*}}(R(\mathbb{A})))|\,=\,|\hom_{\mathrm{EM}^{*}}(\mathbb{D},F^{\mathbb{M}_{k}^{*}}(R(\mathbb{B})))|$

for all $\mathbb{D}\in\mathrm{EM}^{*}$. Since $\mathrm{EM}^{*}$ is
combinatorial by Corollary 14 and Remark 15, the last statement is equivalent
to $F^{\mathbb{M}_{k}^{*}}(R(\mathbb{A}))\cong
F^{\mathbb{M}_{k}^{*}}(R(\mathbb{B}))$ and thus, by Lemma 30, to
$\overline{R}(F^{\mathbb{M}_{k}}(\mathbb{A}))\cong\overline{R}(F^{\mathbb{M}_{k}}(\mathbb{B}))$.
Note that the restriction of $\overline{R}$ to the image of
$F^{\mathbb{M}_{k}}$ is full and faithful. Hence,
$\overline{R}(F^{\mathbb{M}_{k}}(\mathbb{A}))\cong\overline{R}(F^{\mathbb{M}_{k}}(\mathbb{B}))$
if, and only if, $F^{\mathbb{M}_{k}}(\mathbb{A})\cong
F^{\mathbb{M}_{k}}(\mathbb{B})$ which, by Proposition 29, is equivalent to
$\mathbb{A}\equiv_{\mathcal{C}^{\mathrm{ML}}_{k}}\mathbb{B}$. ∎

##  6\. Logical Normal Forms

Let $\mathcal{C}^{k}_{\infty}$ denote the closure of $\mathcal{C}^{k}$ under
infinitary conjunctions and disjunctions. This infinitary logic has been much
studied in finite model theory as a means of delimiting the expressive power
of fixed-point logics with counting. In this logic we can express all, and
only, the properties of finite structures that are invariant under the
equivalence relation $\equiv_{\mathcal{C}^{k}}$. In fact, since it is known
that each finite structure is characterised up to $\equiv_{\mathcal{C}^{k}}$
by a single sentence of $\mathcal{C}^{k}$, it follows that every class of
finite structures that is invariant under $\equiv_{\mathcal{C}^{k}}$ is
defined by a single infinitary disjunction of $\mathcal{C}^{k}$ sentences (see
[24] for details). An entirely analogous normal form holds for
$\mathcal{C}_{n,\infty}$—the closure of $\mathcal{C}_{n}$ under infinitary
conjunctions and disjunctions (see [19, Chapter 8]).

The theorems of Dvořák and Grohe provide a route to alternative normal forms
for these infinitary logics. To see this, note that for any finite structure
$A$, we can write a primitive positive sentence $\gamma_{A}$ of first-order
logic such that for any $B$, $B\models\gamma_{A}$ if, and only if, there is a
homomorphism from $A$ to $B$. Here, _primitive positive_ means that the
sentence is built up from atomic formulas using only conjunctions and
existential quantification. The sentence $\gamma_{A}$ is called the _canonical
conjunctive query of $A$_ (see [13, Chapter 6]). It is known that if $A$ has
tree-width strictly less than $k$, then $\gamma_{A}$ can be written using no
more than $k$ variables [18, Lemma 5.2]. Similarly, if $A$ has tree-depth at
most $n$, then $\gamma_{A}$ can be chosen to have quantifier depth at most $n$
[29, Lemma 2.14].

Given a positive integer $t$, we can transform $\gamma_{A}$ by standard means
into a sentence $\gamma_{A}^{t}$ of $\mathcal{C}$ which asserts that there are
at least $t$ distinct homomorphisms from $A$. That is, for any $B$,
$B\models\gamma^{t}_{A}$ if, and only if, $|\hom(A,B)|\geq t$. To show this,
we establish something more general.

Let $\gamma(\bar{x})$ be a primitive positive formula with free variables
among $\bar{x}$. For any structure $B$ and any interpretation $\iota$ taking
the variables in $\bar{x}$ to elements of $B$, we write
$B\models\gamma[\iota]$ to indicate that the formula $\gamma$ is satisfied in
$B$ when the free variables $\bar{x}$ are interpreted according to $\iota$.
Since $\gamma$ is primitive positive, we have $B\models\gamma[\iota]$
precisely if there is a function $\kappa$ mapping the existential quantifiers
in $\gamma$ to elements of $B$ so that every atomic formula $R(\bar{y})$
occurring in $\gamma$ is satisfied in $B$ when each variable $y$ in $\bar{y}$
is interpreted by $\iota(y)$, if this occurrence of $y$ is free in $\gamma$,
and by $\kappa$ applied to the quantifier binding $y$ otherwise. We write
$|B\models\gamma[\iota]|$ to denote the number of distinct functions $\kappa$
witnessing $B\models\gamma[\iota]$ and observe that
$|B\models\gamma_{A}|=|\hom(A,B)|$.

We now define by induction on the structure of $\gamma$ a formula
$\gamma^{t}(\bar{x})$ of $\mathcal{C}$ with the property that for any
structure $B$ and interpretation $\iota$ of $\bar{x}$ in $B$, we have
$B\models\gamma^{t}[\iota]$ if, and only if, $|B\models\gamma[\iota]|\geq t$.
For atomic $\gamma$, $\gamma^{1}$ is just $\gamma$ and $\gamma^{t}$ is false
if $t>1$. For $\gamma$ a conjunction $\gamma_{1}\land\gamma_{2}$, let
$T\coloneqq\\{(t_{1},t_{2})\in\mathbb{N}^{2}\mid t_{1}\cdot t_{2}\geq t\\}$.
Then

$\gamma^{t}\coloneqq\bigvee_{(t_{1},t_{2})\in
T}(\gamma^{t_{1}}_{1}\land\gamma^{t_{2}}_{2}).$

When $\gamma$ is $\exists x.\gamma_{1}$, let $F$ be the collection of all
finite partial functions $f$ on $\mathbb{N}$ such that
$\sum_{s\in\mathrm{dom}(f)}sf(s)\geq t$. Then

$\gamma^{t}\coloneqq\bigvee_{f\in
F}\bigwedge_{s\in\mathrm{dom}(f)}\exists_{\geq f(s)}x.\gamma_{1}^{s}.$

Note that both the quantifier rank and the total number of variables that
appear in $\gamma^{t}_{A}$ are the same as for $\gamma_{A}$, and
$\gamma^{t}_{A}$ still has no negation symbols. It then follows from Dvořák’s
theorem that any sentence $\varphi$ of $\mathcal{C}^{k}_{\infty}$ is
equivalent in the finite (i.e., over finite structures) to an infinite Boolean
combination of sentences of $\mathcal{C}^{k}$ of the form $\gamma^{t}_{A}$.
Indeed, $\varphi$ is equivalent to

$\bigvee_{B\in\mathcal{M}}\
\bigwedge_{A\in\mathcal{T}}\left(\gamma^{|\hom(A,B)|}_{A}\land\neg\gamma^{|\hom(A,B)|+1}_{A}\right)$

where $\mathcal{M}$ consists of one representative for each
$\equiv_{\mathcal{C}^{k}}$-class of structures in $\\{B\mid
B\models\varphi\\}$ and $\mathcal{T}$ consists of one representative for each
isomorphism class of finite structures that have tree-width at most $k-1$.

Likewise, it is a consequence of Grohe’s theorem that any sentence of
$\mathcal{C}_{n,\infty}$ is equivalent (in the finite) to an infinite Boolean
combination of sentences of $\mathcal{C}_{n}$ of the form $\gamma^{t}_{A}$; a
similar normal form was also exhibited in [14, §5]. This yields an interesting
normal form for these counting logics. In particular, there is no need of
universal quantifiers or of equality, as neither of these is used in the
sentences $\gamma^{t}_{A}$. Further, if we allow dual counting quantifiers
$\exists_{{\leq}i}$ with the semantics that
$A\models\exists_{{\leq}i}x.\,\varphi$ if, and only if, $A\models\varphi[a/x]$
holds for at most $i$ distinct elements $a\in A$, then we do not need negation
at all in our formulas.

From our point of view, the most interesting aspect of this is the elimination
of equality symbols. Consider for example the simple first-order sentence in
the language of graphs: $\exists x\exists y.(x\neq y\land E(x,y))$ asserting
the existence of an edge between two distinct vertices. At first sight, it
does not seem possible to express this property without using the equality
symbol. However, it is possible to do so with infinitary Boolean connectives
and counting quantifiers as we illustrate.

First, consider the formula $\exists_{\geq t}xy.E(x,y)$ asserting that there
exist at least $t$ pairs $x,y$ for which $E(x,y)$. Note this is just
$\gamma^{t}$ when $\gamma$ is the sentence $\exists x\exists y.E(x,y)$. Now,
the sentence $\exists x\exists y.(x\neq y\land E(x,y))$ is equivalent to

$\bigvee_{i\in\mathbb{N}}\left(\exists_{\geq i}xy.E(x,y)\land\exists_{\leq
i-1}x.E(x,x)\right).$

We now give a direct proof, in our categorical framework, that we can
eliminate equality from $\mathcal{C}^{k}_{\infty}$ and
$\mathcal{C}_{n,\infty}$.

######  Theorem 32.

Every sentence of $\mathcal{C}^{k}_{\infty}$ is equivalent in the finite to
one without equality, and every sentence of $\mathcal{C}_{n,\infty}$ is
equivalent in the finite to one without equality.

###### Proof.

We give the proof only for $\mathcal{C}_{n,\infty}$ as the other is entirely
analogous. It suffices to prove that if two finite structures $A,B$ are not
distinguished by any sentence of $\mathcal{C}_{n}$ without equality, then they
are not distinguished by any sentence of $\mathcal{C}_{n}$.

Suppose then that $A$ and $B$ are not distinguished by any sentence of
$\mathcal{C}_{n}$ without equality. We thus have $F^{\mathbb{E}_{n}}(A)\cong
F^{\mathbb{E}_{n}}(B)$ in $\mathrm{EM}(\mathbb{E}_{n})$ and so
$\hom(D,F^{\mathbb{E}_{n}}(A))\cong\hom(D,F^{\mathbb{E}_{n}}(B))$ for every
$D$ in $\mathrm{EM}_{f}(\mathbb{E}_{n})$. By the adjunction
$U^{\mathbb{E}_{n}}\dashv F^{\mathbb{E}_{n}}$, we have
$\hom(U^{\mathbb{E}_{n}}(D),A)\cong\hom(U^{\mathbb{E}_{n}}(D),B)$ for every
$D$ in $\mathrm{EM}_{f}(\mathbb{E}_{n})$. Since a finite structure has tree-
depth at most $n$ if, and only if, it admits an $\mathbb{E}_{n}$-coalgebra
structure, this implies $\hom(C,A)\cong\hom(C,B)$ for every finite structure
$C$ with tree-depth at most $n$ and hence, by Theorem 18,
$A\equiv_{\mathcal{C}_{n}}B$. ∎

##  7\. Conclusion

The ideas developed in this paper connect homomorphism counting results in
finite model theory with the framework of game comonads recently put forward
by Abramsky et al.

Our categorical generalisation of Lovász’ theorem allows us to give uniform
proofs of results by Dvořák and Grohe. The only part of the proof specific to
each of these results is the combinatorial argument underlying the fact that
the adjunction between $\sigma$-structures and $\sigma^{+}$-structures
restricts to structures of bounded tree-width and bounded tree-depth,
respectively. We also establish a new homomorphism counting result for modal
logic which characterises the equivalence relation
$\equiv_{\mathcal{C}^{\mathrm{ML}}_{k}}$ over finite Kripke structures in
terms of homomorphism counts.

As a by-product of the modularity of this general framework, we are
immediately able to deduce: (i) the characterisation of the equivalence
relation $\equiv_{\mathcal{C}^{k}_{n}}$ in terms of homomorphism counts from
structures admitting a $k$-pebble forest cover of height ${\leq\,}n$, (ii) the
specialisation of our results to undirected graphs without loops (cf. Remark
24), and (iii) equality elimination results for counting logics (Theorem 32).

We believe that our method lays a pathway to discovering more Lovász-type
theorems. In particular, any comonad on the category of $\sigma$-structures
that satisfies the conditions of Theorem 16 will yield a Lovász-type theorem.
The natural next step to test this theory is to apply our results to the game
comonads introduced in [2] and [10].

On the other hand, there are many Lovász-type theorems that do not immediately
fit into our framework. For example, quantum isomorphism [23] and co-
spectrality are characterised by restricting the homomorphism counts to planar
graphs and cycles, respectively. Are there suitable comonads (or monads) that
could allow us to recover these characterisations in a uniform manner? Another
line for future investigation consists in fine-tuning the general theory
introduced in this paper. For example, can we refine Theorem 31 to yield a
homomorphism counting result for p-morphisms, the natural concept of morphism
between Kripke structures?

The ideas that we have described in this paper contribute to advancing the
theory of game comonads, which connects two distinct areas of logic in
computer science: on the one hand finite and algorithmic model theory, and on
the other hand categorical and structural methods in semantics. Game comonads
have been successfully applied, e.g., to investigate equirank-variable
homomorphism preservation theorems in finite model theory [25]. We broaden the
applicability of this theory by bringing these techniques to the area of
Lovász-type results in finite model theory.

## Acknowledgment

We acknowledge useful discussions in the Cambridge-Oxford Comonads seminar.
The last-named author is grateful to André Joyal for explaining to him
(private communication) the construction
$E(\,{\text{-}}\,)\mapsto{E}\llbracket\,{\text{-}}\,\rrbracket$ for polyadic
spaces [16], which features in Lemma 12.

## References

  * [1] S. Abramsky, A. Dawar, and P. Wang.  The pebbling comonad in finite model theory.  In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS, pages 1–12, 2017.
  * [2] S. Abramsky and D. Marsden.  Comonadic semantics for guarded fragments.  Preprint available at arXiv:2008.11094, 2020.
  * [3] S. Abramsky and N. Shah.  Relating Structure and Power: Comonadic semantics for computational resources.  In 27th EACSL Annual Conference on Computer Science Logic, CSL, pages 2:1–2:17, 2018.
  * [4] S. Abramsky and N. Shah.  Relating Structure and Power: Extended version.  To appear in Journal of Logic and Computation, preprint available at arXiv:2010.06496, 2021\.
  * [5] J. Adámek, H. Herrlich, and G. E. Strecker.  Abstract and concrete categories.  John Wiley & Sons, Inc., New York, 1990.
  * [6] J. Adámek and J. Rosický.  Locally presentable and accessible categories, volume 189 of London Mathematical Society Lecture Note Series.  Cambridge University Press, Cambridge, 1994.
  * [7] P. Blackburn, M. de Rijke, and Y. Venema.  Modal logic, volume 53 of Cambridge Tracts in Theoretical Computer Science.  Cambridge University Press, Cambridge, 2001.
  * [8] F. Borceux.  Handbook of categorical algebra. 1, volume 50 of Encyclopedia of Mathematics and its Applications.  Cambridge University Press, Cambridge, 1994.
  * [9] J.-Y. Cai, M. Fürer, and N. Immerman.  An optimal lower bound on the number of variables for graph identification.  Combinatorica, 12(4):389–410, 1992.
  * [10] A. Ó Conghaile and A. Dawar.  Game comonads & generalised quantifiers.  In 29th EACSL Annual Conference on Computer Science Logic, CSL, pages 16:1–16:17, 2021.
  * [11] Z. Dvořák.  On recognizing graphs by numbers of homomorphisms.  Journal of Graph Theory, 64(4):330–342, 2010.
  * [12] P. J. Freyd and G. M. Kelly.  Categories of continuous functors, I.  Journal of Pure and Applied Algebra, 2(3):169–191, 1972.
  * [13] E. Grädel, P. G. Kolaitis, L. Libkin, M. Marx, J. Spencer, M. Y. Vardi, Y. Venema, and S. Weinstein.  Finite Model Theory and Its Applications.  Springer, 2007.
  * [14] M. Grohe.  Counting bounded tree depth homomorphisms.  In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 507–520, 2020.
  * [15] J. Isbell.  Some inequalities in hom sets.  Journal of Pure and Applied Algebra, 76(1):87–110, 1991.
  * [16] A. Joyal.  Polyadic spaces and elementary theories.  Notices of the AMS, 18(3):563, 1971.  Preliminary report.
  * [17] S. Kiefer.  The Weisfeiler-Leman algorithm: an exploration of its power.  ACM SIGLOG News, 7(3):5–27, 2020.
  * [18] P. G. Kolaitis and M. Y Vardi.  Conjunctive query containment and constraint satisfaction.  Journal of Computer and System Sciences, 61:302–332, 2000.
  * [19] L. Libkin.  Elements of Finite Model Theory.  Springer, 2004.
  * [20] L. Lovász.  Operations with structures.  Acta Math. Acad. Sci. Hungar., 18:321–328, 1967.
  * [21] L. Lovász.  Direct product in locally finite categories.  Acta Math. Acad. Sci. Hungar., 23:319–322, 1972.
  * [22] S. Mac Lane.  Categories for the working mathematician, volume 5 of Graduate Texts in Mathematics.  Springer-Verlag, New York, second edition, 1998.
  * [23] L. Mančinska and D. E. Roberson.  Quantum isomorphism is equivalent to equality of homomorphism counts from planar graphs.  In 2020 IEEE 61st Annual Symposium on Foundations of Computer Science (FOCS), pages 661–672, 2020.
  * [24] M. Otto.  Bounded Variable Logics and Counting — A Study in Finite Models, volume 9 of Lecture Notes in Logic.  Springer-Verlag, 1997.
  * [25] T. Paine.  A pebbling comonad for finite rank and variable logic, and an application to the equirank-variable homomorphism preservation theorem.  Electronic Notes in Theoretical Computer Science, 352:191–209, 2020\.
  * [26] A. Pultr.  Isomorphism types of objects in categories determined by numbers of morphisms.  Acta Scientiarum Mathematicarum, 35:155–160, 1973.
  * [27] M. V. Ramana, E. R. Scheinerman, and D. Ullman.  Fractional isomorphism of graphs.  Discrete Mathematics, 132:247–265, 1994.
  * [28] E. Riehl.  Factorization systems.  Notes available at http://www.math.jhu.edu/~eriehl/factorization.pdf.
  * [29] B. Rossman.  Homomorphism preservation theorems.  Journal of the ACM, 55, 2008.