The small object argument

Let C be a category. A class of morphisms I : MorphismProperty C permits the small object argument (typeclass HasSmallObjectArgument.{w} I where w is an auxiliary universe) if there exists a regular cardinal κ : Cardinal.{w} such that IsCardinalForSmallObjectArgument I κ holds. This technical condition is defined in the file Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument. It involves certain smallness conditions relative to w, the existence of certain colimits in C, and for each object A which is the source of a morphism in I, the Hom(A, -) functor (coyoneda.obj (op A)) should commute to transfinite compositions of pushouts of coproducts of morphisms in I (this condition is automatically satisfied for a suitable κ when A is a presentable object of C, see the file Mathlib.CategoryTheory.Presentable.Basic).

Main results

Assuming I permits the small object argument, the two main results obtained in this file are:

• the class I.rlp.llp of morphisms that have the left lifting property with respect to the maps that have the right lifting property with respect to I are exactly the retracts of transfinite compositions (indexed by a suitable well ordered type J) of pushouts of coproducts of morphisms in I;
• morphisms in C have a functorial factorization as a morphism in I.rlp.llp followed by a morphism in I.rlp.

In the context of model categories, these results are known as Quillen's small object argument (originally for J := ℕ). Actually, the more general construction by transfinite induction already appeared in the proof of the existence of enough injectives in abelian categories with AB5 and a generator by Grothendieck, who then wrote that the "proof was essentially known". Indeed, the argument appeared in Homological algebra by Cartan and Eilenberg (p. 9-10) in the case of modules, and they mention that the result was initially obtained by Baer.

Structure of the proof

The main part in the proof is the construction of the functorial factorization. This involves a construction by transfinite induction. A general procedure for constructions by transfinite induction in categories (including the iteration of a functor) is done in the file Mathlib.CategoryTheory.SmallObject.TransfiniteIteration. The factorization of the small object argument is obtained by doing a transfinite iteration of a specific functor Arrow C ⥤ Arrow C which is defined in the file Mathlib.CategoryTheory.SmallObject.Construction (this definition involves coproducts and a pushout). These ingredients are combined in the file Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument where the main results are obtained under a IsCardinalForSmallObjectArgument I κ assumption. The fact that the left lifting property with respect to a class of morphisms is stable by transfinite compositions was obtained in the file Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting.

References

• [Henri Cartan and Samuel Eilenberg, Homological algebra][cartan-eilenberg-1956]
• [Alexander Grothendieck, Sur quelques points d'algèbre homologique][grothendieck-1957]
• [Daniel G. Quillen, Homotopical algebra][Quillen1967]
• https://ncatlab.org/nlab/show/small+object+argument

class CategoryTheory.MorphismProperty.HasSmallObjectArgument {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) : Prop

A class of morphisms I : MorphismProperty C satisfies the property HasSmallObjectArgument.{w} I if it permits the small object argument, i.e. there exists a regular cardinal κ : Cardinal.{w} such that IsCardinalForSmallObjectArgument I κ holds.

• exists_cardinal : ∃ (κ : Cardinal.{w}) (x : Fact κ.IsRegular) (x_1 : OrderBot κ.ord.toType), I.IsCardinalForSmallObjectArgument κ

noncomputable def CategoryTheory.MorphismProperty.smallObjectκ {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) [I.HasSmallObjectArgument] : Cardinal.{w}

When I : MorphismProperty C permits the small object argument, this is a cardinal κ such that IsCardinalForSmallObjectArgument I κ holds.

Equations

• I.smallObjectκ = ⋯.choose

theorem CategoryTheory.MorphismProperty.smallObjectκ_isRegular {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) [I.HasSmallObjectArgument] : Fact I.smallObjectκ.IsRegular

noncomputable instance CategoryTheory.MorphismProperty.instOrderBotToTypeOrdSmallObjectκ {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) [I.HasSmallObjectArgument] : OrderBot I.smallObjectκ.ord.toType

Equations

• I.instOrderBotToTypeOrdSmallObjectκ = ⋯.choose

instance CategoryTheory.MorphismProperty.isCardinalForSmallObjectArgument_smallObjectκ {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) [I.HasSmallObjectArgument] : I.IsCardinalForSmallObjectArgument I.smallObjectκ

instance CategoryTheory.MorphismProperty.instHasFunctorialFactorizationLlpRlp {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) [I.HasSmallObjectArgument] : I.rlp.llp.HasFunctorialFactorization I.rlp

theorem CategoryTheory.MorphismProperty.llp_rlp_of_hasSmallObjectArgument' {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) [I.HasSmallObjectArgument] : I.rlp.llp = ((coproducts.{w, v, u} I).pushouts.transfiniteCompositionsOfShape I.smallObjectκ.ord.toType).retracts

If I : MorphismProperty C permits the small object argument, then the class of morphism that have the left lifting property with respect to the maps that have the right lifting property with respect to I are exactly the retracts of transfinite compositions (indexed by I.smallObjectκ.ord.toType) of pushouts of coproducts of morphisms in C.

theorem CategoryTheory.MorphismProperty.llp_rlp_of_hasSmallObjectArgument {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) [I.HasSmallObjectArgument] : I.rlp.llp = (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} I).pushouts).retracts

If I : MorphismProperty C permits the small object argument, then the class of morphism that have the left lifting property with respect to the maps that have the right lifting property with respect to I are exactly the retracts of transfinite compositions of pushouts of coproducts of morphisms in C.