Final functors with filtered (co)domain #
If C
is a filtered category, then the usual equivalent conditions for a functor F : C ⥤ D
to be
final can be restated. We show:
final_iff_of_isFiltered
: a concrete description of finality which is sometimes a convenient way to show that a functor is final.final_iff_isFiltered_structuredArrow
:F
is final if and only ifStructuredArrow d F
is filtered for alld : D
, which strengthens the usual statement thatF
is final if and only ifStructuredArrow d F
is connected for alld : D
.- Under categories of objects of filtered categories are filtered and their forgetful functors are final.
Additionally, we show that if D
is a filtered category and F : C ⥤ D
is fully faithful and
satisfies the additional condition that for every d : D
there is an object c : D
and a morphism
d ⟶ F.obj c
, then C
is filtered and F
is final.
References #
- [M. Kashiwara, P. Schapira, Categories and Sheaves][Kashiwara2006], Section 3.2
If StructuredArrow d F
is filtered for any d : D
, then F : C ⥤ D
is final. This is
simply because filtered categories are connected. More profoundly, the converse is also true if
C
is filtered, see final_iff_isFiltered_structuredArrow
.
If CostructuredArrow F d
is filtered for any d : D
, then F : C ⥤ D
is initial. This is
simply because cofiltered categories are connectged. More profoundly, the converse is also true
if C
is cofiltered, see initial_iff_isCofiltered_costructuredArrow
.
If C
is filtered, then we can give an explicit condition for a functor F : C ⥤ D
to
be final. The converse is also true, see final_iff_of_isFiltered
.
If C
is cofiltered, then we can give an explicit condition for a functor F : C ⥤ D
to
be final. The converse is also true, see initial_iff_of_isCofiltered
.
In this situation, F
is also final, see
Functor.final_of_exists_of_isFiltered_of_fullyFaithful
.
In this situation, F
is also initial, see
Functor.initial_of_exists_of_isCofiltered_of_fullyFaithful
.
In this situation, F
is also final, see
Functor.final_of_exists_of_isFiltered_of_fullyFaithful
.
In this situation, F
is also initial, see
Functor.initial_of_exists_of_isCofiltered_of_fullyFaithful
.
In this situation, C
is also filtered, see
IsFilteredOrEmpty.of_exists_of_isFiltered_of_fullyFaithful
.
In this situation, C
is also cofiltered, see
IsCofilteredOrEmpty.of_exists_of_isCofiltered_of_fullyFaithful
.
Any under category on a filtered or empty category is filtered. (Note that under categories are always cofiltered since they have an initial object.)
Equations
- ⋯ = ⋯
Any over category on a cofiltered or empty category is cofiltered. (Note that over categories are always filtered since they have a terminal object.)
Equations
- ⋯ = ⋯
The forgetful functor of the under category on any filtered or empty category is final.
Equations
- ⋯ = ⋯
The forgetful functor of the over category on any cofiltered or empty category is initial.
Equations
- ⋯ = ⋯
If C
is filtered, then we can give an explicit condition for a functor F : C ⥤ D
to
be final.
If C
is cofiltered, then we can give an explicit condition for a functor F : C ⥤ D
to
be initial.
If C
is filtered, then F : C ⥤ D
is final if and only if StructuredArrow d F
is filtered
for all d : D
.
If C
is cofiltered, then F : C ⥤ D
is initial if and only if CostructuredArrow F d
is
cofiltered for all d : D
.
If C
is filtered, then the structured arrow category on the diagonal functor C ⥤ C × C
is filtered as well.
Equations
- ⋯ = ⋯
The diagonal functor on any filtered category is final.
Equations
- ⋯ = ⋯
If C
is cofiltered, then the costructured arrow category on the diagonal functor C ⥤ C × C
is cofiltered as well.
Equations
- ⋯ = ⋯
The diagonal functor on any cofiltered category is initial.
Equations
- ⋯ = ⋯
If C
is filtered, then every functor F : C ⥤ Discrete PUnit
is final.
If C
is cofiltered, then every functor F : C ⥤ Discrete PUnit
is initial.