residuated
Let be two posets. Recall that a function is order preserving iff implies . This is equivalent to saying that the preimage of any down set under is a down set.
Definition A function between ordered sets is said to be residuated if the preimage of any principal down set is a principal down set. In other words, for any , there is some such that
where for any is the set , and .
Let us make some observations on a residuated function :
-
1.
is order preserving.
Proof.
Suppose in . Then there is some such that . Since , , or , which means , or . But this implies , so that , or . ∎
-
2.
The in the definition above is unique.
Proof.
If , then , or . Similarly, , so that . ∎
-
3.
given by is a well-defined function, with the following properties:
-
(a)
is order preserving,
-
(b)
,
-
(c)
.
Proof.
is order preserving: if in , then , so that , where and . But implies , or .
: let , , and . Then , which implies as desired.
: pick and let . Then , so that , or , or as a result. ∎
-
(a)
Actually, the third observation above characterizes being residuated:
Proposition 1.
If is order preserving, and satisfies through , then is residuated. In fact, such a is unique.
Proof.
Suppose , and let . We want to show that . First, suppose . Then , which means . But then , and we get , or . Next, suppose . Then , so .
To see uniqueness, suppose is order preserving such that and . Then and . ∎
Definition. Given a residuated function , the unique function defined above is called the residual of , and is denoted by .
For example, given any function , the induced function (by abuse of notation, we use the same notation as original function ), given by is residuated. Its residual is the function , given by .
Here are some properties of residuated functions and their residuals:
-
•
A bijective residuated function is an order isomorphism, and conversely. Furthermore, the residual is residuated, and is its inverse.
-
•
If is residuated, then and .
-
•
If and are residuated, so is and .
-
•
If is residuated, then is a closure map on . Conversely, any closure function can be decomposed as the functional composition of a residuated function and its residual.
Remark. Residuated functions and their residuals are closely related to Galois connections. If is residuated, then forms a Galois connection between and . On the other hand, if is a Galois connection between and , then is residuated, and is . Note that PM defines a Galois connection as a pair of order-preserving maps, where as in Blyth, they are order reversing.
References
- 1 T.S. Blyth, Lattices and Ordered Algebraic Structures, Springer, New York (2005).
- 2 G. Grätzer, General Lattice Theory, 2nd Edition, Birkhäuser (1998)
Title | residuated |
---|---|
Canonical name | Residuated |
Date of creation | 2013-03-22 18:53:22 |
Last modified on | 2013-03-22 18:53:22 |
Owner | CWoo (3771) |
Last modified by | CWoo (3771) |
Numerical id | 12 |
Author | CWoo (3771) |
Entry type | Definition |
Classification | msc 06A99 |
Classification | msc 06A15 |
Defines | residual |