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!