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.
- If
D
is a filtered category andF : C ⥤ D
is fully faithful and satisfies the additional condition that for everyd : D
there is an objectc : D
and a morphismd ⟶ F.obj c
, thenC
is filtered andF
is final. - Finality and initiality of diagonal functors
diag : C ⥤ C × C
and of projection functors of (co)structured arrow categories. - Finality of
StructuredArrow.post
, given the finality of its arguments.
References #
- M. Kashiwara, P. Schapira, Categories and Sheaves, 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
.
The inclusion of a terminal object is final.
The inclusion of the terminal object is final.
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
.
The inclusion of an initial object is initial.
The inclusion of the initial object is initial.
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.)
Any over category on a cofiltered or empty category is cofiltered. (Note that over categories are always filtered since they have a terminal object.)
The forgetful functor of the under category on any filtered or empty category is final.
The forgetful functor of the over category on any cofiltered or empty category is initial.
Implementation; use Functor.Final.exists_coeq instead
.
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.
The diagonal functor on any filtered category is final.
If C
is cofiltered, then the costructured arrow category on the diagonal functor C ⥤ C × C
is cofiltered as well.
The diagonal functor on any cofiltered category is initial.
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.
The functor StructuredArrow.proj : StructuredArrow Y T ⥤ C
is final if T : C ⥤ D
is final
and C
is filtered.
The functor CostructuredArrow.proj : CostructuredArrow Y T ⥤ C
is initial if T : C ⥤ D
is
initial and C
is cofiltered.
The functor StructuredArrow d T ⥤ StructuredArrow e (T ⋙ S)
that u : e ⟶ S.obj d
induces via StructuredArrow.map₂
is final, if T
and S
are final and the domain of T
is
filtered.
StructuredArrow.map
is final if the functor T
is final` and its domain is filtered.
StructuredArrow.post X T S
is final if T
and S
are final and the domain of T
is
filtered.
The functor CostructuredArrow T d ⥤ CostructuredArrow (T ⋙ S) e
that u : S.obj d ⟶ e
induces via CostructuredArrow.map₂
is initial, if T
and S
are initial and the domain of T
is
filtered.
CostructuredArrow.post T S X
is initial if T
and S
are initial and the domain of T
is
cofiltered.