# Residuated mapping

In mathematics, the concept of a residuated mapping arises in the theory of partially ordered sets. It refines the concept of a monotone function.
If A, B are posets, a function f: A → B is defined to be monotone if it is order-preserving: that is, if x ≤ y implies f(x) ≤ f(y). This is equivalent to the condition that the preimage under f of every down-set of B is a down-set of A. We define a principal down-set to be one of the form ↓{b} = { b' ∈ B : b' ≤ b }. In general the preimage under f of a principal down-set need not be a principal down-set. If all of them are, f is called residuated.
The notion of residuated map can be generalized to a binary operator (or any higher arity) via component-wise residuation. This approach gives rise to notions of left and right division in a partially ordered magma, additionally endowing it with a quasigroup structure. (One speaks only of residuated algebra for higher arities). A binary (or higher arity) residuated map is usually not residuated as a unary map.

## Definition

If A, B are posets, a function f: A → B is residuated if and only if the preimage under f of every principal down-set of B is a principal down-set of A.

## Consequences

If B is a poset, the set of functions A → B can be ordered by the pointwise order f ≤ g ↔ (∀x ∈ A) f(x) ≤ g(x).
It can be shown that a monotone function f is residuated if and only if there exists a (necessarily unique) monotone function f$^+$: B → A such that f o f$^+$ ≤ id$_B$ and f$^+$ o f ≥ id$_A$, where id is the identity function. The function f$^+$ is the residual of f. A residuated function and its residual form a Galois connection under the (more recent) monotone definition of that concept, and for every (monotone) Galois connection the lower adjoint is residuated with the residual being the upper adjoint. Therefore, the notions of monotone Galois connection and residuated mapping essentially coincide.
Additionally, we have f$^{-1}$(↓{b}) = ↓{f$^+$(b)}.
If B° denotes the dual order (opposite poset) to B then f : A → B is a residuated mapping if and only if there exists an f$^*$ such that f : A → B° and f$^*$: B° → A form a Galois connection under the original antitone definition of this notion.
If f : A → B and g : B → C are residuated mappings, then so is the function composition gf : A → C, with residual (gf)$^+$ = f$^+$g$^+$. The antitone Galois connections do not share this property.
The set of monotone transformations (functions) over a poset is an ordered monoid with the pointwise order, and so is the set of residuated transformations.

## Examples

* The ceiling function $x\mapsto \lceil x\rceil$ from R to Z (with the usual order in each case) is residuated, with residual mapping the natural embedding of Z into R.
* The embedding of Z into R is also residuated. Its residual is the floor function $x\mapsto \lfloor x\rfloor$.

## Residuated binary operators

If • : P × Q → R is a binary map and P, Q, and R are posets, then one may define residuation component-wise for the left and right translations, i.e. multiplication by a fixed element. For an element x in P define $_x$λ(y) = x • y, and for x in Q define λ$_x$(y) = y • x. Then • is said to be residuated if and only if $_x$λ and λ$_x$ are residuated for all x (in P and respectively Q). Left (and respectively right) division are defined by taking the residuals of the left (and respectively right) translations: x\y = ($_x$λ)$^+$(y) and x/y = (λ$_x$)$^+$(y)
For example, every ordered group is residuated, and the division defined by the above coincides with notion of division in a group. A less trivial example is the set Mat$_n$(B) of square matrices over a boolean algebra B, where the matrices are ordered pointwise. The pointwise order endows Mat$_n$(B) with pointwise meets, joins and complements. Matrix multiplication is defined in the usual manner with the "product" being a meet, and the "sum" a join. It can be shown that X\Y = (Y$^t$X ′)′ and X/Y = (X ′Y$^t$)′, where X ′ is the complement of X, and Y $^t$ is the transposed matrix).