Monotonic sequences in posets

src/elementary-number-theory/strict-inequality-natural-numbers.lagda.md

@@ -8,6 +8,7 @@ module elementary-number-theory.strict-inequality-natural-numbers where
 
 ```agda
 open import elementary-number-theory.addition-natural-numbers
+open import elementary-number-theory.equality-natural-numbers
 open import elementary-number-theory.inequality-natural-numbers
 open import elementary-number-theory.multiplication-natural-numbers
 open import elementary-number-theory.natural-numbers
@@ -29,6 +30,8 @@ open import foundation.propositions
 open import foundation.transport-along-identifications
 open import foundation.unit-type
 open import foundation.universe-levels
+
+open import order-theory.strictly-preordered-sets
 ```
 
 </details>
@@ -148,6 +151,15 @@ transitive-le-ℕ (succ-ℕ n) (succ-ℕ m) (succ-ℕ l) p q =
   transitive-le-ℕ n m l p q
 ```
 
+### The strictly preordered set of natural numbers orderd by strict inequality
+
+```agda
+ℕ-Strict-Preordered-Set : Strictly-Preordered-Set lzero lzero
+pr1 ℕ-Strict-Preordered-Set = ℕ-Set
+pr2 ℕ-Strict-Preordered-Set =
+  le-ℕ-Prop , anti-reflexive-le-ℕ , λ n m l I J → transitive-le-ℕ n m l J I
+```
+
 ### A sharper variant of transitivity
 
 ```agda

src/order-theory.lagda.md

@@ -52,6 +52,7 @@ open import order-theory.homomorphisms-meet-suplattices public
 open import order-theory.homomorphisms-suplattices public
 open import order-theory.ideals-preorders public
 open import order-theory.incidence-algebras public
+open import order-theory.increasing-sequences-posets public
 open import order-theory.inflationary-maps-posets public
 open import order-theory.inflationary-maps-preorders public
 open import order-theory.inflattices public
@@ -114,12 +115,15 @@ open import order-theory.reflective-galois-connections-large-posets public
 open import order-theory.resizing-posets public
 open import order-theory.resizing-preorders public
 open import order-theory.resizing-suplattices public
+open import order-theory.sequences-posets public
+open import order-theory.sequences-strictly-preordered-sets public
 open import order-theory.similarity-of-elements-large-posets public
 open import order-theory.similarity-of-elements-large-preorders public
 open import order-theory.similarity-of-order-preserving-maps-large-posets public
 open import order-theory.similarity-of-order-preserving-maps-large-preorders public
 open import order-theory.strict-order-preserving-maps public
 open import order-theory.strict-preorders public
+open import order-theory.strictly-increasing-sequences-strictly-preordered-sets public
 open import order-theory.strictly-inflationary-maps-strict-preorders public
 open import order-theory.strictly-preordered-sets public
 open import order-theory.subposets public

src/order-theory/increasing-sequences-posets.lagda.md

