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 [KS06]).

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

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} [Category.{v, u} C] [IsFilteredOrEmpty C] {α : Type w} {f : α → C} (x : α) : filteredClosure f (f x)
• max {C : Type u} [Category.{v, u} C] [IsFilteredOrEmpty C] {α : Type w} {f : α → C} {j j' : C} : filteredClosure f j → filteredClosure f j' → filteredClosure f (IsFiltered.max j j')
• coeq {C : Type u} [Category.{v, u} C] [IsFilteredOrEmpty C] {α : Type w} {f : α → C} {j j' : C} : filteredClosure f j → filteredClosure f j' → ∀ (f✝ f' : j ⟶ j'), filteredClosure f (IsFiltered.coeq f✝ f')

@[deprecated CategoryTheory.IsFiltered.filteredClosure (since := "2025-03-05")]

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

Alias of CategoryTheory.IsFiltered.filteredClosure.

---

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.

Equations

• @CategoryTheory.IsFiltered.FilteredClosure = @CategoryTheory.IsFiltered.filteredClosure

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

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} [Category.{v, u} C] [IsFilteredOrEmpty C] {α : Type w} (f : α → C) : Small.{max v w, u} (filteredClosure f).FullSubcategory

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

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

Equations

• CategoryTheory.IsFiltered.SmallFilteredIntermediate F = CategoryTheory.SmallModel.{max ?u.32 ?u.35, ?u.35, ?u.33} (CategoryTheory.IsFiltered.filteredClosure F.obj).FullSubcategory

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

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.IsFiltered.SmallFilteredIntermediate.factoring {C : Type u} [Category.{v, u} C] [IsFilteredOrEmpty C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor D C) : Functor D (SmallFilteredIntermediate 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.

noncomputable def CategoryTheory.IsFiltered.SmallFilteredIntermediate.inclusion {C : Type u} [Category.{v, u} C] [IsFilteredOrEmpty C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor D C) : Functor (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.

Equations

• One or more equations did not get rendered due to their size.

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

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

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

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.

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

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

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

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} [Category.{v, u} C] [IsCofilteredOrEmpty C] {α : Type w} {f : α → C} (x : α) : cofilteredClosure f (f x)
• min {C : Type u} [Category.{v, u} C] [IsCofilteredOrEmpty C] {α : Type w} {f : α → C} {j j' : C} : cofilteredClosure f j → cofilteredClosure f j' → cofilteredClosure f (IsCofiltered.min j j')
• eq {C : Type u} [Category.{v, u} C] [IsCofilteredOrEmpty C] {α : Type w} {f : α → C} {j j' : C} : cofilteredClosure f j → cofilteredClosure f j' → ∀ (f✝ f' : j ⟶ j'), cofilteredClosure f (IsCofiltered.eq f✝ f')

@[deprecated CategoryTheory.IsCofiltered.cofilteredClosure (since := "2025-03-05")]

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

Alias of CategoryTheory.IsCofiltered.cofilteredClosure.

---

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.

Equations

• @CategoryTheory.IsCofiltered.CofilteredClosure = @CategoryTheory.IsCofiltered.cofilteredClosure

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

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

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

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

def CategoryTheory.IsCofiltered.SmallCofilteredIntermediate {C : Type u} [Category.{v, u} C] [IsCofilteredOrEmpty C] {D : Type u₁} [Category.{v₁, u₁} D] (F : 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.

Equations

• CategoryTheory.IsCofiltered.SmallCofilteredIntermediate F = CategoryTheory.SmallModel.{max ?u.32 ?u.35, ?u.35, ?u.33} (CategoryTheory.IsCofiltered.cofilteredClosure F.obj).FullSubcategory

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

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.factoring {C : Type u} [Category.{v, u} C] [IsCofilteredOrEmpty C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor D C) : Functor D (SmallCofilteredIntermediate 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.

noncomputable def CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.inclusion {C : Type u} [Category.{v, u} C] [IsCofilteredOrEmpty C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor D C) : Functor (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.

Equations

• One or more equations did not get rendered due to their size.

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

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

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

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.

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

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