module Order.Semilattice.Join.NAry where

n-Ary joins🔗

Let be a join semilattice, and let be a finite family of elements of We can compute joins of in via induction on the size of the family.

  ⋃ᶠ :  {n} (f : Fin n   P )   P 
  ⋃ᶠ {0}           f = bot
  ⋃ᶠ {1}           f = f fzero
  ⋃ᶠ {suc (suc n)} f = f fzero  ⋃ᶠ  i  f (fsuc i))

  ⋃ᶠ-inj :  {n} {f : Fin n  Ob}  (i : Fin n)  f i  ⋃ᶠ f
  ⋃ᶠ-inj i with fin-view i
  ⋃ᶠ-inj {1}           .fzero    | zero  = ≤-refl
  ⋃ᶠ-inj {suc (suc n)} .fzero    | zero  = l≤∪
  ⋃ᶠ-inj {suc (suc n)} .(fsuc i) | suc i = ≤-trans (⋃ᶠ-inj i) r≤∪

  ⋃ᶠ-universal
    :  {n} {f : Fin n  Ob} (x : Ob)
     (∀ i  f i  x)  ⋃ᶠ f  x
  ⋃ᶠ-universal {0} x p = ¡
  ⋃ᶠ-universal {1} x p = p fzero
  ⋃ᶠ-universal {suc (suc n)} x p =
    ∪-universal _ (p fzero) (⋃ᶠ-universal x (p  fsuc))

  Finite-lubs :  {n} (f : Fin n  Ob)  Lub P f
  Finite-lubs f .lub              = ⋃ᶠ f
  Finite-lubs f .has-lub .fam≤lub = ⋃ᶠ-inj
  Finite-lubs f .has-lub .least   = ⋃ᶠ-universal

Furthermore, must also have joins of finitely indexed sets. Let be a finitely indexed set with enumeration and let be an family in is a finite family in so it must have a least upper bound. Furthermore, is surjective, so it must reflect the least upper bound.

  ⋃ᶠˢ : Finset  P    P 
  ⋃ᶠˢ []       = bot
  ⋃ᶠˢ (x  xs) = x  ⋃ᶠˢ xs
  ⋃ᶠˢ (∷-dup x xs i) = along i $
    x  x  ⋃ᶠˢ xs ≡⟨ ∪.pulll ∪-idem 
    x  ⋃ᶠˢ xs     
  ⋃ᶠˢ (∷-swap x y xs i) = along i $
    x  y  ⋃ᶠˢ xs ≡⟨ ∪.extendl ∪-comm 
    y  x  ⋃ᶠˢ xs 
  ⋃ᶠˢ (squash x y p q i j) = hlevel 2 (⋃ᶠˢ x) (⋃ᶠˢ y)  i  ⋃ᶠˢ (p i))  i  ⋃ᶠˢ (q i)) i j

  abstract
    ⋃ᶠˢ-inj : {x :  P } (xs : Finset  P )  x  xs  x  ⋃ᶠˢ xs
    ⋃ᶠˢ-inj {x} xs = ∈ᶠˢ-elim  xs _  x  ⋃ᶠˢ xs) l≤∪  q r  ≤-trans r r≤∪) xs

    ⋃ᶠˢ-univ
      : (xs : Finset  P ) {o :  P }
       ((x :  P )  x ∈ᶠˢ xs  x  o)
       ⋃ᶠˢ xs  o
    ⋃ᶠˢ-univ xs {o} = Finset-elim-prop  xs  ((x :  P )  x ∈ᶠˢ xs  x  o)  ⋃ᶠˢ xs  o)
       _  ¡)
       x ih le  ∪-universal o (le x hereₛ) (ih  y w  le y (thereₛ w))))
      xs

    ⋃ᶠˢ-union : (xs ys : Finset  P )  ⋃ᶠˢ (xs <> ys)  (⋃ᶠˢ xs  ⋃ᶠˢ ys)
    ⋃ᶠˢ-union xs ys = ≤-antisym
      (⋃ᶠˢ-univ (xs <> ys) λ x m  case ∈ᶠˢ-union _ xs ys m of λ where
        (inl x)  ≤-trans (⋃ᶠˢ-inj xs x) l≤∪
        (inr x)  ≤-trans (⋃ᶠˢ-inj ys x) r≤∪)
      (∪-universal _
        (⋃ᶠˢ-univ xs λ x m  ⋃ᶠˢ-inj (xs <> ys) (unionl-∈ᶠˢ _ xs ys m))
        (⋃ᶠˢ-univ ys λ x m  ⋃ᶠˢ-inj (xs <> ys) (unionr-∈ᶠˢ _ xs ys m)))
  opaque
    Finitely-indexed-lubs
      :  {ℓᵢ} {I : Type ℓᵢ}
       is-finitely-indexed I
       (f : I  Ob)
       Lub P f
    Finitely-indexed-lubs {I = I} fin-indexed f = case fin-indexed of λ cov 
      cover-reflects-lub (cov .is-cover) (Finite-lubs (f  cov .cover))
      where open Finite-cover

