Partial order on the set of binary relations (g = f|

On the set of binary relations there exists well known set theoretic partial order ⊆. (Recall that a binary relations is a set of pairs.)

Here I will introduce an another partial order (vertical order) on the set of binary relations. (Analogously can be also introduces horizontal order, and also their intersection/conjunction rectangular order.)

Definition

Let f and g are binary relations. By definition f ⊑ g iff f = g|_{dom f}.

I will call the relation ⊑ vertical order. Below I will prove that ⊑ is a partial order.

Proposition. f ⊑ g iff exists a set K such that f = g|_K.

Proof. Direct implication is obvious. Reverse implication. Let f = g|_K. Then dom f = K ∩ dom g. From this follows f = g|_{dom f}. End of proof.

Reducing vertical order of relations to functions

For any relation p I will denote p* the corresponding function mapping an X to a set of Y. p* is defined by the following two equations:

dom p* = dom p and p*(x) = {y : (x, y) in p} for any x in dom p.

Note that dom f* = dom f.

Proposition. f = g <=> f* = g* for any binary relations f and g.

Proof. Obvious. End of proof.

Proposition. f ⊑ g <=> f* ⊑ g* <=> f* ⊆ g*.

Proof. Obvious. End of proof.

Theorem. f ⊑ g iff ∀x∈dom f : f*(x) = g*(x).

Proof. It follows from the last proposition. End of proof.

Vertical order as a partial order

Proposition. f ⊑ g implies f ⊆ g.

Proof. Obvious. End of proof.

Theorem. ⊑ is a partial order.

Proof. We need to prove reflexivity, transitivity, and antisymmetry of ⊑.

Reflexivity is obvious.

Transitivity. Let f ⊑ g and g ⊑ h. Then f = g|_{dom f} = (h|_{dom g})|_{dom f} = h|_{dom f} because dom f ⊆ dom g. So f ⊑ h.

Antisymmetry. Let f ⊑ g and g ⊑ f. Then f ⊆ g and g ⊆ f. So f = g. End of proof.

I will denote infimum of two elements set {f, g} (where f and g are binary relations), corresponding to the vertical order of, as f ⊓ g.

Theorem. Vertical order is a meet-semilattice (that is has infimum ⊓ of any two binary relations).

Proof. This follows from f ⊑ g <=> f* ⊆ g* and that any two elements of the set of functions, whose images are sets of sets, have the infimum (namely set theoretic intersection). The operation * is a partial order isomorphism and so maps a semilattice to semilattice. Vertical infimum of two binary relations f and g can be so restored by the formula (f ⊓ g)* = f* ∩ g*. End of proof..

Related theorems

About vertical order of binary relations there is an interesting theorem.

Related links

A theorem about vertical order of binary relations.
My category theory research, particularly the theory of dependencies.