A functor from a small category to a filtered category factors through a small filtered category

A consequence of this is that if C is filtered and finally small, then C is also "finally filtered-small", i.e., there is a final functor from a small filtered category to C. This is occasionally useful, for example in the proof of the recognition theorem for ind-objects (Proposition 6.1.5 in [Kashiwara2006]).

inductive CategoryTheory.IsFiltered.FilteredClosure {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {α : Type w} (f : α → C) : C → Prop

• base: ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFilteredOrEmpty C] {α : Type w} {f : α → C} (x : α), CategoryTheory.IsFiltered.FilteredClosure f (f x)
• max: ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFilteredOrEmpty C] {α : Type w} {f : α → C} {j j' : C}, CategoryTheory.IsFiltered.FilteredClosure f j → CategoryTheory.IsFiltered.FilteredClosure f j' → CategoryTheory.IsFiltered.FilteredClosure f (CategoryTheory.IsFiltered.max j j')
• coeq: ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFilteredOrEmpty C] {α : Type w} {f : α → C} {j j' : C}, CategoryTheory.IsFiltered.FilteredClosure f j → CategoryTheory.IsFiltered.FilteredClosure f j' → ∀ (f_1 f' : j ⟶ j'), CategoryTheory.IsFiltered.FilteredClosure f (CategoryTheory.IsFiltered.coeq f_1 f')

The "filtered closure" of an α-indexed family of objects in C is the set of objects in C obtained by starting with the family and successively adding maxima and coequalizers.

instance CategoryTheory.IsFiltered.instIsFilteredOrEmptyFullSubcategoryFilteredClosureCategory {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {α : Type w} (f : α → C) : CategoryTheory.IsFilteredOrEmpty (CategoryTheory.FullSubcategory (CategoryTheory.IsFiltered.FilteredClosure f))

The full subcategory induced by the filtered closure of a family of objects is filtered.

Our goal for this section is to show that the size of the filtered closure of an α-indexed family of objects in C only depends on the size of α and the morphism types of C, not on the size of the objects of C. More precisely, if α lives in Type w, the objects of C live in Type u and the morphisms of C live in Type v, then we want Small.{max v w} (FullSubcategory (FilteredClosure f)).

The strategy is to define a type `AbstractFilteredClosure` which should be an inductive type
similar to `FilteredClosure`, which lives in the correct universe and surjects onto the full
subcategory. The difficulty with this is that we need to define it at the same time as the map
`AbstractFilteredClosure → C`, as the coequalizer constructor depends on the actual morphisms
in `C`. This would require some kind of inductive-recursive definition, which Lean does not
allow. Our solution is to define a function `ℕ → Σ t : Type (max v w), t → C` by (strong)
induction and then take the union over all natural numbers, mimicking what one would do in a
set-theoretic setting.  

theorem CategoryTheory.IsFiltered.small_fullSubcategory_filteredClosure {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {α : Type w} (f : α → C) : Small.{max v w, u} (CategoryTheory.FullSubcategory (CategoryTheory.IsFiltered.FilteredClosure f))

instance CategoryTheory.IsFiltered.instEssentiallySmallFullSubcategoryFilteredClosureCategory {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {α : Type w} (f : α → C) : CategoryTheory.EssentiallySmall (CategoryTheory.FullSubcategory (CategoryTheory.IsFiltered.FilteredClosure f))

def CategoryTheory.IsFiltered.SmallFilteredIntermediate {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C) : Type (max u₁ v)

Every functor from a small category to a filtered category factors fully faithfully through a small filtered category. This is that category.

noncomputable instance CategoryTheory.IsFiltered.instSmallCategorySmallFilteredIntermediate {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C) : CategoryTheory.SmallCategory (CategoryTheory.IsFiltered.SmallFilteredIntermediate F)

noncomputable def CategoryTheory.IsFiltered.SmallFilteredIntermediate.factoring {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C) : CategoryTheory.Functor D (CategoryTheory.IsFiltered.SmallFilteredIntermediate F)

The first part of a factoring of a functor from a small category to a filtered category through a small filtered category.

noncomputable def CategoryTheory.IsFiltered.SmallFilteredIntermediate.inclusion {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C) : CategoryTheory.Functor (CategoryTheory.IsFiltered.SmallFilteredIntermediate F) C

The second, fully faithful part of a factoring of a functor from a small category to a filtered category through a small filtered category.

instance CategoryTheory.IsFiltered.SmallFilteredIntermediate.instFaithfulSmallFilteredIntermediateInstSmallCategorySmallFilteredIntermediateInclusion {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C) : CategoryTheory.Faithful (CategoryTheory.IsFiltered.SmallFilteredIntermediate.inclusion F)

noncomputable instance CategoryTheory.IsFiltered.SmallFilteredIntermediate.instFullSmallFilteredIntermediateInstSmallCategorySmallFilteredIntermediateInclusion {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C) : CategoryTheory.Full (CategoryTheory.IsFiltered.SmallFilteredIntermediate.inclusion F)

noncomputable def CategoryTheory.IsFiltered.SmallFilteredIntermediate.factoringCompInclusion {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C) : CategoryTheory.Functor.comp (CategoryTheory.IsFiltered.SmallFilteredIntermediate.factoring F) (CategoryTheory.IsFiltered.SmallFilteredIntermediate.inclusion F) ≅ F

The factorization through a small filtered category is in fact a factorization, up to natural isomorphism.

instance CategoryTheory.IsFiltered.SmallFilteredIntermediate.instIsFilteredOrEmptySmallFilteredIntermediateInstSmallCategorySmallFilteredIntermediate {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C) : CategoryTheory.IsFilteredOrEmpty (CategoryTheory.IsFiltered.SmallFilteredIntermediate F)

instance CategoryTheory.IsFiltered.SmallFilteredIntermediate.instIsFilteredSmallFilteredIntermediateInstSmallCategorySmallFilteredIntermediate {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C) [Nonempty D] : CategoryTheory.IsFiltered (CategoryTheory.IsFiltered.SmallFilteredIntermediate F)

inductive CategoryTheory.IsCofiltered.CofilteredClosure {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {α : Type w} (f : α → C) : C → Prop

• base: ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofilteredOrEmpty C] {α : Type w} {f : α → C} (x : α), CategoryTheory.IsCofiltered.CofilteredClosure f (f x)
• min: ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofilteredOrEmpty C] {α : Type w} {f : α → C} {j j' : C}, CategoryTheory.IsCofiltered.CofilteredClosure f j → CategoryTheory.IsCofiltered.CofilteredClosure f j' → CategoryTheory.IsCofiltered.CofilteredClosure f (CategoryTheory.IsCofiltered.min j j')
• eq: ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofilteredOrEmpty C] {α : Type w} {f : α → C} {j j' : C}, CategoryTheory.IsCofiltered.CofilteredClosure f j → CategoryTheory.IsCofiltered.CofilteredClosure f j' → ∀ (f_1 f' : j ⟶ j'), CategoryTheory.IsCofiltered.CofilteredClosure f (CategoryTheory.IsCofiltered.eq f_1 f')

The "cofiltered closure" of an α-indexed family of objects in C is the set of objects in C obtained by starting with the family and successively adding minima and equalizers.

instance CategoryTheory.IsCofiltered.instIsCofilteredOrEmptyFullSubcategoryCofilteredClosureCategory {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {α : Type w} (f : α → C) : CategoryTheory.IsCofilteredOrEmpty (CategoryTheory.FullSubcategory (CategoryTheory.IsCofiltered.CofilteredClosure f))

The full subcategory induced by the cofiltered closure of a family is cofiltered.

theorem CategoryTheory.IsCofiltered.small_fullSubcategory_cofilteredClosure {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {α : Type w} (f : α → C) : Small.{max v w, u} (CategoryTheory.FullSubcategory (CategoryTheory.IsCofiltered.CofilteredClosure f))

instance CategoryTheory.IsCofiltered.instEssentiallySmallFullSubcategoryCofilteredClosureCategory {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {α : Type w} (f : α → C) : CategoryTheory.EssentiallySmall (CategoryTheory.FullSubcategory (CategoryTheory.IsCofiltered.CofilteredClosure f))

def CategoryTheory.IsCofiltered.SmallCofilteredIntermediate {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C) : Type (max u₁ v)

Every functor from a small category to a cofiltered category factors fully faithfully through a small cofiltered category. This is that category.

noncomputable instance CategoryTheory.IsCofiltered.instSmallCategorySmallCofilteredIntermediate {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C) : CategoryTheory.SmallCategory (CategoryTheory.IsCofiltered.SmallCofilteredIntermediate F)

noncomputable def CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.factoring {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C) : CategoryTheory.Functor D (CategoryTheory.IsCofiltered.SmallCofilteredIntermediate F)

The first part of a factoring of a functor from a small category to a cofiltered category through a small filtered category.

noncomputable def CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.inclusion {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C) : CategoryTheory.Functor (CategoryTheory.IsCofiltered.SmallCofilteredIntermediate F) C

The second, fully faithful part of a factoring of a functor from a small category to a filtered category through a small filtered category.

instance CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.instFaithfulSmallCofilteredIntermediateInstSmallCategorySmallCofilteredIntermediateInclusion {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C) : CategoryTheory.Faithful (CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.inclusion F)

noncomputable instance CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.instFullSmallCofilteredIntermediateInstSmallCategorySmallCofilteredIntermediateInclusion {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C) : CategoryTheory.Full (CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.inclusion F)

noncomputable def CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.factoringCompInclusion {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C) : CategoryTheory.Functor.comp (CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.factoring F) (CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.inclusion F) ≅ F

The factorization through a small filtered category is in fact a factorization, up to natural isomorphism.

instance CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.instIsCofilteredOrEmptySmallCofilteredIntermediateInstSmallCategorySmallCofilteredIntermediate {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C) : CategoryTheory.IsCofilteredOrEmpty (CategoryTheory.IsCofiltered.SmallCofilteredIntermediate F)

instance CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.instIsCofilteredSmallCofilteredIntermediateInstSmallCategorySmallCofilteredIntermediate {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C) [Nonempty D] : CategoryTheory.IsCofiltered (CategoryTheory.IsCofiltered.SmallCofilteredIntermediate F)