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 , , and are families of elements with a poset, such that, for all , we have 1, then when 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