---
title:        Properties of posetal adjunctions
author:       Ayberk Tosun
date-started: 2024-05-20
---

Many facts about posetal adjunctions have previously been recorded in modules

  - `Locales.GaloisConnection`, and
  - `Locales.AdjointFunctorTheoremForFrames`.

This is a new module in which I will be factoring out some of these facts and
organizing them in a more careful way. One motivation for this is that some of
these constructions and theorems have been formulated for frames, even though
they apply to the much more general setting of arbitrary posets. Now that I want
to apply them to distributive lattices, generalizing them has become necessary.

\begin{code}

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

open import MLTT.Spartan
open import UF.FunExt
open import UF.PropTrunc

module Locales.Adjunctions.Properties
        (pt : propositional-truncations-exist)
        (fe : Fun-Ext) where

open import Locales.ContinuousMap.FrameHomomorphism-Properties pt fe
open import Locales.Frame pt fe
open import Locales.GaloisConnection pt fe
open import UF.Logic
open import UF.SubtypeClassifier

open AllCombinators pt fe

\end{code}

We work in a module parameterized by two posets `P` and `Q`.

\begin{code}

module Some-Properties-Of-Posetal-Adjunctions
        (P : Poset 𝓀  π“₯)
        (Q : Poset 𝓀' π“₯')
       where

 open GaloisConnectionBetween P Q

\end{code}

The two adjunction laws.

\begin{code}

 adjunction-law₁ : (𝒻@(f , _) : P ─mβ†’ Q) (β„Š@(g , _) : Q ─mβ†’ P)
                  β†’ (𝒻 ⊣ β„Š) holds
                 β†’ {x : ∣ P βˆ£β‚š} {y : ∣ Q βˆ£β‚š}
                 β†’ (f x ≀[ Q ] y β‡’ x ≀[ P ] g y) holds
 adjunction-law₁ 𝒻 β„Š adj {x} {y} = pr₁ (adj x y)

 adjunction-lawβ‚‚ : (𝒻@(f , _) : P ─mβ†’ Q) (β„Š@(g , _) : Q ─mβ†’ P)
                 β†’ (𝒻 ⊣ β„Š) holds
                 β†’ {x : ∣ P βˆ£β‚š} {y : ∣ Q βˆ£β‚š}
                 β†’ (x ≀[ P ] g y β‡’ f x ≀[ Q ] y) holds
 adjunction-lawβ‚‚ 𝒻 β„Š adj {x} {y} = prβ‚‚ (adj x y)

\end{code}

Monotone equivalences are adjoints.

\begin{code}

 monotone-equivalences-are-adjoint : (sβ‚˜@(s , _) : P ─mβ†’ Q) (rβ‚˜@(r , _) : Q ─mβ†’ P)
                                   β†’ s ∘ r ∼ id
                                   β†’ r ∘ s ∼ id
                                   β†’ (sβ‚˜ ⊣ rβ‚˜) holds
 monotone-equivalences-are-adjoint (s , 𝓂₁) (r , 𝓂₂) Ο† ψ x y = † , ‑
  where
   open PosetReasoning Q

   † : (s x ≀[ Q ] y β‡’ x ≀[ P ] r y) holds
   † p = sections-are-order-embeddings P Q s r 𝓂₂ ψ β€»
    where
     β…  = p
     β…‘ = Ο† y ⁻¹

     β€» : (s x ≀[ Q ] s (r y)) holds
     β€» = s x      β‰€βŸ¨ β…  ⟩
         y        ＝⟨ β…‘ βŸ©β‚š
         s (r y)  β– 

   ‑ : (x ≀[ P ] r y β‡’ s x ≀[ Q ] y) holds
   ‑ p = s x      β‰€βŸ¨ β…  ⟩
         s (r y)  ＝⟨ β…‘ βŸ©β‚š
         y        β– 
          where
           β…  = 𝓂₁ (x , r y) p
           β…‘ = Ο† y

\end{code}