Bourbaki-Witt Theorem

This file proves the Bourbaki-Witt Theorem.

Main definitions

• class ChainCompletePartialOrder : A nonempty partial order is a chain complete partial order such that every nonempty chain has a supremum

Main statements

• nonempty_fixedPoints_of_inflationary : The Bourbaki-Witt Theorem : If $X$ is a chain complete partial order and $f : X → X$ is inflationary (i.e. ∀ x, x ≤ f x), then $f$ has a fixed point

References

The proof used can be found in [serge_lang_algebra]

structure NonemptyChain (α : Type u_2) [LE α] : Type u_2

The type of nonempty chains of an order

• carrier : Set α

  The underlying set of a nonempty chain

• Nonempty' : self.carrier.Nonempty
• isChain' : IsChain (fun (x1 x2 : α) => x1 ≤ x2) self.carrier

theorem NonemptyChain.ext_iff {α : Type u_2} {inst✝ : LE α} {x y : NonemptyChain α} : x = y ↔ x.carrier = y.carrier

theorem NonemptyChain.ext {α : Type u_2} {inst✝ : LE α} {x y : NonemptyChain α} (carrier : x.carrier = y.carrier) : x = y

instance instSetLikeNonemptyChain {α : Type u_2} [LE α] : SetLike (NonemptyChain α) α

instance instPartialOrderNonemptyChain {α : Type u_2} [LE α] : PartialOrder (NonemptyChain α)

class ChainCompletePartialOrder (α : Type u_2) extends PartialOrder α : Type u_2

A chain complete partial order (CCPO) is a nonempty partial order such that every nonempty chain has a supremum (which we call cSup)

• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• cSup : NonemptyChain α → α

  The supremum of a nonempty chain

• le_cSup (c : NonemptyChain α) (x : α) : x ∈ c.carrier → x ≤ cSup c

  cSup is an upper bound of the nonempty chain

• cSup_le (c : NonemptyChain α) (x : α) : (∀ y ∈ c.carrier, y ≤ x) → cSup c ≤ x

  cSup is a lower bound of the set of upper bounds of the nonempty chain

instance ChainCompletePartialOrder.instOmegaCompletePartialOrder {α : Type u_1} [ChainCompletePartialOrder α] : OmegaCompletePartialOrder α

instance ChainCompletePartialOrder.instOfCompleteLattice {α : Type u_1} [CompleteLattice α] : ChainCompletePartialOrder α

structure ChainCompletePartialOrder.IsAdmissible {α : Type u_1} [ChainCompletePartialOrder α] (x : α) (f : α → α) (s : Set α) : Prop

An admissible set for given x : α and f : α → α has x, the base point, as a least element and is closed under applying f and cSup.

• base_isLeast : IsLeast s x

  The base point is the least element of an admissible set

• image_self_subset_self : f '' s ⊆ s

  The image of an admissible set under f is a subset of itself

• cSup_mem (c : NonemptyChain α) : ↑c ⊆ s → cSup c ∈ s

  If a chain is a subset of an admissible set, its cSup is a member of the admissible set

theorem ChainCompletePartialOrder.ici_isAdmissible {α : Type u_1} [ChainCompletePartialOrder α] {x : α} {f : α → α} (le_map : ∀ (x : α), x ≤ f x) : IsAdmissible x f (Set.Ici x)

@[reducible, inline]

abbrev ChainCompletePartialOrder.bot {α : Type u_1} [ChainCompletePartialOrder α] (x : α) (f : α → α) : Set α

The bottom admissible set with base point x and inflationary function f

theorem ChainCompletePartialOrder.bot_isAdmissible {α : Type u_1} [ChainCompletePartialOrder α] {x : α} {f : α → α} (le_map : ∀ (x : α), x ≤ f x) : IsAdmissible x f (bot x f)

theorem ChainCompletePartialOrder.subset_bot_iff {α : Type u_1} [ChainCompletePartialOrder α] {x : α} {f : α → α} {s : Set α} (h : IsAdmissible x f s) : s ⊆ bot x f ↔ s = bot x f

theorem ChainCompletePartialOrder.map_mem_bot {α : Type u_1} [ChainCompletePartialOrder α] {x : α} {f : α → α} {y : α} (le_map : ∀ (x : α), x ≤ f x) (h : y ∈ bot x f) : f y ∈ bot x f

structure ChainCompletePartialOrder.IsExtremePt {α : Type u_1} [ChainCompletePartialOrder α] (x : α) (f : α → α) (y : α) : Prop

y is an extreme point for x : α and f : α → α if it is in the bottom admissible set and y is larger than f z for any z < y in the bottom admissible set. This definition comes from [serge_lang_algebra]

• mem_bot : y ∈ bot x f
• map_le_of_mem_of_lt {z : α} (h : z ∈ bot x f) (h' : z < y) : f z ≤ y

theorem ChainCompletePartialOrder.IsExtremePt.bot_eq_of_le_or_map_le {α : Type u_1} [ChainCompletePartialOrder α] {x : α} {f : α → α} {y : α} (le_map : ∀ (x : α), x ≤ f x) (hy : IsExtremePt x f y) : {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} = bot x f

If y is an extreme point and f is inflationary, then there are no element between y and f y.

theorem ChainCompletePartialOrder.IsExtremePt.setOf_isExtremePt_isAdmissible {α : Type u_1} [ChainCompletePartialOrder α] {x : α} {f : α → α} (le_map : ∀ (x : α), x ≤ f x) : IsAdmissible x f {y : α | IsExtremePt x f y}

theorem ChainCompletePartialOrder.IsExtremePt.setOf_isExtremePt_eq_bot {α : Type u_1} [ChainCompletePartialOrder α] {x : α} {f : α → α} (le_map : ∀ (x : α), x ≤ f x) : {y : α | IsExtremePt x f y} = bot x f

theorem ChainCompletePartialOrder.IsExtremePt.mem_bot_iff_isExtremePt {α : Type u_1} [ChainCompletePartialOrder α] {x : α} {f : α → α} {y : α} (le_map : ∀ (x : α), x ≤ f x) : y ∈ bot x f ↔ IsExtremePt x f y

theorem ChainCompletePartialOrder.IsExtremePt.bot_isChain {α : Type u_1} [ChainCompletePartialOrder α] {x : α} {f : α → α} (le_map : ∀ (x : α), x ≤ f x) : IsChain (fun (x1 x2 : α) => x1 ≤ x2) (bot x f)

theorem ChainCompletePartialOrder.nonempty_fixedPoints_of_inflationary {α : Type u_1} [ChainCompletePartialOrder α] {f : α → α} [Nonempty α] (le_map : ∀ (x : α), x ≤ f x) : (Function.fixedPoints f).Nonempty