Finality of Projections in Comma Categories #
We show that fst L R is final if R is and that snd L R is initial if L is.
As a corollary, we show that Comma L R with L : A ⥤ T and R : B ⥤ T is connected if R is
final and A is connected.
References #
- M. Kashiwara, P. Schapira, Categories and Sheaves, Lemma 3.4.3
instance
CategoryTheory.Comma.final_fst
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(L : CategoryTheory.Functor A T)
(R : CategoryTheory.Functor B T)
[R.Final]
:
(CategoryTheory.Comma.fst L R).Final
instance
CategoryTheory.Comma.initial_snd
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(L : CategoryTheory.Functor A T)
(R : CategoryTheory.Functor B T)
[L.Initial]
:
(CategoryTheory.Comma.snd L R).Initial
instance
CategoryTheory.Comma.isConnected_comma_of_final
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(L : CategoryTheory.Functor A T)
(R : CategoryTheory.Functor B T)
[CategoryTheory.IsConnected A]
[R.Final]
:
Comma L R with L : A ⥤ T and R : B ⥤ T is connected if R is final and A is
connected.
instance
CategoryTheory.Comma.isConnected_comma_of_initial
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(L : CategoryTheory.Functor A T)
(R : CategoryTheory.Functor B T)
[CategoryTheory.IsConnected B]
[L.Initial]
:
Comma L R with L : A ⥤ T and R : B ⥤ T is connected if L is initial and B is
connected.