module Order.Instances.Lower.Cocompletion where

Lower sets as cocompletionsπŸ”—

In this module we prove the universal property of the poset of lower sets of a poset is the free cocomplete poset on meaning that every map into a cocomplete poset admits a unique cocontinuous extension

As an intermediate step, we establish the posetal analogue of the coyoneda lemma, saying that every lower set is the join of all for

module ↓Coyoneda {o β„“} (P : Poset o β„“) (Ls : Lower-set P) where
  private
    module P  = Order.Reasoning P
    module P↓ = Order.Reasoning (Lower-sets P)

  diagram : βˆ«β‚š Ls β†’ Lower-set P
  diagram (i , i∈P) = ↓ P i

This result is much easier to establish in the posetal case than it is in the case of proper categories, so we do not comment on the construction too much. The curious reader is invited to load this file in Agda and play with it themselves!

  lower-set-is-lub : is-lub (Lower-sets P) diagram Ls
  lower-set-is-lub .is-lub.fam≀lub (j , j∈Ls) i β–‘i≀j =
    Ls .pres-≀ (out! β–‘i≀j) j∈Ls
  lower-set-is-lub .is-lub.least ub' fam≀ub' i i∈Ls =
    fam≀ub' (i , i∈Ls) i (inc (P.≀-refl))

A quick note on notation: The result saying that is the lub of the down-sets of its elements is called lower-set-∫. The integral symbol is because (in the categorical case) we can think of the coyoneda lemma as saying that presheaves are computed as certain coends.

  lower-set-∫ : Ls ≑ Lub.lub (Lower-sets-cocomplete P diagram)
  lower-set-∫ = lub-unique (lower-set-is-lub)
    (Lub.has-lub $ Lower-sets-cocomplete P diagram)

The cocontinuous extension sends a lower set to the join (in of which is expressed familially as the composition

It is readily computed that this procedure results in a monotone map.

  Lan↓ : Monotone (Lower-sets A) B
  Lan↓ .hom S = ⋃ {I = Ξ£[ i ∈ A ] (i ∈ S)} (Ξ» i β†’ f # (i .fst))
  Lan↓ .pres-≀ {S} {T} SβŠ†T = B-cocomplete.⋃-universal _ Ξ» where
    (i , i∈S) β†’ B-cocomplete.⋃-inj (i , SβŠ†T i i∈S)

A further short computation reveals that the least upper bound of all elements under is Put like that, it seems trivial, but it says that our cocontinuous extension commutes with the β€œunit map”

  Lan↓-commutes : βˆ€ x β†’ Lan↓ # (↓ A x) ≑ f # x
  Lan↓-commutes x = B.≀-antisym
    (B-cocomplete.⋃-universal _ (Ξ» { (i , β–‘i≀x) β†’ f .pres-≀ (out! β–‘i≀x) }))
    (B-cocomplete.⋃-inj (x , inc A.≀-refl))

A short argument whose essence is the commutativity of joins with joins establishes that the cocontinuous extension does live up to its name:

  Lan↓-cocontinuous
    : βˆ€ {I : Type o} (F : I β†’ Lower-set A)
    β†’ Lan↓ # Lub.lub (Lower-sets-cocomplete A F) ≑ ⋃ (Ξ» i β†’ Lan↓ # (F i))
  Lan↓-cocontinuous F = B.≀-antisym
    (B-cocomplete.⋃-universal _ Ξ» where
      (i , iβˆˆβ‹ƒF) β†’
        β–‘-rec! (Ξ» { (j , i∈Fj) β†’
          B.≀-trans (B-cocomplete.⋃-inj (i , i∈Fj)) (B-cocomplete.⋃-inj j)
        }) iβˆˆβ‹ƒF)
    (B-cocomplete.⋃-universal _ Ξ» i β†’
     B-cocomplete.⋃-universal _ Ξ» where
       (j , j∈Fi) β†’ B-cocomplete.⋃-inj (j , inc (i , j∈Fi)))

And the coyoneda lemma comes in to show that the cocontinuous extension is unique, for if is any other cocontinuous map sending to then expressing a lower set as

reveals that must agree with

  Lan↓-unique
    : (f~ : ⌞ Monotone (Lower-sets A) B ⌟)
    β†’ ( βˆ€ {I : Type o} (F : I β†’ Lower-set A)
      β†’ f~ # Lub.lub (Lower-sets-cocomplete A F) ≑ ⋃ (Ξ» i β†’ f~ # (F i)) )
    β†’ (βˆ€ x β†’ f~ # (↓ A x) ≑ f # x)
    β†’ f~ ≑ Lan↓
  Lan↓-unique f~ f~-cocont f~-comm = ext Ξ» i β†’
    f~ # i                                                           β‰‘βŸ¨ ap# f~ (↓Coyoneda.lower-set-∫ A i) βŸ©β‰‘
    f~ # Lub.lub (Lower-sets-cocomplete A (↓Coyoneda.diagram A i))   β‰‘βŸ¨ f~-cocont (↓Coyoneda.diagram A i) βŸ©β‰‘
    ⋃ (Ξ» j β†’ f~ # (↓Coyoneda.diagram A i j))                         β‰‘βŸ¨ ap ⋃ (funext Ξ» j β†’ f~-comm (j .fst) βˆ™ sym (Lan↓-commutes (j .fst))) βŸ©β‰‘
    ⋃ (Ξ» j β†’ Lan↓ # (↓ A (j .fst)))                                  β‰‘Λ˜βŸ¨ Lan↓-cocontinuous (↓Coyoneda.diagram A i) βŸ©β‰‘Λ˜
    Lan↓ # Lub.lub (Lower-sets-cocomplete A (↓Coyoneda.diagram A i)) β‰‘Λ˜βŸ¨ ap# Lan↓ (↓Coyoneda.lower-set-∫ A i) βŸ©β‰‘Λ˜
    Lan↓ # i                                                         ∎