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
+strictly-preordered-set-ℕ : Strictly-Preordered-Set lzero lzero
+pr1 strictly-preordered-set-ℕ = ℕ-Set
+pr2 strictly-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/foundation.lagda.md

@@ -405,6 +405,7 @@ open import foundation.structure public
 open import foundation.structure-identity-principle public
 open import foundation.structured-equality-duality public
 open import foundation.structured-type-duality public
+open import foundation.subsequences public
 open import foundation.subsingleton-induction public
 open import foundation.subterminal-types public
 open import foundation.subtype-duality public

src/foundation/strictly-right-unital-concatenation-identifications.lagda.md

@@ -64,7 +64,7 @@ module _
   right-strict-concat' x q p = p ∙ᵣ q
 ```
 
-### Translating between the stictly left and stricly right unital versions of concatenation
+### Translating between the strictly left and strictly right unital versions of concatenation
 
 ```agda
 module _

src/foundation/subsequences.lagda.md

@@ -0,0 +1,154 @@
+# Subsequences
+
+```agda
+module foundation.subsequences where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.inequality-natural-numbers
+open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.strict-inequality-natural-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.function-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.identity-types
+open import foundation.propositional-truncations
+open import foundation.sequences
+open import foundation.universe-levels
+
+open import order-theory.infinite-limit-sequences-preorders
+open import order-theory.strict-order-preserving-maps
+open import order-theory.strictly-increasing-sequences-strictly-preordered-sets
+```
+
+</details>
+
+## Idea
+
+A {{concept "subsequence" Agda=subsequence}} of a
+[sequence](foundation.sequences.md) `u : ℕ → A` is a sequence `u ∘ f` for some
+[strictly increasing](order-theory.strict-order-preserving-maps.md) sequence
+`f : ℕ → ℕ`.
+
+## Definitions
+
+### Subsequences of a sequence
+
+```agda
+module _
+  {l : Level} {A : UU l} (u : sequence A)
+  where
+
+  subsequence : UU lzero
+  subsequence =
+    hom-Strictly-Preordered-Set
+      strictly-preordered-set-ℕ
+      strictly-preordered-set-ℕ
+
+  extract-subsequence : subsequence → ℕ → ℕ
+  extract-subsequence =
+    map-hom-Strictly-Preordered-Set
+      strictly-preordered-set-ℕ
+      strictly-preordered-set-ℕ
+
+  is-strictly-increasing-extract-subsequence :
+    (f : subsequence) →
+    preserves-strict-order-map-Strictly-Preordered-Set
+      ( strictly-preordered-set-ℕ)
+      ( strictly-preordered-set-ℕ)
+      ( extract-subsequence f)
+  is-strictly-increasing-extract-subsequence =
+    preserves-strict-order-hom-Strictly-Preordered-Set
+      strictly-preordered-set-ℕ
+      strictly-preordered-set-ℕ
+
+  seq-subsequence : subsequence → sequence A
+  seq-subsequence f n = u (extract-subsequence f n)
+```
+
+## Properties
+
+### Any sequence is a subsequence of itself
+
+```agda
+module _
+  {l : Level} {A : UU l} (u : sequence A)
+  where
+
+  refl-subsequence : subsequence u
+  refl-subsequence = id-hom-Strictly-Preordered-Set strictly-preordered-set-ℕ
+```
+
+### A subsequence of a subsequence is a subsequence of the original sequence
+
+```agda
+module _
+  {l : Level} {A : UU l} (u : sequence A)
+  where
+
+  sub-subsequence :
+    (v : subsequence u) →
+    (w : subsequence (seq-subsequence u v)) →
+    subsequence u
+  sub-subsequence =
+    comp-hom-Strictly-Preordered-Set
+      strictly-preordered-set-ℕ
+      strictly-preordered-set-ℕ
+      strictly-preordered-set-ℕ
+```
+
+### The extraction sequence of a subsequence is superlinear
+
+```agda
+module _
+  {l : Level} {A : UU l} (u : sequence A) (v : subsequence u)
+  where
+
+  abstract
+    is-superlinear-extract-subsequence :
+      (n : ℕ) → leq-ℕ n (extract-subsequence u v n)
+    is-superlinear-extract-subsequence zero-ℕ =
+      leq-zero-ℕ (extract-subsequence u v zero-ℕ)
+    is-superlinear-extract-subsequence (succ-ℕ n) =
+      leq-succ-le-ℕ
+        ( n)
+        ( extract-subsequence u v (succ-ℕ n))
+        ( concatenate-leq-le-ℕ
+          { n}
+          { extract-subsequence u v n}
+          { extract-subsequence u v (succ-ℕ n)}
+          ( is-superlinear-extract-subsequence n)
+          ( le-succ-is-strictly-increasing-sequence-Strictly-Preordered-Set
+            ( strictly-preordered-set-ℕ)
+            ( extract-subsequence u v)
+            ( is-strictly-increasing-extract-subsequence u v)
+            ( n)))
+```
+
+### The extraction sequence of a subsequence tends to infinity
+
+```agda
+module _
+  {l : Level} {A : UU l} (u : sequence A) (v : subsequence u)
+  where
+
+  modulus-tends-to-infinity-extract-subsequence :
+    modulus-tends-to-infinity-sequence-Preorder
+      ( ℕ-Preorder)
+      ( extract-subsequence u v)
+  modulus-tends-to-infinity-extract-subsequence =
+    modulus-leq-modulus-tends-to-infinity-sequence-Preorder
+      ( ℕ-Preorder)
+      ( id)
+      ( extract-subsequence u v)
+      ( is-superlinear-extract-subsequence u v)
+      ( id , λ i j → id)
+
+  tends-to-infinity-extract-subsequence :
+    tends-to-infinity-sequence-Preorder ℕ-Preorder (extract-subsequence u v)
+  tends-to-infinity-extract-subsequence =
+    unit-trunc-Prop modulus-tends-to-infinity-extract-subsequence
+```

src/order-theory.lagda.md

@@ -52,6 +52,8 @@ 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.infinite-limit-sequences-preorders 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 +116,16 @@ 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-preorders 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-leq-succ-sequence-Poset :
+    ((n : ℕ) → leq-Poset P (u n) (u (succ-ℕ n))) →
+    is-increasing-sequence-Poset P u
+  is-increasing-leq-succ-sequence-Poset =
+    preserves-order-ind-ℕ-Poset P u
+
+  leq-succ-is-increasing-sequence-Poset :
+    is-increasing-sequence-Poset P u →
+    ((n : ℕ) → leq-Poset P (u n) (u (succ-ℕ n)))
+  leq-succ-is-increasing-sequence-Poset H n =
+    H n (succ-ℕ n) (succ-leq-ℕ n)
+```