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 if StructuredArrow d F is filtered for all d : D, which strengthens the usual statement that F is final if and only if StructuredArrow d F is connected for all d : D.

Additionally, we show that if D is a filtered category and F : C ⥤ D is fully faithful and satisfies the additional condition that for every d : D there is an object c : D and a morphism d ⟶ F.obj c, then C is filtered and F is final.

References

• [M. Kashiwara, P. Schapira, Categories and Sheaves][Kashiwara2006], Section 3.2

theorem CategoryTheory.Functor.final_of_isFiltered_structuredArrow {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [∀ (d : D), CategoryTheory.IsFiltered (CategoryTheory.StructuredArrow d F)] : F.Final

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.

theorem CategoryTheory.Functor.initial_of_isCofiltered_costructuredArrow {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [∀ (d : D), CategoryTheory.IsCofiltered (CategoryTheory.CostructuredArrow F d)] : F.Initial

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.

theorem CategoryTheory.isFiltered_structuredArrow_of_isFiltered_of_exists {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsFilteredOrEmpty C] (h₁ : ∀ (d : D), ∃ (c : C), Nonempty (d ⟶ F.obj c)) (h₂ : ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ (c' : C) (t : c ⟶ c'), CategoryTheory.CategoryStruct.comp s (F.map t) = CategoryTheory.CategoryStruct.comp s' (F.map t)) (d : D) : CategoryTheory.IsFiltered (CategoryTheory.StructuredArrow d F)

theorem CategoryTheory.isCofiltered_costructuredArrow_of_isCofiltered_of_exists {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsCofilteredOrEmpty C] (h₁ : ∀ (d : D), ∃ (c : C), Nonempty (F.obj c ⟶ d)) (h₂ : ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ (c' : C) (t : c' ⟶ c), CategoryTheory.CategoryStruct.comp (F.map t) s = CategoryTheory.CategoryStruct.comp (F.map t) s') (d : D) : CategoryTheory.IsCofiltered (CategoryTheory.CostructuredArrow F d)

theorem CategoryTheory.Functor.final_of_exists_of_isFiltered {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsFilteredOrEmpty C] (h₁ : ∀ (d : D), ∃ (c : C), Nonempty (d ⟶ F.obj c)) (h₂ : ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ (c' : C) (t : c ⟶ c'), CategoryTheory.CategoryStruct.comp s (F.map t) = CategoryTheory.CategoryStruct.comp s' (F.map t)) : F.Final

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.

theorem CategoryTheory.Functor.initial_of_exists_of_isCofiltered {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsCofilteredOrEmpty C] (h₁ : ∀ (d : D), ∃ (c : C), Nonempty (F.obj c ⟶ d)) (h₂ : ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ (c' : C) (t : c' ⟶ c), CategoryTheory.CategoryStruct.comp (F.map t) s = CategoryTheory.CategoryStruct.comp (F.map t) s') : F.Initial

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.

theorem CategoryTheory.IsFilteredOrEmpty.of_exists_of_isFiltered_of_fullyFaithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsFilteredOrEmpty D] [F.Full] [F.Faithful] (h : ∀ (d : D), ∃ (c : C), Nonempty (d ⟶ F.obj c)) : CategoryTheory.IsFilteredOrEmpty C

In this situation, F is also final, see Functor.final_of_exists_of_isFiltered_of_fullyFaithful.

theorem CategoryTheory.IsCofilteredOrEmpty.of_exists_of_isCofiltered_of_fullyFaithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsCofilteredOrEmpty D] [F.Full] [F.Faithful] (h : ∀ (d : D), ∃ (c : C), Nonempty (F.obj c ⟶ d)) : CategoryTheory.IsCofilteredOrEmpty C

In this situation, F is also initial, see Functor.initial_of_exists_of_isCofiltered_of_fullyFaithful.

theorem CategoryTheory.IsFiltered.of_exists_of_isFiltered_of_fullyFaithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsFiltered D] [F.Full] [F.Faithful] (h : ∀ (d : D), ∃ (c : C), Nonempty (d ⟶ F.obj c)) : CategoryTheory.IsFiltered C

In this situation, F is also final, see Functor.final_of_exists_of_isFiltered_of_fullyFaithful.

theorem CategoryTheory.IsCofiltered.of_exists_of_isCofiltered_of_fullyFaithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsCofiltered D] [F.Full] [F.Faithful] (h : ∀ (d : D), ∃ (c : C), Nonempty (F.obj c ⟶ d)) : CategoryTheory.IsCofiltered C

In this situation, F is also initial, see Functor.initial_of_exists_of_isCofiltered_of_fullyFaithful.

theorem CategoryTheory.Functor.final_of_exists_of_isFiltered_of_fullyFaithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsFilteredOrEmpty D] [F.Full] [F.Faithful] (h : ∀ (d : D), ∃ (c : C), Nonempty (d ⟶ F.obj c)) : F.Final

In this situation, C is also filtered, see IsFilteredOrEmpty.of_exists_of_isFiltered_of_fullyFaithful.

theorem CategoryTheory.Functor.initial_of_exists_of_isCofiltered_of_fullyFaithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsCofilteredOrEmpty D] [F.Full] [F.Faithful] (h : ∀ (d : D), ∃ (c : C), Nonempty (F.obj c ⟶ d)) : F.Initial

