Commuting squares of Galois connections between large posets

Content created by Egbert Rijke.

Created on 2023-11-24.
Last modified 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)

Recent changes