↑ Top


Residuation

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

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

module Base.Adjunction.Residuation where

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

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

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

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

 record Residuation : Type (suc (α  ρᵃ  β  ρᵇ))  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)

← Base.Adjunction.Galois Base.Categories →