# Order preserving maps between large posets

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-05-10.

module order-theory.order-preserving-maps-large-posets where

Imports
open import foundation.universe-levels

open import order-theory.large-posets
open import order-theory.order-preserving-maps-large-preorders
open import order-theory.similarity-of-elements-large-posets


## Idea

An order preserving map between large posets P and Q consists of a map

  f : type-Large-Poset P l1 → type-Large-Poset Q (γ l1)


for each universe level l1, such that x ≤ y implies f x ≤ f y for any two elements x y : P. The function γ : Level → Level that specifies the universe level of f x in terms of the universe level of x is called the universe level reindexing function of the order preserving map f.

## Definitions

### The predicate that a map between large posets is order preserving

module _
{αP αQ : Level → Level} {βP βQ : Level → Level → Level} {γ : Level → Level}
(P : Large-Poset αP βP) (Q : Large-Poset αQ βQ)
where

preserves-order-map-Large-Poset :
({l : Level} → type-Large-Poset P l → type-Large-Poset Q (γ l)) →
UUω
preserves-order-map-Large-Poset =
preserves-order-map-Large-Preorder
( large-preorder-Large-Poset P)
( large-preorder-Large-Poset Q)


### The type of order preserving maps between large posets

module _
{αP αQ : Level → Level} {βP βQ : Level → Level → Level}
(γ : Level → Level)
(P : Large-Poset αP βP) (Q : Large-Poset αQ βQ)
where

hom-Large-Poset : UUω
hom-Large-Poset =
hom-Large-Preorder γ
( large-preorder-Large-Poset P)
( large-preorder-Large-Poset Q)

module _
{αP αQ γ : Level → Level} {βP βQ : Level → Level → Level}
(P : Large-Poset αP βP) (Q : Large-Poset αQ βQ) (f : hom-Large-Poset γ P Q)
where

map-hom-Large-Poset :
{l : Level} → type-Large-Poset P l → type-Large-Poset Q (γ l)
map-hom-Large-Poset =
map-hom-Large-Preorder f

preserves-order-hom-Large-Poset :
preserves-order-map-Large-Poset P Q map-hom-Large-Poset
preserves-order-hom-Large-Poset =
preserves-order-hom-Large-Preorder f


### The identity order preserving map on a large poset

module _
{αP : Level → Level} {βP : Level → Level → Level} (P : Large-Poset αP βP)
where

id-hom-Large-Poset : hom-Large-Poset (λ l → l) P P
id-hom-Large-Poset = id-hom-Large-Preorder (large-preorder-Large-Poset P)


### Composition of order preserving maps between large posets

module _
{αP αQ αR γg γf : Level → Level} {βP βQ βR : Level → Level → Level}
(P : Large-Poset αP βP)
(Q : Large-Poset αQ βQ)
(R : Large-Poset αR βR)
(g : hom-Large-Poset γg Q R)
(f : hom-Large-Poset γf P Q)
where

map-comp-hom-Large-Poset :
{l1 : Level} → type-Large-Poset P l1 → type-Large-Poset R (γg (γf l1))
map-comp-hom-Large-Poset =
map-comp-hom-Large-Preorder
( large-preorder-Large-Poset P)
( large-preorder-Large-Poset Q)
( large-preorder-Large-Poset R)
( g)
( f)

preserves-order-comp-hom-Large-Poset :
preserves-order-map-Large-Poset P R map-comp-hom-Large-Poset
preserves-order-comp-hom-Large-Poset =
preserves-order-comp-hom-Large-Preorder
( large-preorder-Large-Poset P)
( large-preorder-Large-Poset Q)
( large-preorder-Large-Poset R)
( g)
( f)

comp-hom-Large-Poset : hom-Large-Poset (λ l → γg (γf l)) P R
comp-hom-Large-Poset =
comp-hom-Large-Preorder
( large-preorder-Large-Poset P)
( large-preorder-Large-Poset Q)
( large-preorder-Large-Poset R)
( g)
( f)


