where for any is the set , and .
Let us make some observations on a residuated function :
is order preserving.
Suppose in . Then there is some such that . Since , , or , which means , or . But this implies , so that , or . ∎
The in the definition above is unique.
If , then , or . Similarly, , so that . ∎
given by is a well-defined function, with the following properties:
is order preserving,
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. ∎
Actually, the third observation above characterizes being residuated:
If is order preserving, and satisfies through , then is residuated. In fact, such a is unique.
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:
If is residuated, then and .
If and are residuated, so is and .
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.
|Date of creation||2013-03-22 18:53:22|
|Last modified on||2013-03-22 18:53:22|
|Last modified by||CWoo (3771)|