This theorem has appeared wrong. There is a counterexample (formulated in this news message). It seems that I’ve mistaken in the following phrase “what accordingly noted above is equivalent to gg-1 = fg-1.” There seems no thing noted above accordingly which would be gg-1 = fg-1.
The counterexample:
f = N2; g = {(n,m) in N2 | n less or equal than m} where N is the set of natural numbers.
In this example gg-1 = fg-1 = N2 but not g = f|dom g because f|dom g = f.
Theorem. Let f and g are binary relations. Then the following statements are equivalent:
- g = f|dom g.
- Exists a set K such that g = f|K.
- gg-1 = fg-1 and g is a subset of f.
- gg-1 = gf-1 and g is a subset of f.
- gg-1 = fg-1 and dom g is a subset of dom f.
- gg-1 = gf-1 and dom g is a subset of dom f.
An other, a little less convenient for usage but much easier to remember (mnemonic), equivalent form of this theorem is:
Theorem (mnemonic form). Given that f and g are binary relations and dom g is a subset of dom f, right multiplying
(composing) both sides of the equation g = f|dom g with g-1 produces a formula equivalent to this equation.
I have stated this theorem as a conjecture in this weblog post. Now I have proved it. (The proof is below.)
Note that qp denotes the composition of binary relations p and q.
Lemma
First we will prove the following lemma:
Lemma. If gg-1 = fg-1 and dom g is a subset of dom f then f|dom g = g for any binary relations f and g.
Proof. Let gg-1 = fg-1.
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.
I will denote L the multivalued function (relation) which maps a set to its elements (that is the reverse of set membership relation). Obviously p = Lp* and p = q <=> p* = q* for any relations p and q.
Our equation can be equivalently rewritten as Lg*(Lg*)-1 = Lf*(Lg*)-1; Lg*g*-1L-1 = Lf*g*-1L-1; what accordingly noted above is equivalent to g*g*-1 = f*g*-1.
By well known properties of monovalued functions, we have g*g*-1 = Iim g* (Iim g* denotes the identity relation on the set im g*); so f*g*-1 = Iim g*, that is for any y in im g* we have f*g*-1y = y.
So for any x in dom g* we have f*g*-1g*x = g*x. Because g*-1g*x contains x and x in dom f* (dom f* is a superset of dom g*), we have f*x = g*x.
So f*|dom g* = g* what is the same as f|dom g = g. End of proof.
Proof of the main theorem
Now we can easily prove the main theorem. First we will prove its mnemonic form (repeated below):
Theorem (mnemonic form). Given that f and g are binary relations and dom g is a subset of dom f, right multiplying both sides of the equation g = f|dom g with g-1 produces a formula equivalent to this equation.
Proof of the main theorem (mnemonic form).
Multiplying both sides of the equation g = f|dom g with g-1 produces the formula gg-1 = fg-1. We need to prove that this formula is equivalent to g = f|dom g (under the condition that dom g is a subset of dom f).
Direct implication is obvious. Reverse implication is already proved in the lemma (that dom g is a subset of dom f is taken into account). End of proof.
Now let reprise the full form of the main theorem again and prove it:
Theorem. Let f and g are binary relations. Then the following statements are equivalent:
- g = f|dom g.
- Exists a set K such that g = f|K.
- gg-1 = fg-1 and g is a subset of f.
- gg-1 = gf-1 and g is a subset of f.
- gg-1 = fg-1 and dom g is a subset of dom f.
- gg-1 = gf-1 and dom g is a subset of dom f.
Proof of the main theorem (full form).
Equivalences (3)<=>(4) and (5)<=>(6) can be proved by inverting the formulas taking in account that (qp)-1 = p-1q-1 for any binary relations p and q.
Implications (3)=>(5) and (4)=>(6) are obvious.
(5)=>(1) is exactly the lemma proved above.
(1)=>(3) is obvious (right multiply both sides of the equality (1) with g-1).
(1)=>(2) is obvious. (Take K = dom g.)
To prove (2)=>(1) let assume that g = f|K. Then dom g is intersection of dom f and the set K; from this follows g = f|dom g.
From proved implications follows that all six statements are equivalent. End of proof.
Name and authorship of the theorem
I do not remember that I would have seen this theorem anywhere else. Maybe I am the first who found this theorem (in the start of November 2005)? If so let this theorem be called the theorem of Porton about limiting binary relations or simply the theorem about limiting binary relations.
Related links
- Homepage of this theorem.
- Definition of vertical order of binary relations (a partial order).
- This theorem is used in my category theory research, particularly the theory of dependencies.