The Knaster–Tarski fixed point theorem

Content created by Fredrik Bakke.

Created on 2024-11-20.
Last modified on 2024-11-20.

module order-theory.knaster-tarski-fixed-point-theorem where
Imports 
open import foundation.dependent-pair-types
open import foundation.fixed-points-endofunctions
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.universe-levels

open import order-theory.inflattices
open import order-theory.order-preserving-maps-posets
open import order-theory.posets
open import order-theory.suplattices

Idea

The Knaster–Tarski fixed point theorem states that every order preserving endomap f : 𝒜 → 𝒜 on a complete lattice has a least and a greatest fixed point. Indeed, any order preserving endomap on a suplattice has a greatest fixed point and any order preserving endomap on an inflattice has a least fixed point.

Theorem

The Knaster–Tarski fixed point theorem for suplattices

module _
  {l1 l2 : Level}
  (𝒜 : Suplattice l1 l2 (l1 ⊔ l2))
  (f : type-Suplattice 𝒜 → type-Suplattice 𝒜)
  (F : preserves-order-Poset (poset-Suplattice 𝒜) (poset-Suplattice 𝒜) f)
  where

  indexing-type-family-of-elements-knaster-tarski-Suplattice : UU (l1 ⊔ l2)
  indexing-type-family-of-elements-knaster-tarski-Suplattice =
    Σ ( type-Suplattice 𝒜) (λ x → leq-Suplattice 𝒜 x (f x))

  family-of-elements-knaster-tarski-Suplattice :
    indexing-type-family-of-elements-knaster-tarski-Suplattice →
    type-Suplattice 𝒜
  family-of-elements-knaster-tarski-Suplattice = pr1

  point-knaster-tarski-Suplattice : type-Suplattice 𝒜
  point-knaster-tarski-Suplattice =
    sup-Suplattice 𝒜 family-of-elements-knaster-tarski-Suplattice

  leq-point-knaster-tarski-Suplattice :
    leq-Suplattice 𝒜
      ( point-knaster-tarski-Suplattice)
      ( f point-knaster-tarski-Suplattice)
  leq-point-knaster-tarski-Suplattice =
    forward-implication
      ( is-least-upper-bound-sup-Suplattice 𝒜
        ( family-of-elements-knaster-tarski-Suplattice)
        ( f point-knaster-tarski-Suplattice))
      ( λ w →
        transitive-leq-Suplattice 𝒜 _ _ _
          ( F ( pr1 w)
              ( point-knaster-tarski-Suplattice)
              ( is-upper-bound-family-of-elements-sup-Suplattice 𝒜 _ w))
          ( pr2 w))

  geq-point-knaster-tarski-Suplattice :
    leq-Suplattice 𝒜
      ( f point-knaster-tarski-Suplattice)
      ( point-knaster-tarski-Suplattice)
  geq-point-knaster-tarski-Suplattice =
    is-upper-bound-family-of-elements-sup-Suplattice 𝒜
      ( family-of-elements-knaster-tarski-Suplattice)
      ( f point-knaster-tarski-Suplattice ,
        F point-knaster-tarski-Suplattice
          ( f point-knaster-tarski-Suplattice)
          ( leq-point-knaster-tarski-Suplattice))

  is-fixed-point-knaster-tarski-Suplattice :
    f ( point-knaster-tarski-Suplattice) ＝
    point-knaster-tarski-Suplattice
  is-fixed-point-knaster-tarski-Suplattice =
    antisymmetric-leq-Suplattice 𝒜
      ( f (point-knaster-tarski-Suplattice))
      ( point-knaster-tarski-Suplattice)
      ( geq-point-knaster-tarski-Suplattice)
      ( leq-point-knaster-tarski-Suplattice)

  fixed-point-knaster-tarski-Suplattice : fixed-point f
  fixed-point-knaster-tarski-Suplattice =
    point-knaster-tarski-Suplattice ,
    is-fixed-point-knaster-tarski-Suplattice

  greatest-fixed-point-knaster-tarski-Suplattice :
    (x : fixed-point f) →
    leq-Suplattice 𝒜 (pr1 x) point-knaster-tarski-Suplattice
  greatest-fixed-point-knaster-tarski-Suplattice (x , p) =
    is-upper-bound-family-of-elements-sup-Suplattice 𝒜 _
      ( x ,
        concatenate-leq-eq-Poset
          ( poset-Suplattice 𝒜)
          ( refl-leq-Suplattice 𝒜 x)
          ( inv p))

