The following situation is typical of several tasks of model
construction that arise, e.g., in connection with finite model
properties and finite controllability. Given a finite set of
local templates, i.e., isomorphism types of finite
structures, together with specifications of required and permitted
pairwise overlaps between them, the task is to find finite
global realisations. In the most general sense, a
realisation is a single structure that is the union of a
family \(\mathcal{S}\) of designated substructures, each isomorphic
to one of the given templates and with pairwise overlaps in
accordance with the specification. We think of the overlap
specification as prescribing required and permitted pairwise
overlaps, specified by partial isomorphisms of the form
\(\rho \colon V_s \rightarrow V_t\) between templates \(V_s\) and
\(V_s\), in the following sense:
- for each specified overlap between templates \(V_s\) and
\(V_{t}\), every instance of \(V_s\) in \(\mathcal{S}\) overlaps
with some instance of \(V_{t}\) in \(\mathcal{S}\) as prescribed
by \(\rho\);
- there are no incidental overlaps: any non-trivial intersection
between two substructures in \(\mathcal{S}\) conforms to some
composition \(\rho_n \circ \cdots \circ \rho_1\) of prescribed
overlaps.
We approach the finite realisation task via a generic construction
of reduced products with suitable groupoids. Due to strong
acyclicity properties, these groupoids can serve as structural
backbones in the construction of finite realisations, similar to the
use of free groups in standard constructions of infinite
realisations. The underlying groupoids are constructed in a process
that interleaves model-theoretic amalgamation techniques with
groupoidal analogues of permutation group actions. The proposed
constructions are sufficiently generic and natural as to be
compatible with symmetries of the given specification while also
allowing us to avoid incidental cycles of overlaps up to any
specified finite length. It follows that the resulting finite
realisations can be forced
- to realise certain symmetries built into the specification,
and
- to admit local, size-bounded homomorphisms into any (finite or
infinite) realisation and in particular into the (infinite)
canonical free realisation.
As one remarkable consequence we obtain a new proof of the powerful
finite-model-assertion in a theorem of Herwig and Lascar, which
allows us to lift partial isomorphisms (local symmetries) of finite
structures to automorphisms (global symmetries) within classes
defined by forbidden homomorphisms.
|
