residuated (original) (raw)
Definition A function f:P→Q between ordered sets P,Q is said to be residuated if the preimage of any principal down set is a principal down set. In other words, for any y∈Q, there is some x∈P such that
where f-1(A) for any A⊆Q is the set {a∈X∣f(a)∈A}, and ↓b={c∣c≤b}.
Let us make some observations on a residuated function f:P→Q:
- f is order preserving.
Proof.
Suppose a≤b in P. Then there is some c∈P such that ↓c=f-1(↓f(b)). Since f(b)∈↓f(b), b∈↓c, or b≤c, which means a≤c, or a∈↓c. But this implies a∈f-1(↓f(b)), so that f(a)∈↓f(b), or f(a)≤f(b). ∎
2. 2.
The x in the definition above is unique.
Proof.
If ↓x=↓z, then x∈↓z, or x≤z. Similarly, z≤x, so that x=z. ∎
3. 3.
g:Q→P given by g(y)=x is a well-defined function, with the following properties:
- (a)
g is order preserving, - (b)
1P≤g∘f, - (c)
f∘g≤1Q.
Proof.
g is order preserving: if r≤s in Q, then ↓r⊆↓s, so that ↓u=f-1(↓r)⊆f-1(↓s)=↓v, where u=g(r) and v=g(s). But ↓u⊆↓v implies u≤v, or g(r)≤g(s).
1P≤g∘f: let x∈P, y=f(x), and z=g(y). Then x∈f-1(y)⊆f-1(↓y)=↓z, which implies x≤z=g(f(x)) as desired.
f∘g≤1Q: pick y∈Q and let x=g(y). Then f-1(↓y)=↓x, so that f(x)∈f(↓x)=f(f-1(↓y))=↓y, or f(x)≤y, or f(g(y))=f(x)≤y as a result. ∎
Actually, the third observation above characterizes f being residuated:
Proposition 1.
If f is order preserving, and g satisfies 3(a) through 3(c), then f is residuated. In fact, such a g is unique.
Proof.
Suppose y∈Q, and let x=g(y). We want to show that ↓x=f-1(↓y). First, suppose a∈f-1(↓y). Then f(a)≤y, which means g(f(a))≤g(y)=x. But then a≤g(f(a)), and we get a≤x, or a∈↓x. Next, suppose a≤x=g(y). Then f(a)≤f(x)=f(g(y))≤y, so a∈f-1(f(a))⊆f-1(↓y).
To see uniqueness, suppose h:Q→P is order preserving such that 1P≤h∘f and f∘h≤1Q. Then g=1P∘g≤(h∘f)∘g=h∘(f∘g)≤=h∘1Q=h and h=1P∘h≤(g∘f)∘h=g∘(f∘h)≤g∘1Q=g. ∎
Definition. Given a residuated function f:P→Q, the unique function g:Q→P defined above is called the residual of f, and is denoted by f+.
For example, given any function f:A→B, the induced function f:P(A)→P(B) (by abuse of notation, we use the same notation as original function f), given by f(S)={f(a)∣a∈S} is residuated. Its residual is the function f-1:P(B)→P(A), given by f-1(T)={a∈A∣f(a)∈T}.
Here are some properties of residuated functions and their residuals:
Remark. Residuated functions and their residuals are closely related to Galois connections. If f:P→Q is residuated, then (f,f+) forms a Galois connection between P and Q. On the other hand, if (f,g) is a Galois connection between P and Q, then f:P→Q is residuated, and g:Q→P is f+. Note that PM defines a Galois connection as a pair of order-preserving maps, where as in Blyth, they are order reversing.