Commit 2025-02-03 20:04 96a5ba5c
View on Github →refactor(CategoryTheory/SmallObject): generalization of the definitions (#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.