Characterization of connected categories using initial/final functors #
A category C is connected iff the constant functor C ⥤ Discrete PUnit
is final (or initial).
We deduce that the projection C × D ⥤ C is final (or initial) if D is connected.
theorem
CategoryTheory.isConnected_iff_final_of_unique
{C : Type u}
[Category.{v, u} C]
{T : Type w}
[Unique T]
(F : Functor C (Discrete T))
:
theorem
CategoryTheory.isConnected_iff_initial_of_unique
{C : Type u}
[Category.{v, u} C]
{T : Type w}
[Unique T]
(F : Functor C (Discrete T))
:
instance
CategoryTheory.instFinalDiscreteOfIsConnected
{C : Type u}
[Category.{v, u} C]
{T : Type w}
[Unique T]
(F : Functor C (Discrete T))
[IsConnected C]
:
F.Final
instance
CategoryTheory.instInitialDiscreteOfIsConnected
{C : Type u}
[Category.{v, u} C]
{T : Type w}
[Unique T]
(F : Functor C (Discrete T))
[IsConnected C]
:
F.Initial
instance
CategoryTheory.final_fst
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
[IsConnected D]
:
instance
CategoryTheory.final_snd
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
[IsConnected C]
:
instance
CategoryTheory.initial_fst
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
[IsConnected D]
:
instance
CategoryTheory.initial_snd
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
[IsConnected C]
: