open import Cat.Prelude

open import Order.Base

import Cat.Reasoning

import Order.Reasoning

module Order.Morphism where


# Basic properties of monotone mapsπ

private variable
o β : Level
P Q : Poset o β


While we have singled out the monotone maps as the most important class of maps between posets, the following classes of maps are also very relevant in the study of order theory:

module _ {o β o' β'} (P : Poset o β) (Q : Poset o' β') (f : β P β β β Q β) where
private
module P = Poset P
module Q = Poset Q

is-monotone : Type _
is-monotone = β {x y} β x P.β€ y β f x Q.β€ f y

• the antitone maps, which reverse the order:

  is-antitone : Type _
is-antitone = β {x y} β x P.β€ y β f y Q.β€ f x

• the order reflections, which, as the name imply, reflect the order:

  is-order-reflection : Type _
is-order-reflection = β {x y} β f x Q.β€ f y β x P.β€ y

• and finally, the order embeddings, which both preserve and reflect the order.

  is-order-embedding : Type _
is-order-embedding = β {x y} β (x P.β€ y) β (f x Q.β€ f y)


The name βorder embeddingβ reflects the fact that any order embedding is also an embedding of the underlying sets:

  is-order-embeddingβis-embedding
: is-order-embedding β is-embedding f
is-order-embeddingβis-embedding p = injectiveβis-embedding! Ξ» {x} {y} fx=fy β
let
xβ€y = Equiv.from p (Q.β€-refl' fx=fy)
yβ€x = Equiv.from p (Q.β€-refl' (sym fx=fy))
in P.β€-antisym xβ€y yβ€x


Since the order is a proposition, even though an order embedding is defined to be a map which induces equivalences, this is easily seen to reduce to being both monotone and an order-reflection.

  monotone-reflectionβis-order-embedding
: is-monotone β is-order-reflection β is-order-embedding
monotone-reflectionβis-order-embedding p q .fst = p
monotone-reflectionβis-order-embedding p q .snd = biimp-is-equiv! p q

module _ {o β o' β'} {P : Poset o β} {Q : Poset o' β'} where
private
module P = Order.Reasoning P
module Q = Order.Reasoning Q


The rest of this module will be dedicated to proving various closure properties about the classes of maps defined above. First, we turn to the construction of order-embeddings. If is any function (not necessarily monotone!) which admits a monotone right inverse then is an order-reflection:

  sectionβorder-reflection
: β (f : β P β β β Q β) (g : Monotone Q P)
β is-right-inverse f (g .hom)
β is-order-reflection P Q f
sectionβorder-reflection f g sect {x = x} {y = y} fxβ€fy =
g # (f x)   P.β€β¨ g .pres-β€ fxβ€fy β©P.β€
g # (f y)   P.=β¨ sect y β©P.=
y           P.β€β


As a corollary, if in the setup above is monotone, then itβs actually an order-embedding. This means that is equivalent, as a poset, to its image in

  sectionβorder-embedding
: β (f : Monotone P Q) (g : Monotone Q P)
β is-right-inverse (f .hom) (g .hom)
β is-order-embedding P Q (f .hom)
sectionβorder-embedding f g sect =
monotone-reflectionβis-order-embedding P Q _
(f .pres-β€) (sectionβorder-reflection (apply f) g sect)

module _ {o β} {P Q : Poset o β} where
private
module P = Order.Reasoning P
module Q = Order.Reasoning Q

open Cat.Reasoning (Posets o β)

  has-retractβis-order-reflection
: (f : Hom P Q)
β Posets.has-retract f
β is-order-reflection P Q (apply f)
has-retractβis-order-reflection f f-ret =
sectionβorder-reflection (apply f) (f-ret .retract) (Ξ» x β f-ret .is-retract #β x)

has-retractβis-order-embedding
: (f : Hom P Q)
β Posets.has-retract f
β is-order-embedding P Q (apply f)
has-retractβis-order-embedding f f-ret =
sectionβorder-embedding f (f-ret .retract) (Ξ» x β f-ret .is-retract #β x)


Since an isomorphism in certainly has a monotone right inverse, we conclude that order-isomorphisms are also order-embeddings.

  order-iso-is-order-embedding
: (f : P β Q) β is-order-embedding P Q (apply (f .Posets.to))
order-iso-is-order-embedding f =
has-retractβis-order-embedding (f .to) (isoβto-has-retract f)