Dependencies

Let \( s : \operatorname {\mathsf{Set}}\tau \). An orbit restriction for \( s \) (over some type \( \sigma \)) consists of a set \( t : \operatorname {\mathsf{Set}}\tau \) disjoint from \( s \), a function \( f : \tau \to \sigma \), and a permutation \( \pi : \sigma \simeq \sigma \), such that for each \( u : \sigma \), the set \( t \cap f^{-1}(u) \) has cardinality at least \( \max (\aleph _0, \# s, \# d) \).

An orbit restriction encapsulates information about how orbits should be completed.

• \( t \) is the sandbox, the set inside which all added items must reside.

• \( f \) is a categorisation function, placing each value \( x : \tau \) into a category \( u : \sigma \).

• \( \pi \) is a permutation of categories. If \( x \) has category \( u \), then anything that \( x \) is mapped to should have category \( \pi (u) \).

Let \( R : \sigma \to \tau \to \mathsf{Prop}\). We define

• the image of \( R \) to be the set \( \operatorname {\mathsf{im}}R = \{ y : \tau \mid \exists x : \sigma ,\, x \mathrel {R} y \} \);

• the coimage of \( R \) to be the set \( \operatorname {\mathsf{coim}}R = \{ x : \sigma \mid \exists y : \tau ,\, x \mathrel {R} y \} \) (note that this is not the same as the category-theoretic coimage of a morphism);

• the field of \( R \) to be the set \( \operatorname {\mathsf{field}}R = \operatorname {\mathsf{coim}}R \cup \operatorname {\mathsf{im}}R \);

• the image of \( R \) on \( s : \operatorname {\mathsf{Set}}\sigma \) to be the set \( \operatorname {\mathsf{im}}R|_s = \{ y : \tau \mid \exists x \in s,\, x \mathrel {R} y \} \);

• the coimage of \( R \) on \( t : \operatorname {\mathsf{Set}}\tau \) to be the set \( \operatorname {\mathsf{coim}}R|_t = \{ x : \sigma \mid \exists y \in t,\, x \mathrel {R} y \} \);

• the converse of \( R \) to be the relation \( R^{-1} : \tau \to \sigma \to \mathsf{Prop}\) such that \( y \mathrel {R^{-1}} x \) if and only if \( x \mathrel {R} y \);

• if \( S : \tau \to \upsilon \to \mathsf{Prop}\), the composition \( S \circ R : \sigma \to \upsilon \to \mathsf{Prop}\) is the relation given by \( x \mathrel {(S\circ R)} z \) if and only if there is \( y : \tau \) such that \( x \mathrel {R} y \) and \( y \mathrel {S} z \);

• for a natural number \( n \), the \( n \)th power of \( R : \tau \to \tau \to \mathsf{Prop}\) is defined by \( R^{n+1} = R \circ R^n \) and \( R^0 \) is the identity relation on \( \operatorname {\mathsf{coim}}R \);

• for an integer \( n \), the \( n \)th power of \( R : \tau \to \tau \to \mathsf{Prop}\) is defined by \( R^{(n : \mathbb Z)} = R^n \) and \( R^{-(n : \mathbb Z)} = (R^n)^{-1} \) for \( n : \mathbb N \). ¹

We say that \( R \) is

• injective, if \( s_1 \mathrel {R} t, s_2 \mathrel {R} t \) imply \( s_1 = s_2 \);

• surjective, if for every \( t : \tau \), there is some \( s : \sigma \) such that \( s \mathrel {R} t \);

• coinjective, if \( s \mathrel {R} t_1, s \mathrel {R} t_2 \) imply \( t_1 = t_2 \);

• cosurjective, if for every \( s : \sigma \), there is some \( t : \tau \) such that \( s \mathrel {R} t \);

• functional, if \( R \) is coinjective and cosurjective, or equivalently, for every \( s : \sigma \) there is exactly one \( t : \tau \) such that \( s \mathrel {R} t \);

• cofunctional, if \( R \) is injective and surjective, or equivalently, for every \( t : \tau \) there is exactly one \( s : \sigma \) such that \( s \mathrel {R} t \);

• one-to-one, if \( R \) is injective and coinjective;

• bijective, if \( R \) is functional and cofunctional;

• permutative, if \( R : \tau \to \tau \to \mathsf{Prop}\) is one-to-one and has equal image and coimage.

We also define the graph of a function \( f : \sigma \to \tau \) to be the functional relation \( R : \sigma \to \tau \to \mathsf{Prop}\) given by \( (x, y) \in R \) if and only if \( f(x) = y \). Most of these definitions are from https://www.kylem.net/math/relations.html, and most of these are in mathlib under Mathlib.Logic.Relator.

Let \( \# \mu \) be a strong limit cardinal. Then there are precisely \( \# \mu \)-many subsets of \( \mu \) of size strictly less than \( \operatorname {\mathsf{cof}}(\operatorname {\mathsf{ord}}(\# \mu )) \).

Let \( R : \tau \to \tau \to \mathsf{Prop}\) be a one-to-one relation. Let \( s : \operatorname {\mathsf{Set}}\tau \) be an infinite set such that \( \# \operatorname {\mathsf{field}}R \leq \# s \), and \( \operatorname {\mathsf{field}}R \) and \( s \) are disjoint. Then there is a permutative relation \( S \) such that \( R \leq S \) and \( \operatorname {\mathsf{coim}}S \subseteq \operatorname {\mathsf{field}}R \cup s \).

Let \( R : \tau \to \tau \to \mathsf{Prop}\) be a one-to-one relation, and let \( (t, f, \pi ) \) be an orbit restriction for \( \operatorname {\mathsf{field}}R \) over some type \( \sigma \). Then there is a permutative relation \( T \) such that

• \( \operatorname {\mathsf{coim}}T \subseteq \operatorname {\mathsf{field}}R \cup t \);

• \( \# \operatorname {\mathsf{coim}}T \leq \max (\aleph _0, \# \operatorname {\mathsf{coim}}R) \);

• \( R \leq T \); and

• if \( (x, y) \in T \), then \( (x, y) \in R \vee f(y) = \pi (f(x)) \).

1. \( R : \tau \to \tau \to \mathsf{Prop}\) is permutative if and only if it is one-to-one and for all \( x : \tau \), there exists \( y \) such that \( x \mathrel {R} y \) if and only if there exists \( y \) such that \( y \mathrel {R} x \).

2. If \( R, S : \tau \to \tau \to \mathsf{Prop}\) are permutative and \( \operatorname {\mathsf{coim}}R \cap \operatorname {\mathsf{coim}}S = \emptyset \), then \( R \sqcup S \) is permutative and has coimage \( \operatorname {\mathsf{coim}}R \cup \operatorname {\mathsf{coim}}S \).

3. If \( R, S : \tau \to \tau \to \mathsf{Prop}\) are permutative and \( \operatorname {\mathsf{coim}}R = \operatorname {\mathsf{coim}}S \), then \( R \circ S \) is permutative and has coimage equal to that of \( R \) and \( S \).

4. If \( R \) is permutative, then \( \operatorname {\mathsf{coim}}R^n = \operatorname {\mathsf{coim}}R = \operatorname {\mathsf{im}}R = \operatorname {\mathsf{im}}R^n \) for any natural number or integer \( n \).

5. If \( R \) is permutative and \( s_1, s_2 \subseteq \operatorname {\mathsf{coim}}R \), then the image of \( R \) on \( s_1 \) is equal to \( s_2 \) if and only if the coimage of \( R \) on \( s_2 \) is equal to \( s_1 \).