Let be an equivariant relation. We show that under a certain assumption on , for every , if there exists a witness such that holds, then there also exists one with small support. We show an application to extending homomorphisms.
The assumption on the set is that it is locally finite, i.e., for every finite support there are only finitely many elements supported by in . Examples of such sets include all orbit-finite sets, but also the set of all finitely supported functions between two orbit-finite sets. See this post for more on locally finite sets.
Lemma. Suppose that is locally finite and is an equivariant relation. Then there is a function such that for every if there exists a witness such that , then there is one with.
Proof. For an element , let denote the minimal size of the support of an element such that holds, and if no such element exists. Then is an equivariant function from to .
For a number , let denote the set of elements of whose support has size at most . By local finiteness of , the set is orbit-finite, for each number . Therefore, the mapping , restricted to , attains a maximal value, let it be denoted by . The function satisfies the condition of the lemma.
An application. In the application below, it does not really matter what an orbit-finite relational structure is. What matters is that their domains are orbit-finite, so the set of (partial) homomorphisms between two such structures is locally finite.
Proposition. Let be two orbit-finite relational structures. Let be a finitely supported, partial homomorphism from to , which extends to some homomorphism . Then the extension can be chosen so that , where is some mapping depending on .
Proof. Apply the lemma to the relation , consisting of pairs where is a partial homomorphism from to and is an extension of to .
The assumption that the domain of is all of is not necessary, is it? Later you say “if a witness exists” anyway… Just say that the function is partial and everything should work.
Fixed – the assumption is not necessary. But doesn’t need to be partial.