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]).
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')
Instances For
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.
Every functor from a small category to a filtered category factors fully faithfully through a small filtered category. This is that category.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
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
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
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')
Instances For
The full subcategory induced by the cofiltered closure of a family is cofiltered.
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
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
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
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.