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

Many properties of posetal adjunctions have previously been written down, mostly
in the context of frames. In this module, we collect some of these properties in
the more general case where the lattices in consideration are not necessarily
frames.

\begin{code}

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

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

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

open import Locales.Adjunctions.Properties pt fe
open import Locales.DistributiveLattice.Definition fe pt
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 distributive lattices `K` and `L`.

\begin{code}

module Properties-Of-Posetal-Adjunctions-on-Distributive-Lattices
        (K : DistributiveLattice 𝓀)
        (L : DistributiveLattice π“₯)
       where

 open GaloisConnectionBetween (poset-ofᡈ K) (poset-ofᡈ L)
 open Some-Properties-Of-Posetal-Adjunctions

\end{code}

We denote by `P` and `Q` the underlying posets of distributive lattices `K` and
`L`.

\begin{code}

 P : Poset 𝓀 𝓀
 P = poset-ofᡈ K

 Q : Poset π“₯ π“₯
 Q = poset-ofᡈ L

 open DistributiveLattice K
  using ()
  renaming (𝟎 to 𝟎K; 𝟏 to 𝟏K; _∧_ to _βˆ§β‚–_; _∨_ to _βˆ¨β‚–_)
 open DistributiveLattice L
  using ()
  renaming (𝟎 to 𝟎L; 𝟏 to 𝟏L; _∧_ to _βˆ§β‚—_; _∨_ to _βˆ¨β‚—_)

\end{code}

Right adjoints preserve the top element `𝟏`.

\begin{code}

 right-adjoint-preserves-𝟏 : (𝒻@(f , _) : P ─mβ†’ Q) (β„Š@(g , _) : Q ─mβ†’ P)
                           β†’ (𝒻 ⊣ β„Š) holds
                           β†’ g 𝟏L ＝ 𝟏K
 right-adjoint-preserves-𝟏 𝒻@(f , _) β„Š@(g , _) 𝒢𝒹𝒿 = ≀-is-antisymmetric P † ‑
  where
   † : (g 𝟏L ≀[ poset-ofᡈ K ] 𝟏K) holds
   † = 𝟏ᡈ-is-top K (g 𝟏L)

   ‑ : (𝟏K ≀[ poset-ofᡈ K ] g 𝟏L) holds
   ‑ = adjunction-law₁ (poset-ofᡈ K) (poset-ofᡈ L) 𝒻 β„Š 𝒢𝒹𝒿 (𝟏ᡈ-is-top L (f 𝟏K))

\end{code}

Left adjoints preserve the bottom element `𝟎`.

\begin{code}

 left-adjoint-preserves-𝟎 : (𝒻@(f , _) : P ─mβ†’ Q) (β„Š@(g , _) : Q ─mβ†’ P)
                          β†’ (𝒻 ⊣ β„Š) holds
                          β†’ f 𝟎K ＝ 𝟎L
 left-adjoint-preserves-𝟎 𝒻@(f , _) β„Š@(g , _) 𝒢𝒹𝒿 = ≀-is-antisymmetric Q † ‑
  where
   † : (f 𝟎K ≀[ poset-ofᡈ L ] 𝟎L) holds
   † = adjunction-lawβ‚‚ P Q 𝒻 β„Š 𝒢𝒹𝒿 (𝟎ᡈ-is-bottom K (g 𝟎L))

   ‑ : (𝟎L ≀[ poset-ofᡈ L ] f 𝟎K) holds
   ‑ = 𝟎ᡈ-is-bottom L (f 𝟎K)

\end{code}

Right adjoints preserve binary meets.