In this situation, C is also cofiltered, see IsCofilteredOrEmpty.of_exists_of_isCofiltered_of_fullyFaithful.

theorem CategoryTheory.Functor.final_iff_of_isFiltered {C : Type v₁} [CategoryTheory.Category.{v₁, v₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsFilteredOrEmpty C] : F.Final ↔ (∀ (d : D), ∃ (c : C), Nonempty (d ⟶ F.obj c)) ∧ ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ (c' : C) (t : c ⟶ c'), CategoryTheory.CategoryStruct.comp s (F.map t) = CategoryTheory.CategoryStruct.comp s' (F.map t)

If C is filtered, then we can give an explicit condition for a functor F : C ⥤ D to be final.

theorem CategoryTheory.Functor.initial_iff_of_isCofiltered {C : Type v₁} [CategoryTheory.Category.{v₁, v₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsCofilteredOrEmpty C] : F.Initial ↔ (∀ (d : D), ∃ (c : C), Nonempty (F.obj c ⟶ d)) ∧ ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ (c' : C) (t : c' ⟶ c), CategoryTheory.CategoryStruct.comp (F.map t) s = CategoryTheory.CategoryStruct.comp (F.map t) s'

If C is cofiltered, then we can give an explicit condition for a functor F : C ⥤ D to be initial.

theorem CategoryTheory.Functor.Final.exists_coeq {C : Type v₁} [CategoryTheory.Category.{v₁, v₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsFilteredOrEmpty C] [F.Final] {d : D} {c : C} (s : d ⟶ F.obj c) (s' : d ⟶ F.obj c) : ∃ (c' : C) (t : c ⟶ c'), CategoryTheory.CategoryStruct.comp s (F.map t) = CategoryTheory.CategoryStruct.comp s' (F.map t)

theorem CategoryTheory.Functor.Initial.exists_eq {C : Type v₁} [CategoryTheory.Category.{v₁, v₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsCofilteredOrEmpty C] [F.Initial] {d : D} {c : C} (s : F.obj c ⟶ d) (s' : F.obj c ⟶ d) : ∃ (c' : C) (t : c' ⟶ c), CategoryTheory.CategoryStruct.comp (F.map t) s = CategoryTheory.CategoryStruct.comp (F.map t) s'

theorem CategoryTheory.Functor.final_iff_isFiltered_structuredArrow {C : Type v₁} [CategoryTheory.Category.{v₁, v₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsFilteredOrEmpty C] : F.Final ↔ ∀ (d : D), CategoryTheory.IsFiltered (CategoryTheory.StructuredArrow d F)

If C is filtered, then F : C ⥤ D is final if and only if StructuredArrow d F is filtered for all d : D.

theorem CategoryTheory.Functor.initial_iff_isCofiltered_costructuredArrow {C : Type v₁} [CategoryTheory.Category.{v₁, v₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsCofilteredOrEmpty C] : F.Initial ↔ ∀ (d : D), CategoryTheory.IsCofiltered (CategoryTheory.CostructuredArrow F d)

If C is cofiltered, then F : C ⥤ D is initial if and only if CostructuredArrow F d is cofiltered for all d : D.