# 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} {α : Type w} (f : αC) :
CProp

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.

• base: ∀ {C : Type u} [inst : ] [inst_1 : ] {α : Type w} {f : αC} (x : α),
• max: ∀ {C : Type u} [inst : ] [inst_1 : ] {α : Type w} {f : αC} {j j' : C},
• coeq: ∀ {C : Type u} [inst : ] [inst_1 : ] {α : Type w} {f : αC} {j j' : C}, ∀ (f_1 f' : j j'),
Instances For

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

Equations
• =

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.

def CategoryTheory.IsFiltered.SmallFilteredIntermediate {C : Type u} {D : Type u₁} [] (F : ) :
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.

Equations
Instances For
noncomputable instance CategoryTheory.IsFiltered.instSmallCategorySmallFilteredIntermediate {C : Type u} {D : Type u₁} [] (F : ) :
Equations
• = let_fun this := inferInstance; this
noncomputable def CategoryTheory.IsFiltered.SmallFilteredIntermediate.factoring {C : Type u} {D : Type u₁} [] (F : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def CategoryTheory.IsFiltered.SmallFilteredIntermediate.inclusion {C : Type u} {D : Type u₁} [] (F : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• = let_fun this := inferInstance; this

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• =
inductive CategoryTheory.IsCofiltered.CofilteredClosure {C : Type u} {α : Type w} (f : αC) :
CProp

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.

• base: ∀ {C : Type u} [inst : ] [inst_1 : ] {α : Type w} {f : αC} (x : α),
• min: ∀ {C : Type u} [inst : ] [inst_1 : ] {α : Type w} {f : αC} {j j' : C},
• eq: ∀ {C : Type u} [inst : ] [inst_1 : ] {α : Type w} {f : αC} {j j' : C}, ∀ (f_1 f' : j j'),
Instances For

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

Equations
• =
Equations
• =
def CategoryTheory.IsCofiltered.SmallCofilteredIntermediate {C : Type u} {D : Type u₁} [] (F : ) :
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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable instance CategoryTheory.IsCofiltered.instSmallCategorySmallCofilteredIntermediate {C : Type u} {D : Type u₁} [] (F : ) :
Equations
• = let_fun this := inferInstance; this
noncomputable def CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.factoring {C : Type u} {D : Type u₁} [] (F : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.inclusion {C : Type u} {D : Type u₁} [] (F : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• = let_fun this := inferInstance; this

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• =