\begin{code}

 right-adjoint-preserves-∧ : (𝒻@(f , _) : P ─mβ†’ Q) (β„Š@(g , _) : Q ─mβ†’ P)
                           β†’ (𝒻 ⊣ β„Š) holds
                           β†’ (x y : ∣ Q βˆ£β‚š) β†’ g (x βˆ§β‚— y) ＝ g x βˆ§β‚– g y
 right-adjoint-preserves-∧ 𝒻@(f , μ₁) β„Š@(g , ΞΌβ‚‚) 𝒢𝒹𝒿 x y =
  ≀-is-antisymmetric P † ‑
   where
    † : (g (x βˆ§β‚— y) ≀[ P ] g x βˆ§β‚– g y) holds
    † = ∧-is-greatest K (g x) (g y) (g (x βˆ§β‚— y)) (†₁ , †₂)
     where
      †₁ : (g (x βˆ§β‚— y) ≀[ P ] g x) holds
      †₁ = ΞΌβ‚‚ (x βˆ§β‚— y , x) (∧-is-a-lower-bound₁ L x y)

      †₂ : (g (x βˆ§β‚— y) ≀[ P ] g y) holds
      †₂ = ΞΌβ‚‚ (x βˆ§β‚— y , y) (∧-is-a-lower-boundβ‚‚ L x y)

    ‑ : (g x βˆ§β‚– g y ≀[ P ] g (x βˆ§β‚— y)) holds
    ‑ =
     adjunction-law₁ P Q 𝒻 β„Š 𝒢𝒹𝒿 (∧-is-greatest L x y (f (g x βˆ§β‚– g y)) (‑₁ , ‑₂))
      where
       ‑₁ : (f (g x βˆ§β‚– g y) ≀[ Q ] x) holds
       ‑₁ = adjunction-lawβ‚‚ P Q 𝒻 β„Š 𝒢𝒹𝒿 (∧-is-a-lower-bound₁ K (g x) (g y))

       ‑₂ : (f (g x βˆ§β‚– g y) ≀[ Q ] y) holds
       ‑₂ = adjunction-lawβ‚‚ P Q 𝒻 β„Š 𝒢𝒹𝒿 (∧-is-a-lower-boundβ‚‚ K (g x) (g y))

\end{code}

Left adjoints preserve binary joins.

\begin{code}

 left-adjoint-preserves-∨ : (𝒻@(f , _) : P ─mβ†’ Q) (β„Š@(g , _) : Q ─mβ†’ P)
                          β†’ (𝒻 ⊣ β„Š) holds
                          β†’ (x y : ∣ P βˆ£β‚š) β†’ f (x βˆ¨β‚– y) ＝ f x βˆ¨β‚— f y
 left-adjoint-preserves-∨ 𝒻@(f , μ₁) β„Š@(g , ΞΌβ‚‚) 𝒢𝒹𝒿 x y =
  ≀-is-antisymmetric Q † ‑
   where
    † : (f (x βˆ¨β‚– y) ≀[ Q ] f x βˆ¨β‚— f y) holds
    † =
     adjunction-lawβ‚‚
      P
      Q
      𝒻
      β„Š
      𝒢𝒹𝒿
      (∨-is-least K x y (g (f x βˆ¨β‚— f y)) (†₁ , †₂))
       where
        †₁ : (x ≀[ P ] g (f x βˆ¨β‚— f y)) holds
        †₁ = adjunction-law₁ P Q 𝒻 β„Š 𝒢𝒹𝒿 (∨-is-an-upper-bound₁ L (f x) (f y))

        †₂ : (y ≀[ P ] g (f x βˆ¨β‚— f y)) holds
        †₂ = adjunction-law₁ P Q 𝒻 β„Š 𝒢𝒹𝒿 (∨-is-an-upper-boundβ‚‚ L (f x) (f y))

    ‑ : (f x βˆ¨β‚— f y ≀[ Q ] f (x βˆ¨β‚– y)) holds
    ‑ = ∨-is-least L (f x) (f y) (f (x βˆ¨β‚– y)) (‑₁ , ‑₂)
     where
      ‑₁ : (f x β‰€α΅ˆ[ L ] f (x βˆ¨β‚– y)) holds
      ‑₁ = μ₁ (x , x βˆ¨β‚– y) (∨-is-an-upper-bound₁ K x y)

      ‑₂ : (f y β‰€α΅ˆ[ L ] f (x βˆ¨β‚– y)) holds
      ‑₂ = μ₁ (y , x βˆ¨β‚– y) (∨-is-an-upper-boundβ‚‚ K x y)

\end{code}