The Knaster–Tarski fixed point theorem for inflattices

module _
  {l1 l2 : Level}
  (𝒜 : Inflattice l1 l2 (l1 ⊔ l2))
  (f : type-Inflattice 𝒜 → type-Inflattice 𝒜)
  (F : preserves-order-Poset (poset-Inflattice 𝒜) (poset-Inflattice 𝒜) f)
  where

  indexing-type-family-of-elements-knaster-tarski-Inflattice : UU (l1 ⊔ l2)
  indexing-type-family-of-elements-knaster-tarski-Inflattice =
    Σ ( type-Inflattice 𝒜) (λ x → leq-Inflattice 𝒜 (f x) x)

  family-of-elements-knaster-tarski-Inflattice :
    indexing-type-family-of-elements-knaster-tarski-Inflattice →
    type-Inflattice 𝒜
  family-of-elements-knaster-tarski-Inflattice = pr1

  point-knaster-tarski-Inflattice : type-Inflattice 𝒜
  point-knaster-tarski-Inflattice =
    inf-Inflattice 𝒜 family-of-elements-knaster-tarski-Inflattice

  geq-point-knaster-tarski-Inflattice :
    leq-Inflattice 𝒜
      ( f point-knaster-tarski-Inflattice)
      ( point-knaster-tarski-Inflattice)
  geq-point-knaster-tarski-Inflattice =
    forward-implication
      ( is-greatest-lower-bound-inf-Inflattice 𝒜
        ( family-of-elements-knaster-tarski-Inflattice)
        ( f point-knaster-tarski-Inflattice))
      ( λ w →
        transitive-leq-Inflattice 𝒜 _ _ _
          ( pr2 w)
          ( F _ _ (is-lower-bound-family-of-elements-inf-Inflattice 𝒜 _ w)))

  leq-point-knaster-tarski-Inflattice :
    leq-Inflattice 𝒜
      ( point-knaster-tarski-Inflattice)
      ( f point-knaster-tarski-Inflattice)
  leq-point-knaster-tarski-Inflattice =
    is-lower-bound-family-of-elements-inf-Inflattice 𝒜
      ( family-of-elements-knaster-tarski-Inflattice)
      ( f point-knaster-tarski-Inflattice ,
        F (f point-knaster-tarski-Inflattice)
          ( point-knaster-tarski-Inflattice)
          ( geq-point-knaster-tarski-Inflattice))

  is-fixed-point-knaster-tarski-Inflattice :
    f ( point-knaster-tarski-Inflattice) ＝
    point-knaster-tarski-Inflattice
  is-fixed-point-knaster-tarski-Inflattice =
    antisymmetric-leq-Inflattice 𝒜
      ( f (point-knaster-tarski-Inflattice))
      ( point-knaster-tarski-Inflattice)
      ( geq-point-knaster-tarski-Inflattice)
      ( leq-point-knaster-tarski-Inflattice)

  fixed-point-knaster-tarski-Inflattice : fixed-point f
  fixed-point-knaster-tarski-Inflattice =
    point-knaster-tarski-Inflattice ,
    is-fixed-point-knaster-tarski-Inflattice

  least-fixed-point-knaster-tarski-Inflattice :
    (x : fixed-point f) →
    leq-Inflattice 𝒜 point-knaster-tarski-Inflattice (pr1 x)
  least-fixed-point-knaster-tarski-Inflattice (x , p) =
    is-lower-bound-family-of-elements-inf-Inflattice 𝒜 _
      ( x ,
        concatenate-eq-leq-Poset
          ( poset-Inflattice 𝒜)
          ( p)
          ( refl-leq-Inflattice 𝒜 x))

References

Recent changes