Order preserving maps between large posets
Content created by Egbert Rijke and Fredrik Bakke.
Created on 2023-05-10.
Last modified on 2024-03-11.
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)
See also
- Order preserving maps between large posets
- Similarity of order preserving maps between large posets
Recent changes
- 2024-03-11. Fredrik Bakke. Refactor category theory to use strictly involutive identity types (#1052).
- 2023-11-27. Fredrik Bakke. Refactor categories to carry a bidirectional witness of associativity (#945).
- 2023-11-24. Egbert Rijke. Refactor precomposition (#937).
- 2023-11-24. Egbert Rijke. Abelianization (#877).
- 2023-09-26. Fredrik Bakke and Egbert Rijke. Maps of categories, functor categories, and small subprecategories (#794).