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.

Finally we prove filteredness of a Comma L R and finality of snd L R, given that R is final and A and B are filtered.

References

• M. Kashiwara, P. Schapira, Categories and Sheaves, Lemma 3.4.3 -- 3.4.5

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.{v₂, 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.{v₆, 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.

instance CategoryTheory.Comma.isFiltered_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) [IsFiltered A] [IsFiltered B] [R.Final] : IsFiltered (Comma L R)

Let A and B be filtered categories, R : B ⥤ T be final and L : A ⥤ T. Then, the comma category Comma L R is filtered.

theorem CategoryTheory.Comma.isCofiltered_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) [IsCofiltered A] [IsCofiltered B] [L.Initial] : IsCofiltered (Comma L R)

Let A and B be cofiltered categories, L : A ⥤ T be initial and R : B ⥤ T. Then, the comma category Comma L R is cofiltered.

instance CategoryTheory.Comma.final_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) [IsFiltered A] [IsFiltered B] [R.Final] : (snd L R).Final

Let A and B be filtered categories, R : B ⥤ T be final and R : A ⥤ T. Then, the projection snd L R : Comma L R ⥤ B is final.

instance CategoryTheory.Comma.initial_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) [IsCofiltered A] [IsCofiltered B] [L.Initial] : (fst L R).Initial

Let A and B be cofiltered categories, L : A ⥤ T be initial and R : B ⥤ T. Then, the projection fst L R : Comma L R ⥤ A is initial.