open import Cat.Prelude

open import Order.Instances.Pointwise
open import Order.Diagram.Glb
open import Order.Diagram.Lub
open import Order.Base

module Order.Instances.Pointwise.Diagrams where

Pointwise joins and meetsπŸ”—

This module establishes that joins and meets are a pointwise construction, in the following sense: Suppose that fif_i, gig_i, and hih_i are families of elements Iβ†’PI \to P with (P,≀)(P, \le) a poset, such that, for all ii, we have hi=fi∧gih_i = f_i \land g_i1, then h=f∧gh = f \land g when Iβ†’PI \to P is given the pointwise ordering.

module
  _ {β„“β‚’ β„“α΅£ β„“α΅’} {I : Type β„“α΅’} (P : Poset β„“β‚’ β„“α΅£)
    (f g h : I β†’ ⌞ P ⌟)
  where

  is-meet-pointwise
    : (βˆ€ i β†’ is-meet P (f i) (g i) (h i))
    β†’ is-meet (Pointwise I P) f g h
  is-meet-pointwise pwise .is-meet.meet≀l i = pwise i .is-meet.meet≀l
  is-meet-pointwise pwise .is-meet.meet≀r i = pwise i .is-meet.meet≀r
  is-meet-pointwise pwise .is-meet.greatest lbβ€² lbβ€²<f lbβ€²<g i =
    pwise i .is-meet.greatest (lbβ€² i) (lbβ€²<f i) (lbβ€²<g i)

  is-join-pointwise
    : (βˆ€ i β†’ is-join P (f i) (g i) (h i))
    β†’ is-join (Pointwise I P) f g h
  is-join-pointwise pwise .is-join.l≀join i = pwise i .is-join.l≀join
  is-join-pointwise pwise .is-join.r≀join i = pwise i .is-join.r≀join
  is-join-pointwise pwise .is-join.least lbβ€² lbβ€²<f lbβ€²<g i =
    pwise i .is-join.least (lbβ€² i) (lbβ€²<f i) (lbβ€²<g i)

With a couple more variables, we see that the results above are a special case of both arbitrary lubs and glbs being pointwise:

module
  _ {β„“β‚’ β„“α΅£ β„“α΅’ β„“β±Ό} {I : Type β„“α΅’} {J : Type β„“β±Ό}
    (P : Poset β„“β‚’ β„“α΅£)
    (F : I β†’ J β†’ ⌞ P ⌟)
    (m : J β†’ ⌞ P ⌟)
  where

  is-lub-pointwise
    : (βˆ€ j β†’ is-lub P (Ξ» i β†’ F i j) (m j))
    β†’ is-lub (Pointwise J P) F m
  is-lub-pointwise pwise .is-lub.fam≀lub i j = pwise j .is-lub.fam≀lub i
  is-lub-pointwise pwise .is-lub.least ubβ€² fi<ubβ€² j =
    pwise j .is-lub.least (ubβ€² j) Ξ» i β†’ fi<ubβ€² i j

  is-glb-pointwise
    : (βˆ€ j β†’ is-glb P (Ξ» i β†’ F i j) (m j))
    β†’ is-glb (Pointwise J P) F m
  is-glb-pointwise pwise .is-glb.glb≀fam i j = pwise j .is-glb.glb≀fam i
  is-glb-pointwise pwise .is-glb.greatest ubβ€² fi<ubβ€² j =
    pwise j .is-glb.greatest (ubβ€² j) Ξ» i β†’ fi<ubβ€² i j

  1. In the code, this means that is-meet holds, but we will abuse this β€œfunctional” notation for clarity.β†©οΈŽ