### Homotopies of order preserving maps between large posets

Given two order preserving maps f g : hom-Large-Poset γ P Q with the same universe level reindexing γ, a homotopy of order preserving maps from f to g is a pointwise identification of the underlying maps of f and g.

module _
{αP αQ γ : Level → Level} {βP βQ : Level → Level → Level}
(P : Large-Poset αP βP) (Q : Large-Poset αQ βQ)
where

htpy-hom-Large-Poset : (f g : hom-Large-Poset γ P Q) → UUω
htpy-hom-Large-Poset =
htpy-hom-Large-Preorder
( large-preorder-Large-Poset P)
( large-preorder-Large-Poset Q)

refl-htpy-hom-Large-Poset :
(f : hom-Large-Poset γ P Q) → htpy-hom-Large-Poset f f
refl-htpy-hom-Large-Poset =
refl-htpy-hom-Large-Preorder
( large-preorder-Large-Poset P)
( large-preorder-Large-Poset Q)


## Properties

### Composition of order preserving maps is associative

module _
{αP αQ αR αS γh γg γf : Level → Level} {βP βQ βR βS : Level → Level → Level}
(P : Large-Poset αP βP)
(Q : Large-Poset αQ βQ)
(R : Large-Poset αR βR)
(S : Large-Poset αS βS)
(h : hom-Large-Poset γh R S)
(g : hom-Large-Poset γg Q R)
(f : hom-Large-Poset γf P Q)
where

associative-comp-hom-Large-Poset :
htpy-hom-Large-Poset P S
( comp-hom-Large-Poset P Q S (comp-hom-Large-Poset Q R S h g) f)
( comp-hom-Large-Poset P R S h (comp-hom-Large-Poset P Q R g f))
associative-comp-hom-Large-Poset =
associative-comp-hom-Large-Preorder
( large-preorder-Large-Poset P)
( large-preorder-Large-Poset Q)
( large-preorder-Large-Poset R)
( large-preorder-Large-Poset S)
( h)
( g)
( f)


### Composition of order preserving maps satisfies left and right unit laws

module _
{αP αQ γf : Level → Level} {βP βQ : Level → Level → Level}
(P : Large-Poset αP βP)
(Q : Large-Poset αQ βQ)
(f : hom-Large-Poset γf P Q)
where

left-unit-law-comp-hom-Large-Poset :
htpy-hom-Large-Poset P Q
( comp-hom-Large-Poset P Q Q (id-hom-Large-Poset Q) f)
( f)
left-unit-law-comp-hom-Large-Poset =
left-unit-law-comp-hom-Large-Preorder
( large-preorder-Large-Poset P)
( large-preorder-Large-Poset Q)
( f)

right-unit-law-comp-hom-Large-Poset :
htpy-hom-Large-Poset P Q
( comp-hom-Large-Poset P P Q f (id-hom-Large-Poset P))
( f)
right-unit-law-comp-hom-Large-Poset =
right-unit-law-comp-hom-Large-Preorder
( large-preorder-Large-Poset P)
( large-preorder-Large-Poset Q)
( f)


### Order preserving maps preserve similarity of elements

module _
{αP αQ γf : Level → Level} {βP βQ : Level → Level → Level}
(P : Large-Poset αP βP)
(Q : Large-Poset αQ βQ)
(f : hom-Large-Poset γf P Q)
where

preserves-sim-hom-Large-Poset :
{l1 l2 : Level} (x : type-Large-Poset P l1) (y : type-Large-Poset P l2) →
sim-Large-Poset P x y →
sim-Large-Poset Q
( map-hom-Large-Poset P Q f x)
( map-hom-Large-Poset P Q f y)
preserves-sim-hom-Large-Poset =
preserves-sim-hom-Large-Preorder
( large-preorder-Large-Poset P)
( large-preorder-Large-Poset Q)
( f)