@@ -0,0 +1,74 @@
+# Increasing sequences in partially ordered sets
+
+```agda
+module order-theory.increasing-sequences-posets where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.decidable-total-order-natural-numbers
+open import elementary-number-theory.inequality-natural-numbers
+open import elementary-number-theory.natural-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.sequences
+open import foundation.universe-levels
+
+open import order-theory.order-preserving-maps-posets
+open import order-theory.posets
+open import order-theory.sequences-posets
+```
+
+</details>
+
+## Idea
+
+A [sequence in a partially ordered set](order-theory.sequences-posets.md) `u` is
+{{#concept "increasing" Disambiguation="sequence in a poset" Agda=is-increasing-sequence-Poset}}
+if it [preserves](order-theory.order-preserving-maps-posets.md) the
+[standard ordering on the natural numbers](elementary-number-theory.inequality-natural-numbers.md)
+or, equivalently, if `uₙ ≤ uₙ₊₁` for all `n : ℕ`.
+
+## Definitions
+
+### The predicate of being an increasing sequence in a partially ordered set
+
+```agda
+module _
+  {l1 l2 : Level} (P : Poset l1 l2) (u : type-sequence-Poset P)
+  where
+
+  is-increasing-prop-sequence-Poset : Prop l2
+  is-increasing-prop-sequence-Poset =
+    preserves-order-prop-Poset ℕ-Poset P u
+
+  is-increasing-sequence-Poset : UU l2
+  is-increasing-sequence-Poset =
+    type-Prop is-increasing-prop-sequence-Poset
+```
+
+## Properties
+
+### A sequence `u` in a poset is increasing if and only if `uₙ ≤ uₙ₊₁` for all n : ℕ
+
+```agda
+module _
+  {l1 l2 : Level} (P : Poset l1 l2) (u : type-sequence-Poset P)
+  where
+
+  is-increasing-is-everywhere-increasing-sequence-Poset :
+    ((n : ℕ) → leq-Poset P (u n) (u (succ-ℕ n))) →
+    is-increasing-sequence-Poset P u
+  is-increasing-is-everywhere-increasing-sequence-Poset =
+    preserves-order-ind-ℕ-Poset P u
+
+  is-everywhere-increasing-is-increasing-sequence-Poset :
+    is-increasing-sequence-Poset P u →
+    ((n : ℕ) → leq-Poset P (u n) (u (succ-ℕ n)))
+  is-everywhere-increasing-is-increasing-sequence-Poset H n =
+    H n (succ-ℕ n) (succ-leq-ℕ n)
+```

src/order-theory/order-preserving-maps-posets.lagda.md

@@ -25,7 +25,7 @@ open import order-theory.posets
 
 ## Idea
 
-A map `f : P → Q` between the underlying types of two posets is siad to be
+A map `f : P → Q` between the underlying types of two posets is said to be
 **order preserving** if `x ≤ y` in `P` implies `f x ≤ f y` in `Q`.
 
 ## Definition

src/order-theory/sequences-posets.lagda.md

@@ -0,0 +1,94 @@
+# Sequences in partially ordered sets
+
+```agda
+module order-theory.sequences-posets where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.binary-relations
+open import foundation.dependent-pair-types
+open import foundation.function-extensionality
+open import foundation.function-types
+open import foundation.propositions
+open import foundation.sequences
+open import foundation.universe-levels
+
+open import order-theory.posets
+```
+
+</details>
+
+## Idea
+
+A {{#concept "sequence" Disambiguation="in a poset" Agda=type-sequence-Poset}}
+in a [poset](order-theory.posets.md) is a [sequence](foundation.sequences.md) in
+its underlying type.
+
+## Definitions
+
+### Sequences in partially ordered sets
+
+```agda
+module _
+  {l1 l2 : Level} (P : Poset l1 l2)
+  where
+
+  type-sequence-Poset : UU l1
+  type-sequence-Poset = sequence (type-Poset P)
+```
+
+### Pointwise comparison on sequences in partially ordered sets
+
+```agda
+module _
+  {l1 l2 : Level} (P : Poset l1 l2) (u v : type-sequence-Poset P)
+  where
+
+  leq-value-prop-sequence-Poset : ℕ → Prop l2
+  leq-value-prop-sequence-Poset n = leq-prop-Poset P (u n) (v n)
+
+  leq-value-sequence-Poset : ℕ → UU l2
+  leq-value-sequence-Poset = type-Prop ∘ leq-value-prop-sequence-Poset
+
+  leq-prop-sequence-Poset : Prop l2
+  leq-prop-sequence-Poset = Π-Prop ℕ leq-value-prop-sequence-Poset
+
+  leq-sequence-Poset : UU l2
+  leq-sequence-Poset = type-Prop leq-prop-sequence-Poset
+
+  is-prop-leq-sequence-Poset : is-prop leq-sequence-Poset
+  is-prop-leq-sequence-Poset = is-prop-type-Prop leq-prop-sequence-Poset
+```
+
+## Properties
+
+### The type of sequences in a poset is a poset ordered by pointwise comparison
+
+```agda
+module _
+  {l1 l2 : Level} (P : Poset l1 l2)
+  where
+
+  sequence-Poset : Poset l1 l2
+  pr1 (pr1 sequence-Poset) = type-sequence-Poset P
+  pr1 (pr2 (pr1 sequence-Poset)) = leq-prop-sequence-Poset P
+  pr1 (pr2 (pr2 (pr1 sequence-Poset))) u n = refl-leq-Poset P (u n)
+  pr2 (pr2 (pr2 (pr1 sequence-Poset))) u v w J I n =
+    transitive-leq-Poset P (u n) (v n) (w n) (J n) (I n)
+  pr2 sequence-Poset u v I J =
+    eq-htpy (λ n → antisymmetric-leq-Poset P (u n) (v n) (I n) (J n))
+
+  refl-leq-sequence-Poset : is-reflexive (leq-sequence-Poset P)
+  refl-leq-sequence-Poset = refl-leq-Poset sequence-Poset
+
+  transitive-leq-sequence-Poset : is-transitive (leq-sequence-Poset P)
+  transitive-leq-sequence-Poset = transitive-leq-Poset sequence-Poset
+
+  antisymmetric-leq-sequence-Poset : is-antisymmetric (leq-sequence-Poset P)
+  antisymmetric-leq-sequence-Poset =
+    antisymmetric-leq-Poset sequence-Poset
+```

src/order-theory/sequences-strictly-preordered-sets.lagda.md

@@ -0,0 +1,37 @@
+# Sequences in strictly preordered sets
+
+```agda
+module order-theory.sequences-strictly-preordered-sets where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.sequences
+open import foundation.universe-levels
+
+open import order-theory.strictly-preordered-sets
+```
+
+</details>
+
+## Idea
+
+A
+{{#concept "sequence" Disambiguation="in a strictly preordered set" Agda=type-sequence-Strictly-Preordered-Set}}
+in a [strictly preordered set](order-theory.strictly-preordered-sets.md) is a
+[sequence](foundation.sequences.md) in its underlying type.
+
+## Definition
+
+### Sequences in a strictly preordered set
+
+```agda
+module _
+  {l1 l2 : Level} (A : Strictly-Preordered-Set l1 l2)
+  where
+
+  type-sequence-Strictly-Preordered-Set : UU l1
+  type-sequence-Strictly-Preordered-Set =
+    sequence (type-Strictly-Preordered-Set A)
+```

src/order-theory/strict-order-preserving-maps.lagda.md

@@ -9,6 +9,7 @@ module order-theory.strict-order-preserving-maps where
 ```agda
 open import foundation.binary-relations
 open import foundation.dependent-pair-types
+open import foundation.function-types
 open import foundation.propositions
 open import foundation.subtypes
 open import foundation.universe-levels
@@ -155,3 +156,69 @@ module _
   preserves-strict-order-hom-Strictly-Preordered-Set =
     pr2 f
 ```
+
+## Properties
+
+### The composition of strict order preserving maps preserves the strict ordering
+
+```agda
+module _
+  {l1 l1' l2 l2' l3 l3' : Level}
+  (P : Strict-Preorder l1 l1')
+  (Q : Strict-Preorder l2 l2')
+  (R : Strict-Preorder l3 l3')
+  (g : type-Strict-Preorder Q → type-Strict-Preorder R)
+  (f : type-Strict-Preorder P → type-Strict-Preorder Q)
+  where
+
+  preserves-strict-order-comp-preserves-strict-order-map-Strict-Preorder :
+    preserves-strict-order-map-Strict-Preorder Q R g →
+    preserves-strict-order-map-Strict-Preorder P Q f →
+    preserves-strict-order-map-Strict-Preorder P R (g ∘ f)
+  preserves-strict-order-comp-preserves-strict-order-map-Strict-Preorder
+    G F x y = G (f x) (f y) ∘ (F x y)
+```
+
+### Strict order preserving composition of strict order preserving maps between strict preorders
+
+```agda
+module _
+  {l1 l1' l2 l2' l3 l3' : Level}
+  (P : Strict-Preorder l1 l1')
+  (Q : Strict-Preorder l2 l2')
+  (R : Strict-Preorder l3 l3')
+  (g : hom-Strict-Preorder Q R)
+  (f : hom-Strict-Preorder P Q)
+  where
+
+  comp-hom-Strict-Preorder : hom-Strict-Preorder P R
+  comp-hom-Strict-Preorder =
+    map-hom-Strict-Preorder Q R g ∘ map-hom-Strict-Preorder P Q f ,
+    preserves-strict-order-comp-preserves-strict-order-map-Strict-Preorder P Q R
+      ( map-hom-Strict-Preorder Q R g)
+      ( map-hom-Strict-Preorder P Q f)
+      ( preserves-strict-order-hom-Strict-Preorder Q R g)
+      ( preserves-strict-order-hom-Strict-Preorder P Q f)
+```
+
+### Strict order preserving composition of strict order preserving maps between strictly preordered sets
+
+```agda
+module _
+  {l1 l1' l2 l2' l3 l3' : Level}
+  (P : Strictly-Preordered-Set l1 l1')
+  (Q : Strictly-Preordered-Set l2 l2')
+  (R : Strictly-Preordered-Set l3 l3')
+  (g : hom-Strictly-Preordered-Set Q R)
+  (f : hom-Strictly-Preordered-Set P Q)
+  where
+
+  comp-hom-Strictly-Preordered-Set : hom-Strictly-Preordered-Set P R
+  comp-hom-Strictly-Preordered-Set =
+    comp-hom-Strict-Preorder
+      ( strict-preorder-Strictly-Preordered-Set P)
+      ( strict-preorder-Strictly-Preordered-Set Q)
+      ( strict-preorder-Strictly-Preordered-Set R)
+      ( g)
+      ( f)
+```