Transfinite iterations of a successor structure #
In this file, we introduce the structure SuccStruct on a category C.
It consists of the data of an object X₀ : C, a successor map succ : C → C
and a morphism toSucc : X ⟶ succ X for any X : C. The map toSucc
does not have to be natural in X. For any element j : J in a
well-ordered type J, we would like to define
the iteration of Φ : SuccStruct C, as a functor F : J ⥤ C
such that F.obj ⊥ = X₀, F.obj j ⟶ F.obj (Order.succ j) is toSucc (F.obj j)
when j is not maximal, and when j is limit, F.obj j should be the
colimit of the F.obj k for k < j.
In the small object argument, we shall apply this to the iteration of
a functor F : C ⥤ C equipped with a natural transformation ε : 𝟭 C ⟶ F:
this will correspond to the case of
SuccStruct.ofNatTrans ε : SuccStruct (C ⥤ C), for which X₀ := 𝟭 C,
succ G := G ⋙ F and toSucc G : G ⟶ G ⋙ F is given by whiskerLeft G ε.
The construction of the iteration of Φ : SuccStruct C is done
by transfinite induction, under an assumption HasIterationOfShape C J.
However, for a limit element j : J, the definition of F.obj j
does not involve only the objects F.obj i for i < j, but it also
involves the maps F.obj i₁ ⟶ F.obj i₂ for i₁ ≤ i₂ < j.
Then, this is not a straightforward application of definitions by
transfinite induction. In order to solve this technical difficulty,
we introduce a structure Φ.Iteration j for any j : J. This
structure contains all the expected data and properties for
all the indices that are ≤ j. In this file, we show that
Φ.Iteration j is a subsingleton. The existence shall be
obtained in the file SmallObject.Iteration.Nonempty, and
the construction of the functor Φ.iterationFunctor J : J ⥤ C
and of its colimit Φ.iteration J : C will done in the
file SmallObject.TransfiniteIteration.
The map Φ.toSucc X : X ⟶ Φ.succ X does not have to be natural
(and it is not in certain applications). Then, two isomorphic
objects X and Y may have non isomorphic successors. This is
the reason why we make an extensive use of equalities in
C and in Arrow C in the definitions.
Note #
The iteration was first introduced in mathlib by Joël Riou, using a different approach as the one described above. After refactoring his code, he found that the approach described above had already been used in the pioneering formalization work in Lean 3 by Reid Barton in 2018 towards the model category structure on topological spaces.
The functor Set.Iio i ⥤ C obtained by "restriction" of F : Set.Iic j ⥤ C
when i ≤ j.
Equations
Instances For
Given F : Set.Iic j ⥤ C, i : J such that hi : i ≤ j, this is the
cocone consisting of all maps F.obj ⟨k, hk⟩ ⟶ F.obj ⟨i, hi⟩ for k : J such that k < i.
Equations
Instances For
The functor Set.Iic i ⥤ C obtained by "restriction" of F : Set.Iic j ⥤ C
when i ≤ j.
Equations
Instances For
Given a functor Φ : C ⥤ C, a natural transformation of the form 𝟭 C ⟶ Φ
induces a successor structure on C ⥤ C.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The class of morphisms that are of the form toSucc X : X ⟶ succ X.
Equations
- Φ.prop = CategoryTheory.MorphismProperty.ofHoms fun (X : C) => Φ.toSucc X
Instances For
The map Φ.toSucc X : X ⟶ Φ.Succ X, as an element in Arrow C.
Equations
- Φ.toSuccArrow X = CategoryTheory.Arrow.mk (Φ.toSucc X)
Instances For
If Φ : SuccStruct C and f is a morphism in C which
satisfies Φ.prop f, then this is the isomorphism of arrows
between f and Φ.toSuccArrow X.
Equations
Instances For
Given a functor F : Set.Iic ⥤ C, this is the morphism in C, as an element
in Arrow C, that is obtained by applying F.map to an inequality.
Equations
- CategoryTheory.SmallObject.SuccStruct.arrowMap F i₁ i₂ h₁₂ h₂ = CategoryTheory.Arrow.mk (F.map (CategoryTheory.homOfLE h₁₂))
Instances For
Given a functor F : Set.Iic j ⥤ C and i : J such that i < j,
this is the arrow F.obj ⟨i, _⟩ ⟶ F.obj ⟨Order.succ i, _⟩.
Equations
Instances For
Given F : Set.Iio i ⥤ C, with i a limit element, and k such that hk : k < i,
this is the map colimit.ι F ⟨k, hk⟩, as an element in Arrow C.
Equations
- CategoryTheory.SmallObject.SuccStruct.arrowι F hi k hk = CategoryTheory.Arrow.mk (CategoryTheory.Limits.colimit.ι F ⟨k, hk⟩)
Instances For
The category of jth iterations of a successor structure Φ : SuccStruct C.
An object consists of the data of all iterations of Φ for i : J such
that i ≤ j (this is the field F). Such objects are
equipped with data and properties which characterizes uniquely the iterations
on three types of elements: ⊥, successors, limit elements.
The data of all
ith iterations fori : Jsuch thati ≤ j.The zeroth iteration is the zeroth object .
The iteration on a successor element is the successor.
- arrowMap_limit (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j) (k : J) (hk : k < i) : arrowMap self.F k i ⋯ hij = arrowι (restrictionLT self.F hij) hi k hk
The iteration on a limit element identifies to the colimit of the value on smaller elements, see
Iteration.isColimit.
Instances For
The iteration on a limit element identifies to the colimit of the value on smaller elements.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The element in Φ.Iteration i that is deduced from an element
in Φ.Iteration j when i ≤ j.
Equations
- iter.trunc hj' = { F := CategoryTheory.SmallObject.restrictionLE iter.F hj', obj_bot := ⋯, arrowSucc_eq := ⋯, arrowMap_limit := ⋯ }
Instances For
Auxiliary definition for the proof of Subsingleton (Φ.Iteration j).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given iter₁ : Φ.Iteration j₁ and iter₂ : Φ.Iteration j₂, with j₁ ≤ j₂,
if k₁ ≤ k₂ are elements such that k₁ ≤ j₁ and k₂ ≤ k₂, then this
is the canonical map iter₁.F.obj ⟨k₁, h₁⟩ ⟶ iter₂.F.obj ⟨k₂, h₂⟩.
Equations
- iter₁.mapObj iter₂ h₁₂ h₁ h₂ hj = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (iter₂.F.map (CategoryTheory.homOfLE h₁₂))