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. 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 it is, 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. 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. With A, B posets, 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 f is residuated if and only if there exists a (necessarily unique) monotone function f +: B → A such that f o f + ≤ idB and f + o f ≥ idA, 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 adjoints 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 order dual (opposite poset) to B then f : A → B is a residuated mapping if and only if 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 fg : A → C, with residual (fg) + = g +f +. The antitone Galois connections do not share this property.