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.
• Under categories of objects of filtered categories are filtered and their forgetful functors are final.
• 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.
• Finality and initiality of diagonal functors diag : C ⥤ C × C and of projection functors of (co)structured arrow categories.

References

• M. Kashiwara, P. Schapira, Categories and Sheaves, 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.

instance CategoryTheory.IsFiltered.under {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.IsFilteredOrEmpty C] (c : C) : CategoryTheory.IsFiltered (CategoryTheory.Under c)

Any under category on a filtered or empty category is filtered. (Note that under categories are always cofiltered since they have an initial object.)

Equations

• ⋯ = ⋯

instance CategoryTheory.IsCofiltered.over {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.IsCofilteredOrEmpty C] (c : C) : CategoryTheory.IsCofiltered (CategoryTheory.Over c)

Any over category on a cofiltered or empty category is cofiltered. (Note that over categories are always filtered since they have a terminal object.)

Equations

• ⋯ = ⋯

instance CategoryTheory.Under.final_forget {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.IsFilteredOrEmpty C] (c : C) : (CategoryTheory.Under.forget c).Final

The forgetful functor of the under category on any filtered or empty category is final.

Equations

• ⋯ = ⋯

instance CategoryTheory.Over.initial_forget {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.IsCofilteredOrEmpty C] (c : C) : (CategoryTheory.Over.forget c).Initial

The forgetful functor of the over category on any cofiltered or empty category is initial.

Equations

• ⋯ = ⋯

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.

instance CategoryTheory.instIsFilteredStructuredArrowProdDiag {C : Type v₁} [CategoryTheory.Category.{v₁, v₁} C] [CategoryTheory.IsFiltered C] (X : C × C) : CategoryTheory.IsFiltered (CategoryTheory.StructuredArrow X (CategoryTheory.Functor.diag C))

If C is filtered, then the structured arrow category on the diagonal functor C ⥤ C × C is filtered as well.

Equations

• ⋯ = ⋯

instance CategoryTheory.Functor.final_diag_of_isFiltered {C : Type v₁} [CategoryTheory.Category.{v₁, v₁} C] [CategoryTheory.IsFiltered C] : (CategoryTheory.Functor.diag C).Final

The diagonal functor on any filtered category is final.

Equations

• ⋯ = ⋯

instance CategoryTheory.instIsCofilteredCostructuredArrowProdDiag {C : Type v₁} [CategoryTheory.Category.{v₁, v₁} C] [CategoryTheory.IsCofiltered C] (X : C × C) : CategoryTheory.IsCofiltered (CategoryTheory.CostructuredArrow (CategoryTheory.Functor.diag C) X)

If C is cofiltered, then the costructured arrow category on the diagonal functor C ⥤ C × C is cofiltered as well.

Equations

• ⋯ = ⋯

instance CategoryTheory.Functor.initial_diag_of_isFiltered {C : Type v₁} [CategoryTheory.Category.{v₁, v₁} C] [CategoryTheory.IsCofiltered C] : (CategoryTheory.Functor.diag C).Initial

The diagonal functor on any cofiltered category is initial.

Equations

• ⋯ = ⋯

theorem CategoryTheory.Functor.final_of_isFiltered_of_pUnit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.IsFiltered C] (F : CategoryTheory.Functor C (CategoryTheory.Discrete PUnit.{u_1 + 1} )) : F.Final

If C is filtered, then every functor F : C ⥤ Discrete PUnit is final.

theorem CategoryTheory.Functor.initial_of_isCofiltered_pUnit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.IsCofiltered C] (F : CategoryTheory.Functor C (CategoryTheory.Discrete PUnit.{u_1 + 1} )) : F.Initial

If C is cofiltered, then every functor F : C ⥤ Discrete PUnit is initial.

instance CategoryTheory.StructuredArrow.final_proj_of_isFiltered {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.IsFilteredOrEmpty C] (T : CategoryTheory.Functor C D) [T.Final] (Y : D) : (CategoryTheory.StructuredArrow.proj Y T).Final

The functor StructuredArrow.proj : StructuredArrow Y T ⥤ C is final if T : C ⥤ D is final and C is filtered.

Equations

• ⋯ = ⋯

instance CategoryTheory.CostructuredArrow.initial_proj_of_isCofiltered {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.IsCofilteredOrEmpty C] (T : CategoryTheory.Functor C D) [T.Initial] (Y : D) : (CategoryTheory.CostructuredArrow.proj T Y).Initial

The functor CostructuredArrow.proj : CostructuredArrow Y T ⥤ C is initial if T : C ⥤ D is initial and C is cofiltered.

Equations

• ⋯ = ⋯