Existence of objects in the category of iterations of functors #
Given a functor Φ : C ⥤ C and a natural transformation ε : 𝟭 C ⟶ Φ,
we shall show in this file that for any well ordered set J,
and j : J, the category Functor.Iteration ε j is nonempty.
As we already know from the main result in SmallObject.Iteration.UniqueHom
that such objects, if they exist, are unique up to a unique isomorphism,
we shall show the existence of a term in Functor.Iteration ε j by
transfinite induction.
def
CategoryTheory.Functor.Iteration.mkOfBot
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{Φ : CategoryTheory.Functor C C}
(ε : CategoryTheory.Functor.id C ⟶ Φ)
(J : Type u)
[LinearOrder J]
[OrderBot J]
[SuccOrder J]
:
The obvious term in Iteration ε ⊥: it is given by the identity functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.Functor.Iteration.mkOfSucc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{Φ : CategoryTheory.Functor C C}
{ε : CategoryTheory.Functor.id C ⟶ Φ}
{J : Type u}
[LinearOrder J]
[OrderBot J]
[SuccOrder J]
{j : J}
(hj : ¬IsMax j)
(iter : CategoryTheory.Functor.Iteration ε j)
:
When j : J is not maximal, this is the extension as Iteration ε (Order.succ j)
of any iter : Iteration ε j.
Equations
- One or more equations did not get rendered due to their size.