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 $x \le y$ , then the least upper bound of $x$ and $y$ is just $y$ :

  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 .in₀ = lub .is-join.l≤join
  is-join→coproduct lub .in₁ = 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 .in₀∘factor = prop!
  is-join→coproduct lub .has-is-coproduct .in₁∘factor = prop!
  is-join→coproduct lub .has-is-coproduct .unique _ _ _ = prop!