Library UniMath.ModelCategories.Generated.SmallObjectArgument

The Algebraic Small Object Argument The Algebraic Small Object Argument by Richard Garner is a refinement of the (Classical) Small Object Argument by Quillen. The ASOA can be used to construct a NWFS starting from a sufficiently well-behaved morphism class J. The construction uses a convergent transfinite sequence, the "Free Monoid Sequence". This sequence can be used to construct a monoid in a category, and since a monoid in the LNWFS category is a NWFS, we require some smallness properties on this category and on J to apply it and construct a NWFS. This is done in the files in this directory. A brief description of the files in this directory, all only used to prove the Algebraic Small Object Argument:

• MonoidalHelpers.v: Some helper definitions used throughout the construction.
• LiftingWithClass.v and OneStepMonad.v: One can define a functorial factorization from the morphism class J: the "one step factorization" F1. In fact, this factorization always admits an LNWFS structure, so we denote it with L1 instead.
  This will be the starting point, from which we apply the transfinite construction.
• FFMonoidalStructure.v: Defines a monoidal structure on the category of Functorial Factorizations (FF). This monoidal structure can be lifted to one in LNWFS, and is defined in such a way that a monoid in this structure corresponds with a NWFS. Also a proof that a monoid in this monoidal structure corresponds with an object of RNWFS.
• LNWFSHelpers.v: Useful lemmas related to the LNWFS category, used throughout the construction.
• LNWFSMonoidalStucture.v: Lemmas proving that the monoidal structure on FF in fact lifts to one in LNWFS. Also a proof that a monoid in LNWFS corresponds with an object of NWFS.
• LNWFSCocomplete.v: We show that FF is cocomplete, and that LNWFS is also cocomplete, with colimits lying over those in FF. The main use cases are that LNWFS has all chains and coequalizers, which is necessary for the ASOA.
• LNWFSClosed.v: We show that the monoidal structure on LNWFS is closed under (connected) colimits. Again the main use cases are that it is closed under chains and coequalizers, needed for the ASOA.
• GenericFreeMonoid.v: Theory attempting to construct a free monoid from an adjunction. This is the way Garner initially defines the construction, but I ended up finding it easier to take a more direct approach, constructing the monoid directly. Also definitions for the category of monoid algebras.
• GenericFreeMonoidSequence.v: A file containing the definition of the free monoid sequence, in a monoidal category "V", as well as a proof that it converges, given a smallness requirement on the object "T", defining the sequence. Also contains the construction of the monoid one obtains from the sequence whenever it converges.
• LNWFSSmallnessReduction.v: The smallness requirement on T in V (for which we use L1 in LNWFS), can be reduced to one only depending on the left functor of F1.
• OneStepMonadSmall.v: This smallness requirement that we reduced above can be reduced even further, to one only depending on the morphism class J, used to define F1.
• SmallObjectArgument.v (this file): We put all the above results together, allowing us to construct a NWFS, given a basic smallness requirement on J.

Important sources:

• Cofibrantly generated natural weak factorisation systems by Richard Garner
• Understanding the small object argument by Richard Garner
• My thesis: https://studenttheses.uu.nl/handle/20.500.12932/45658
• A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on by Kelly.