 Residuation

This is the Adjunction.Residuation module of the Agda Universal Algebra Library.

{-# OPTIONS --without-K --exact-split --safe #-}

-- Imports from Agda and the Agda Standard Library --------------------------------------
open import Agda.Primitive          using ( _⊔_ ;  Level ; lsuc) renaming ( Set to Type )
open import Function.Base           using ( _on_ ; _∘_ )
open import Relation.Binary.Bundles using ( Poset )
open import Relation.Binary.Core    using ( _Preserves_⟶_ )

-- Imports from the Agda Universal Algebra Library --------------------------------------
open import Relations.Discrete using ( PointWise )

private variable
α ιᵃ ρᵃ β ιᵇ ρᵇ : Level

module _ (A : Poset α ιᵃ ρᵃ)(B : Poset β ιᵇ ρᵇ) where
open Poset
private
_≤A_ = _≤_ A
_≤B_ = _≤_ B

record Residuation : Type (lsuc (α  ρᵃ  β  ρᵇ))  where
field
f     : Carrier A  Carrier B
g     : Carrier B  Carrier A
fhom  : f Preserves _≤A_  _≤B_
ghom  : g Preserves _≤B_  _≤A_
gf≥id :  a  a ≤A g (f a)
fg≤id :  b  f (g b) ≤B b

Basic properties of residual pairs

open Residuation
open Poset

module _ {A : Poset α ιᵃ ρᵃ} {B : Poset β ιᵇ ρᵇ} (R : Residuation A B) where
private
_≤A_ = _≤_ A
_≤B_ = _≤_ B

𝑓 = (R .f)
𝑔 = (R .g)

-- Pointwise equality of unary functions wrt equality on the given poset carrier
-- 1. pointwise equality on B → A
_≈̇A_ = PointWise{α = β}{A = Carrier B} (_≈_ A)
-- 2. pointwise equality on A → B
_≈̇B_ = PointWise{α = α}{A = Carrier A} (_≈_ B)

In a ring R, if x y : R and if x y x = x, then y is called a weak inverse for x. (A ring is called von Neumann regular if every element has a unique weak inverse.)

-- 𝑔 is a weak inverse for 𝑓
weak-inverse : (𝑓  𝑔  𝑓) ≈̇B 𝑓
weak-inverse a = antisym B lt gt
where
lt : 𝑓 (𝑔 (𝑓 a)) ≤B 𝑓 a
lt = fg≤id R (𝑓 a)
gt : 𝑓 a ≤B 𝑓 (𝑔 (𝑓 a))
gt = fhom R (gf≥id R a)

-- 𝑓 is a weak inverse of 𝑔
weak-inverse' : (𝑔  𝑓  𝑔) ≈̇A 𝑔
weak-inverse' b = antisym A lt gt
where
lt : 𝑔 (𝑓 (𝑔 b)) ≤A 𝑔 b
lt = ghom R (fg≤id R b)
gt : 𝑔 b ≤A 𝑔 (𝑓 (𝑔 b))
gt = gf≥id R (𝑔 b)