Transfinite iteration of a function I → I

Given φ : I → I where [SupSet I], we define the jth transfinite iteration of φ for any j : J, with J a well-ordered type: this is transfiniteIterate φ j : I → I. If i₀ : I, then transfiniteIterate φ ⊥ i₀ = i₀; if j is a non-maximal element, then transfiniteIterate φ (Order.succ j) i₀ = φ (transfiniteIterate φ j i₀); and if j is a limit element, transfiniteIterate φ j i₀ is the supremum of the transfiniteIterate φ l i₀ for l < j.

If I is a complete lattice, we show that j ↦ transfiniteIterate φ j i₀ is a monotone function if i ≤ φ i for all i. Moreover, if i < φ i when i ≠ ⊤, we show in the lemma top_mem_range_transfiniteIteration that there exists j : J such that transfiniteIteration φ i₀ j = ⊤ if we assume that j ↦ transfiniteIterate φ i₀ j : J → I is not injective (which shall hold when we know Cardinal.mk I < Cardinal.mk J).

TODO (@joelriou)

• deduce that in a Grothendieck abelian category, there is a set I of monomorphisms such that any monomorphism is a transfinite composition of pushouts of morphisms in I, and then an object X is injective iff X ⟶ 0 has the right lifting property with respect to I.

noncomputable def transfiniteIterate {I : Type u} [SupSet I] (φ : I → I) {J : Type w} [LinearOrder J] [SuccOrder J] [WellFoundedLT J] (j : J) : I → I

The jth-iteration of a function φ : I → I when j : J belongs to a well-ordered type.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem transfiniteIterate_bot {I : Type u} [SupSet I] (φ : I → I) {J : Type w} [LinearOrder J] [SuccOrder J] [WellFoundedLT J] [OrderBot J] (i₀ : I) : transfiniteIterate φ ⊥ i₀ = i₀

theorem transfiniteIterate_succ {I : Type u} [SupSet I] (φ : I → I) {J : Type w} [LinearOrder J] [SuccOrder J] [WellFoundedLT J] (i₀ : I) (j : J) (hj : ¬IsMax j) : transfiniteIterate φ (Order.succ j) i₀ = φ (transfiniteIterate φ j i₀)

theorem transfiniteIterate_limit {I : Type u} [SupSet I] (φ : I → I) {J : Type w} [LinearOrder J] [SuccOrder J] [WellFoundedLT J] (i₀ : I) (j : J) (hj : Order.IsSuccLimit j) : transfiniteIterate φ j i₀ = ⨆ (x : ↑(Set.Iio j)), transfiniteIterate φ (↑x) i₀

theorem monotone_transfiniteIterate {I : Type u} [CompleteLattice I] (φ : I → I) (i₀ : I) {J : Type w} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] (hφ : ∀ (i : I), i ≤ φ i) : Monotone fun (j : J) => transfiniteIterate φ j i₀

theorem top_mem_range_transfiniteIterate {I : Type u} [CompleteLattice I] (φ : I → I) (i₀ : I) {J : Type w} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] (hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i) (φtop : φ ⊤ = ⊤) (H : ¬Function.Injective fun (j : J) => transfiniteIterate φ j i₀) : ∃ (j : J), transfiniteIterate φ j i₀ = ⊤