module Order.Diagram.Join where

Joins🔗

In the binary case, a least upper bound is called a join. A short computation shows that being a join is precisely being the lub of a family of two elements.

record is-join (P : Poset o ) (a b lub :  P ) : Type (o  ) where
  no-eta-equality
  open Poset P

  field
    l≤join : a  lub
    r≤join : b  lub
    least  : (ub' : Ob)  a  ub'  b  ub'  lub  ub'

record Join (P : Poset o ) (a b :  P ) : Type (o  ) where
  no-eta-equality
  field
    lub :  P 
    has-join : is-join P a b lub
  open is-join has-join public

Has-joins : Poset o   Type (o  )
Has-joins P =  x y  Join P x y

open is-join
  is-join→is-lub :  {a b lub}  is-join P a b lub  is-lub P (if_then a else b) lub
  is-join→is-lub join .fam≤lub true = join .l≤join
  is-join→is-lub join .fam≤lub false = join .r≤join
  is-join→is-lub join .least ub' x = join .least ub' (x true) (x false)

  is-lub→is-join :  {a b lub}  is-lub P (if_then a else b) lub  is-join P a b lub
  is-lub→is-join lub .l≤join = lub .fam≤lub true
  is-lub→is-join lub .r≤join = lub .fam≤lub false
  is-lub→is-join lub .least ub' a<ub' b<ub' = lub .least ub' λ where
    true   a<ub'
    false  b<ub'

An important lemma about joins is that, if then the least upper bound of and is just

  gt→is-join :  {a b}  a  b  is-join P a b b
  gt→is-join a≤b .l≤join = a≤b
  gt→is-join a≤b .r≤join = ≤-refl
  gt→is-join a≤b .least ub' _ b≤ub' = b≤ub'

  gt-join :  {a b l}  a  b  is-join P a b l  b  l
  gt-join a≤b l = join-unique (gt→is-join a≤b) l

As coproducts🔗

Joins are the “thinning” of coproducts; Put another way, when we allow a set of relators, rather than insisting on a propositional relation, the concept of join needs to be refined to that of coproduct.

  open is-coproduct
  open Coproduct

  is-join→coproduct :  {a b lub : Ob}  is-join P a b lub  Coproduct (poset→category P) a b
  is-join→coproduct lub .coapex = _
  is-join→coproduct lub .ι₁ = lub .is-join.l≤join
  is-join→coproduct lub .ι₂ = lub .is-join.r≤join
  is-join→coproduct lub .has-is-coproduct .[_,_] a<q b<q =
    lub .is-join.least _ a<q b<q
  is-join→coproduct lub .has-is-coproduct .[]∘ι₁ = prop!
  is-join→coproduct lub .has-is-coproduct .[]∘ι₂ = prop!
  is-join→coproduct lub .has-is-coproduct .unique _ _ = prop!