Join semilattice homomorphisms must also preserve finite joins. This follows from another induction on the size of the family we are taking a join over.

module
  _ {o  o' ℓ'} {P : Poset o } {Q : Poset o' ℓ'} {f : Monotone P Q} {Pl Ql}
    (hom : is-join-slat-hom f Pl Ql) where abstract

  private
    module Pₗ = is-join-semilattice Pl
    module Qₗ = is-join-semilattice Ql

  open is-join-slat-hom hom

  pres-⋃ᶠ :  {n} (k : Fin n   P )  f · (⋃ᶠ Pl k)  ⋃ᶠ Ql (apply f  k)
  pres-⋃ᶠ {n = 0} k = pres-bot
  pres-⋃ᶠ {n = 1} k = refl
  pres-⋃ᶠ {n = suc (suc n)} k =
    f · (k fzero Pₗ.∪ ⋃ᶠ Pl (k  fsuc))       ≡⟨ pres-∪ _ _ 
    f · (k fzero) Qₗ.∪ f · (⋃ᶠ Pl (k  fsuc)) ≡⟨ ap₂ Qₗ._∪_ refl (pres-⋃ᶠ (k  fsuc)) 
    ⋃ᶠ Ql (apply f  k)                       

  pres-⋃ᶠˢ :  xs  f · ⋃ᶠˢ Pl xs  ⋃ᶠˢ Ql (map (f ·_) xs)
  pres-⋃ᶠˢ = Finset-elim-prop _ pres-bot  x ih  pres-∪ _ _  ap₂ Qₗ._∪_ refl ih)

  pres-fin-lub
    :  {n} (k : Fin n   P ) (x :  P )
     is-lub P k x
     is-lub Q  x  f · (k x)) (f · x)
  pres-fin-lub k x lub = done where
    rem₁ : x  ⋃ᶠ Pl k
    rem₁ = lub-unique lub (Finite-lubs Pl k .has-lub)

    rem₂ : f · x  ⋃ᶠ Ql (apply f  k)
    rem₂ = ap (apply f) rem₁  pres-⋃ᶠ k

    done : is-lub Q  x  f · k x) (f · x)
    done = subst (is-lub Q (apply f  k)) (sym rem₂) (Finite-lubs Ql _ .has-lub)

  pres-finite-lub
    :  {ℓᵢ} {I : Type ℓᵢ}
     Finite I
     (k : I   P )
     (x :  P )
     is-lub P k x
     is-lub Q  x  f · k x) (f · x)
  pres-finite-lub I-finite k x P-lub = ∥-∥-out! do
    li  I-finite
    let enum = listing→equiv-fin li
    pure $
      cast-is-lub (enum e⁻¹)  _  refl) $
      pres-fin-lub (k  Equiv.from enum) x $
      cast-is-lub enum  x  sym (ap k (Equiv.η enum x))) P-lub

As a corollary, join semilattice homomorphisms must also preserve joins of finitely-indexed sets.

  pres-finitely-indexed-lub
    :  {ℓᵢ} {I : Type ℓᵢ}
     is-finitely-indexed I
     (k : I   P )
     (x :  P )
     is-lub P k x
     is-lub Q  x  f · k x) (f · x)
  pres-finitely-indexed-lub I-fin-indexed k x P-lub = case I-fin-indexed of λ cov 
    cover-reflects-is-lub (Finite-cover.is-cover cov) $
    pres-fin-lub (k  Finite-cover.cover cov) x $
    cover-preserves-is-lub (Finite-cover.is-cover cov) P-lub