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.

We then use this in a proof that derives finality of map between two comma categories on a quasi-commutative diagram of functors, some of which need to be final.

References

• M. Kashiwara, P. Schapira, Categories and Sheaves, Lemma 3.4.3 & 3.4.4

instance CategoryTheory.Comma.final_fst {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) [R.Final] : (fst L R).Final

instance CategoryTheory.Comma.initial_snd {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) [L.Initial] : (snd L R).Initial

instance CategoryTheory.Comma.isConnected_comma_of_final {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) [IsConnected A] [R.Final] : IsConnected (Comma L R)

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₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) [IsConnected B] [L.Initial] : IsConnected (Comma L R)

Comma L R with L : A ⥤ T and R : B ⥤ T is connected if L is initial and B is connected.

theorem CategoryTheory.Comma.map_final {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{u₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor A T} {R : Functor B T} {A' : Type u₄} [Category.{v₄, u₄} A'] {B' : Type u₅} [Category.{v₅, u₅} B'] {T' : Type u₂} [Category.{u₂, u₂} T'] {L' : Functor A' T'} {R' : Functor B' T'} {F : Functor A A'} {G : Functor B B'} {H : Functor T T'} (iL : F.comp L' ≅ L.comp H) (iR : G.comp R' ≅ R.comp H) [IsFiltered B] [R.Final] [R'.Final] [F.Final] [G.Final] : (map iL.hom iR.inv).Final

Let the following diagram commute up to isomorphism:

  L       R

A ---→ T ←--- B | | | | F | H | G ↓ ↓ ↓ A' ---→ T' ←--- B' L' R'

Let F, G, R and R' be final and B be filtered. Then, the induced functor between the comma categories of the first and second row of the diagram is final.