module Order.Morphism where

Basic properties of monotone mapsπŸ”—

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:

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:

    : βˆ€ (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 =
    x           P.=˘⟨ sect x ⟩P.=˘
    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

    : βˆ€ (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)

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

    : (f : P β‰… Q) β†’ is-order-embedding P Q (apply (f
  order-iso-is-order-embedding f =
    has-retract→is-order-embedding (f .to) (iso→to-has-retract f)