Skip to content

Order.Iso

Order isomorphisms

This is the Order.Iso module of the Agda Universal Algebra Library.

An order isomorphism between two ordered objects is a pair of monotone maps that are mutually inverse up to the respective equivalences. Because both maps are monotone and the round trips are the identity up to the equivalence, an order isomorphism transports every existing infimum and supremum, so isomorphic posets carry the same lattice (indeed, complete-lattice) structure; this is why no separate preservation clauses for meet and join are needed.

OrderIso states this for raw relations rather than for a bundle, so it applies uniformly to setoid-valued and propositionally-valued orders. That generality is what the library's two motivating instances need: the congruence poset (Con 𝑨 , ≑ , βŠ†) of Setoid.Congruences.Lattice carries an equivalence of mutual containment rather than propositional equality, while a classical lattice carries its meet order from Classical.Properties.Lattice.

(The standard library's IsOrderIsomorphism packages one map with surjectivity instead of an explicit inverse; the two presentations are interconvertible, and the inverse-pair form is the convenient one for transporting structure.)

The record was first introduced next to its first use in a downstream development, with a note that it should migrate here once the group-theoretic side of the library needed it. Classical.Structures.Group.Congruences is that consumer (the correspondence between normal subgroups and congruences is ordinary group theory), so the record now lives in Order/.

{-# OPTIONS --without-K --exact-split --safe #-}

module Order.Iso where

open import Agda.Primitive using () renaming ( Set to Type )

-- Imports from the Agda Standard Library ---------------------------------------
open import Function         using ( _∘_ )
open import Level            using ( Level ; _βŠ”_ )
open import Relation.Binary  using () renaming ( Rel to BinaryRel )

The record

record OrderIso
  {a b ℓ₁ β„“β‚‚ m₁ mβ‚‚ : Level}
  {A : Type a} {B : Type b}
  (_β‰ˆβ‚_ : BinaryRel A ℓ₁) (_≀₁_ : BinaryRel A β„“β‚‚)
  (_β‰ˆβ‚‚_ : BinaryRel B m₁) (_≀₂_ : BinaryRel B mβ‚‚) : Type (a βŠ” b βŠ” ℓ₁ βŠ” β„“β‚‚ βŠ” m₁ βŠ” mβ‚‚) where
  field
    to         : A β†’ B
    from       : B β†’ A
    to-mono    : βˆ€ {x y} β†’ x ≀₁ y β†’ to x ≀₂ to y
    from-mono  : βˆ€ {u v} β†’ u ≀₂ v β†’ from u ≀₁ from v
    to∘from    : βˆ€ u β†’ to (from u) β‰ˆβ‚‚ u
    from∘to    : βˆ€ x β†’ from (to x) β‰ˆβ‚ x

Composition

Order isomorphisms compose. The round trips of the composite pass the inner round trip through the outer maps, which is sound only up to the middle equivalence β€” so composition asks for two congruence witnesses (the second map's to and the first map's from respect the middle equivalence) and for transitivity of the two end equivalences. These are not derivable from the raw relations, but every instance has them: for setoid-valued orders they are the setoid laws, and for containment-style orders (congruences, intervals, partitions) they are monotonicity applied to the two directions of the equivalence. Nothing is assumed of the middle relations beyond what the two isomorphisms already state.

module _
  {a b c ℓ₁ β„“β‚‚ m₁ mβ‚‚ n₁ nβ‚‚ : Level}
  {A : Type a} {B : Type b} {C : Type c}
  {_β‰ˆβ‚_ : BinaryRel A ℓ₁} {_≀₁_ : BinaryRel A β„“β‚‚}
  {_β‰ˆβ‚‚_ : BinaryRel B m₁} {_≀₂_ : BinaryRel B mβ‚‚}
  {_β‰ˆβ‚ƒ_ : BinaryRel C n₁} {_≀₃_ : BinaryRel C nβ‚‚}
  where

  -- Composition of order isomorphisms, given the two congruence witnesses at
  -- the middle equivalence and transitivity at the ends.
  OrderIso-trans :
      (F : OrderIso _β‰ˆβ‚_ _≀₁_ _β‰ˆβ‚‚_ _≀₂_) (G : OrderIso _β‰ˆβ‚‚_ _≀₂_ _β‰ˆβ‚ƒ_ _≀₃_)
    β†’ (βˆ€ {x y} β†’ x β‰ˆβ‚‚ y β†’ OrderIso.to G x β‰ˆβ‚ƒ OrderIso.to G y)
    β†’ (βˆ€ {x y} β†’ x β‰ˆβ‚‚ y β†’ OrderIso.from F x β‰ˆβ‚ OrderIso.from F y)
    β†’ (βˆ€ {x y z} β†’ x β‰ˆβ‚ y β†’ y β‰ˆβ‚ z β†’ x β‰ˆβ‚ z)
    β†’ (βˆ€ {x y z} β†’ x β‰ˆβ‚ƒ y β†’ y β‰ˆβ‚ƒ z β†’ x β‰ˆβ‚ƒ z)
    β†’ OrderIso _β‰ˆβ‚_ _≀₁_ _β‰ˆβ‚ƒ_ _≀₃_
  OrderIso-trans F G G-to-cong F-from-cong β‰ˆβ‚-trans β‰ˆβ‚ƒ-trans = record
    { to         = G.to ∘ F.to
    ; from       = F.from ∘ G.from
    ; to-mono    = G.to-mono ∘ F.to-mono
    ; from-mono  = F.from-mono ∘ G.from-mono
    ; to∘from    = Ξ» u β†’ β‰ˆβ‚ƒ-trans (G-to-cong (F.to∘from (G.from u))) (G.to∘from u)
    ; from∘to    = Ξ» x β†’ β‰ˆβ‚-trans (F-from-cong (G.from∘to (F.to x))) (F.from∘to x)
    }
    where
    module F = OrderIso F
    module G = OrderIso G