Commuting squares of Galois connections between large posets

Content created by Egbert Rijke.

Created on 2023-11-24.

module order-theory.commuting-squares-of-galois-connections-large-posets where

Imports
open import foundation.universe-levels

open import order-theory.commuting-squares-of-order-preserving-maps-large-posets
open import order-theory.galois-connections-large-posets
open import order-theory.large-posets


Idea

Consider a diagram of Galois connections

           LI
------->
P     ⊥    U
|  <-------
| ∧   UI   | ∧
| |        | |
LF | |     LG | |
|⊣| UF     |⊣| UG
| |        | |
∨ |   LJ   ∨ |
------->  |
Q     ⊥    V.
<-------
UJ


between large posets. We say that the diagram commutes if there is a similarity LJ ∘ LF ≈ LG ∘ LI. This condition is equivalent the condition that there is a similarity UF ∘ UJ ≈ UI ∘ UG.

Definitions

Commuting squares of Galois connections

module _
{αP αQ αU αV γF γG γI γJ δF δG δI δJ : Level → Level}
{βP βQ βU βV : Level → Level → Level}
(P : Large-Poset αP βP)
(Q : Large-Poset αQ βQ)
(U : Large-Poset αU βU)
(V : Large-Poset αV βV)
(I : galois-connection-Large-Poset γI δI P U)
(F : galois-connection-Large-Poset γF δF P Q)
(G : galois-connection-Large-Poset γG δG U V)
(J : galois-connection-Large-Poset γJ δJ Q V)
where

lower-coherence-square-galois-connection-Large-Poset : UUω
lower-coherence-square-galois-connection-Large-Poset =
lower-sim-galois-connection-Large-Poset P V
( comp-galois-connection-Large-Poset P Q V J F)
( comp-galois-connection-Large-Poset P U V G I)

upper-coherence-square-galois-connection-Large-Poset : UUω
upper-coherence-square-galois-connection-Large-Poset =
upper-sim-galois-connection-Large-Poset P V
( comp-galois-connection-Large-Poset P U V G I)
( comp-galois-connection-Large-Poset P Q V J F)


Properties

A commuting square of lower adjoints of galois connections induces a commuting square of upper adjoints and vice versa

module _
{αP αQ αU αV γF γG γI γJ δF δG δI δJ : Level → Level}
{βP βQ βU βV : Level → Level → Level}
(P : Large-Poset αP βP)
(Q : Large-Poset αQ βQ)
(U : Large-Poset αU βU)
(V : Large-Poset αV βV)
(I : galois-connection-Large-Poset γI δI P U)
(F : galois-connection-Large-Poset γF δF P Q)
(G : galois-connection-Large-Poset γG δG U V)
(J : galois-connection-Large-Poset γJ δJ Q V)
where

lower-coherence-square-upper-coherence-square-galois-connection-Large-Poset :
upper-coherence-square-galois-connection-Large-Poset
P Q U V I F G J →
lower-coherence-square-galois-connection-Large-Poset
P Q U V I F G J
lower-coherence-square-upper-coherence-square-galois-connection-Large-Poset =
lower-sim-upper-sim-galois-connection-Large-Poset P V
( comp-galois-connection-Large-Poset P Q V J F)
( comp-galois-connection-Large-Poset P U V G I)

upper-coherence-square-lower-coherence-square-galois-connection-Large-Poset :
lower-coherence-square-galois-connection-Large-Poset
P Q U V I F G J →
upper-coherence-square-galois-connection-Large-Poset
P Q U V I F G J
upper-coherence-square-lower-coherence-square-galois-connection-Large-Poset =
upper-sim-lower-sim-galois-connection-Large-Poset P V
( comp-galois-connection-Large-Poset P Q V J F)
( comp-galois-connection-Large-Poset P U V G I)