refactor(CategoryTheory/SmallObject): generalization of the definitio…

…ns (#20256)

The ongoing definition of the iteration of a natural transformation `ε : 𝟭 C ⟶ F` (with `F : C ⥤ C`) is generalized to "successor structures" (which shall become a mathlibism), i.e. in a category `D`, this consists of a zeroth object `X₀`, a successor application `succ : D → D` and, for all `X : D`, a map `toSucc X : X → succ X` (which does not have to be natural: it is not always so in some applications). For such a `Φ : SuccStruct D`, if `J` is a well-ordered type, we define the `J`-th iteration of `Φ`. (In the case `J := ℕ`, this is the colimit of `succ (succ (succ (succ ... X₀)))`.)

The iteration of a functor is a particular case of this constructor with `D := C ⥤ C`.

As `toSucc` does not have to be natural in `X`, the caveat is that the proofs make extensive use of equalities of objects in `C` and `Arrow C`, while my previous construction used comparison isomorphisms. Nevertheless, the proofs look much more clean now. One of the reasons is that in the inductive construction (file `Iteration.Nonempty`), in the terms of data, we only need to provide a functor, and then all the fields are in `Prop`. (In the downstream API, we shall obviously use isomorphisms instead of equalities...)

This PR supersedes #19264. The results are used in #20245 in order to get functorial factorizations in the small object argument.

After refactoring my code, I found that this approach had already been used in 2018 by Reid Barton in his pioneering formalization work in Lean 3 towards the model category structure on topological spaces.



Co-authored-by: Joël Riou <[email protected]>

Mathlib.lean

@@ -2268,7 +2268,6 @@ import Mathlib.CategoryTheory.SmallObject.Iteration.Basic
 import Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
 import Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
 import Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
-import Mathlib.CategoryTheory.SmallObject.Iteration.UniqueHom
 import Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
 import Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
 import Mathlib.CategoryTheory.Square