module Order.Diagram.Lub where

Least upper boundsπŸ”—

A lub (short for least upper bound) for a family of elements is, as the name implies, a least elemnet among the upper boudns of the Being an upper bound means that we have for all Being the least upper bound means that if we’re given some other satisfying (for each then we have

The same observation about the naming of glbs vs meets applies to lubs, with the binary name being join.

  record is-lub
    {β„“α΅’} {I : Type β„“α΅’} (F : I β†’ Ob) (lub : Ob)
    : Type (o βŠ” β„“ βŠ” β„“α΅’)
    where
    no-eta-equality
    field
      fam≀lub : βˆ€ i β†’ F i ≀ lub
      least   : (ub' : Ob) β†’ (βˆ€ i β†’ F i ≀ ub') β†’ lub ≀ ub'

  record Lub {β„“α΅’} {I : Type β„“α΅’} (F : I β†’ Ob) : Type (o βŠ” β„“ βŠ” β„“α΅’) where
    no-eta-equality
    field
      lub : Ob
      has-lub : is-lub F lub
    open is-lub has-lub public
unquoteDecl H-Level-is-lub = declare-record-hlevel 1 H-Level-is-lub (quote is-lub)

module _ {o β„“} {P : Poset o β„“} where
  open Order.Reasoning P
  open is-lub

  lub-unique
    : βˆ€ {β„“α΅’} {I : Type β„“α΅’} {F : I β†’ Ob} {x y}
    β†’ is-lub P F x β†’ is-lub P F y
    β†’ x ≑ y
  lub-unique {x = x} {y = y} lub lub' = ≀-antisym
    (lub .least y (lub' .fam≀lub))
    (lub' .least x (lub .fam≀lub))

  Lub-is-prop
    : βˆ€ {β„“α΅’} {I : Type β„“α΅’} {F : I β†’ Ob}
    β†’ is-prop (Lub P F)
  Lub-is-prop p q i .Lub.lub =
    lub-unique (Lub.has-lub p) (Lub.has-lub q) i
  Lub-is-prop {F = F} p q i .Lub.has-lub =
    is-prop→pathp
      (Ξ» i β†’ hlevel {T = is-lub _ _ (lub-unique (Lub.has-lub p) (Lub.has-lub q) i)} 1)
      (Lub.has-lub p) (Lub.has-lub q) i

  instance
    H-Level-Lub
      : βˆ€ {β„“α΅’} {I : Type β„“α΅’} {F : I β†’ Ob} {n}
      β†’ H-Level (Lub P F) (suc n)
    H-Level-Lub = prop-instance Lub-is-prop

  lift-is-lub
    : βˆ€ {β„“α΅’ β„“α΅’'} {I : Type β„“α΅’} {F : I β†’ Ob} {lub}
    β†’ is-lub P F lub β†’ is-lub P (F βŠ™ Lift.lower {β„“ = β„“α΅’'}) lub
  lift-is-lub is .fam≀lub (lift ix) = is .fam≀lub ix
  lift-is-lub is .least ub' le = is .least ub' (le βŠ™ lift)

  lift-lub
    : βˆ€ {β„“α΅’ β„“α΅’'} {I : Type β„“α΅’} {F : I β†’ Ob}
    β†’ Lub P F β†’ Lub P (F βŠ™ Lift.lower {β„“ = β„“α΅’'})
  lift-lub lub .Lub.lub = Lub.lub lub
  lift-lub lub .Lub.has-lub = lift-is-lub (Lub.has-lub lub)

  lower-is-lub
    : βˆ€ {β„“α΅’ β„“α΅’'} {I : Type β„“α΅’} {F : I β†’ Ob} {lub}
    β†’ is-lub P (F βŠ™ Lift.lower {β„“ = β„“α΅’'}) lub β†’ is-lub P F lub
  lower-is-lub is .fam≀lub ix = is .fam≀lub (lift ix)
  lower-is-lub is .least ub' le = is .least ub' (le βŠ™ Lift.lower)

  lower-lub
    : βˆ€ {β„“α΅’ β„“α΅’'} {I : Type β„“α΅’} {F : I β†’ Ob}
    β†’ Lub P (F βŠ™ Lift.lower {β„“ = β„“α΅’'}) β†’ Lub P F
  lower-lub lub .Lub.lub = Lub.lub lub
  lower-lub lub .Lub.has-lub = lower-is-lub (Lub.has-lub lub)
  module _
    {β„“α΅’ β„“α΅’'} {Ix : Type β„“α΅’} {Im : Type β„“α΅’'}
    {f : Ix β†’ Im}
    {F : Im β†’ Ob}
    (surj : is-surjective f)
    where
      cover-preserves-is-lub : βˆ€ {lub} β†’ is-lub P F lub β†’ is-lub P (F βŠ™ f) lub
      cover-preserves-is-lub l .fam≀lub x = l .fam≀lub (f x)
      cover-preserves-is-lub l .least   ub' le = l .least ub' Ξ» i β†’ βˆ₯-βˆ₯-out! do
        (i' , p) ← surj i
        pure (≀-trans (≀-refl' (ap F (sym p))) (le i'))

      cover-preserves-lub : Lub P F β†’ Lub P (F βŠ™ f)
      cover-preserves-lub l .Lub.lub = _
      cover-preserves-lub l .Lub.has-lub = cover-preserves-is-lub (l .Lub.has-lub)

      cover-reflects-is-lub : βˆ€ {lub} β†’ is-lub P (F βŠ™ f) lub β†’ is-lub P F lub
      cover-reflects-is-lub l .fam≀lub x = βˆ₯-βˆ₯-out! do
        (y , p) ← surj x
        pure (≀-trans (≀-refl' (ap F (sym p))) (l .fam≀lub y))
      cover-reflects-is-lub l .least ub' le = l .least ub' Ξ» i β†’ le (f i)

      cover-reflects-lub : Lub P (F βŠ™ f) β†’ Lub P F
      cover-reflects-lub l .Lub.lub     = _
      cover-reflects-lub l .Lub.has-lub = cover-reflects-is-lub (l .Lub.has-lub)

  cast-is-lub
    : βˆ€ {β„“α΅’ β„“α΅’'} {I : Type β„“α΅’} {I' : Type β„“α΅’'} {F : I β†’ Ob} {G : I' β†’ Ob} {lub}
    β†’ (e : I ≃ I')
    β†’ (βˆ€ i β†’ F i ≑ G (Equiv.to e i))
    β†’ is-lub P F lub
    β†’ is-lub P G lub
  cast-is-lub {G = G} e p has-lub .fam≀lub i' =
    ≀-trans
      (≀-refl' (sym (p (Equiv.from e i') βˆ™ ap G (Equiv.Ξ΅ e i'))))
      (has-lub .fam≀lub (Equiv.from e i'))
  cast-is-lub e p has-lub .least ub G≀ub =
    has-lub .least ub (Ξ» i β†’ ≀-trans (≀-refl' (p i)) (G≀ub (Equiv.to e i)))

  cast-is-lubαΆ 
    : βˆ€ {β„“α΅’} {I : Type β„“α΅’} {F G : I β†’ Ob} {lub}
    β†’ (βˆ€ i β†’ F i ≑ G i)
    β†’ is-lub P F lub
    β†’ is-lub P G lub
  cast-is-lubαΆ  {lub = lub} p has-lub = cast-is-lub (_ , id-equiv) p has-lub

Let be a family. If there is some such that for all then is the least upper bound of

  fam-bound→is-lub
    : βˆ€ {β„“α΅’} {I : Type β„“α΅’} {F : I β†’ Ob}
    β†’ (i : I) β†’ (βˆ€ j β†’ F j ≀ F i)
    β†’ is-lub P F (F i)
  fam-boundβ†’is-lub i ge .fam≀lub = ge
  fam-bound→is-lub i ge .least y le = le i

If is the least upper bound of a constant family, then must be equal to every member of the family.

  lub-of-const-fam
    : βˆ€ {β„“α΅’} {I : Type β„“α΅’} {F : I β†’ Ob} {x}
    β†’ (βˆ€ i j β†’ F i ≑ F j)
    β†’ is-lub P F x
    β†’ βˆ€ i β†’ F i ≑ x
  lub-of-const-fam {F = F} is-const x-lub i =
    ≀-antisym
      (fam≀lub x-lub i)
      (least x-lub (F i) Ξ» j β†’ ≀-refl' (sym (is-const i j)))

Furthermore, if is a constant family and is merely inhabited, then has a least upper bound.

  const-inhabited-fam→is-lub
    : βˆ€ {β„“α΅’} {I : Type β„“α΅’} {F : I β†’ Ob} {x}
    β†’ (βˆ€ i β†’ F i ≑ x)
    β†’ βˆ₯ I βˆ₯
    β†’ is-lub P F x
  const-inhabited-fam→is-lub {I = I} {F = F} {x = x} is-const =
    rec! mk-is-lub where
      mk-is-lub : I β†’ is-lub P F x
      mk-is-lub i .is-lub.fam≀lub j = ≀-refl' (is-const j)
      mk-is-lub i .is-lub.least y le =
        x   =˘⟨ is-const i ⟩=˘
        F i β‰€βŸ¨ le i βŸ©β‰€
        y β‰€βˆŽ

  const-inhabited-fam→lub
    : βˆ€ {β„“α΅’} {I : Type β„“α΅’} {F : I β†’ Ob}
    β†’ (βˆ€ i j β†’ F i ≑ F j)
    β†’ βˆ₯ I βˆ₯
    β†’ Lub P F
  const-inhabited-fam→lub {I = I} {F = F} is-const =
    rec! mk-lub where
      mk-lub : I β†’ Lub P F
      mk-lub i .Lub.lub = F i
      mk-lub i .Lub.has-lub =
        const-inhabited-fam→is-lub (λ j → is-const j i) (inc i)