Commit 2024-03-18 20:42 7ba92d5c

View on Github →

feat(CategoryTheory): construction of a functor for the small object argument (#11056) Given a family of morphisms f i : A i ⟶ B i in a category C and an object S : C, we define a functor SmallObject.functor f S : Over S ⥤ Over S which shall play an important role in the formalization of the "small object argument".

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/SmallObject/Construction.lean

added theorem CategoryTheory.SmallObject.FunctorObjIndex.comm

added structure CategoryTheory.SmallObject.FunctorObjIndex

added theorem CategoryTheory.SmallObject.functorMapSrc_functorObjTop

added theorem CategoryTheory.SmallObject.functorMap_comm

added theorem CategoryTheory.SmallObject.functorMap_id

added theorem CategoryTheory.SmallObject.functorMap_π

added theorem CategoryTheory.SmallObject.functorObj_comm

added theorem CategoryTheory.SmallObject.ιFunctorObj_extension

added theorem CategoryTheory.SmallObject.ιFunctorObj_naturality

added theorem CategoryTheory.SmallObject.ιFunctorObj_πFunctorObj

added theorem CategoryTheory.SmallObject.ι_functorMapSrc

added theorem CategoryTheory.SmallObject.ι_functorMapTgt

added theorem CategoryTheory.SmallObject.ρFunctorObj_π