Increasing sequences in partially ordered sets

Content created by malarbol.

Created on 2025-04-22.
Last modified on 2025-04-22.

module order-theory.increasing-sequences-posets where
Imports 
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
open import order-theory.subposets

Idea

A sequence in a partially ordered set u is increasing if it preserves the standard ordering on the natural numbers or, equivalently, if uₙ ≤ uₙ₊₁ for all n : ℕ.

Definitions

The predicate of being an increasing sequence in a partially ordered set

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

The poset of increasing sequences in a poset

module _
  {l1 l2 : Level} (P : Poset l1 l2)
  where

  increasing-sequence-Poset : Poset (l1 ⊔ l2) l2
  increasing-sequence-Poset =
    poset-Subposet
      ( sequence-Poset P)
      ( is-increasing-prop-sequence-Poset P)

  type-increasing-sequence-Poset : UU (l1 ⊔ l2)
  type-increasing-sequence-Poset =
    type-Poset increasing-sequence-Poset

  seq-increasing-sequence-Poset :
    type-increasing-sequence-Poset →
    type-sequence-Poset P
  seq-increasing-sequence-Poset = pr1

  is-increasing-seq-increasing-sequence-Poset :
    (u : type-increasing-sequence-Poset) →
    is-increasing-sequence-Poset
      ( P)
      ( seq-increasing-sequence-Poset u)
  is-increasing-seq-increasing-sequence-Poset = pr2

Properties

A sequence u in a poset is increasing if and only if uₙ ≤ uₙ₊₁ for all n : ℕ

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)

Recent changes