Documentation

Mathlib.CategoryTheory.Filtered.Final

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:

References #

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.

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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [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'), CategoryStruct.comp s (F.map t) = CategoryStruct.comp s' (F.map t)) (d : D) :
theorem CategoryTheory.isCofiltered_costructuredArrow_of_isCofiltered_of_exists {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [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), CategoryStruct.comp (F.map t) s = CategoryStruct.comp (F.map t) s') (d : D) :
theorem CategoryTheory.Functor.final_of_exists_of_isFiltered {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [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'), CategoryStruct.comp s (F.map t) = 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. The converse is also true, see final_iff_of_isFiltered.

The inclusion of a terminal object is final.

The inclusion of the terminal object is final.

theorem CategoryTheory.Functor.initial_of_exists_of_isCofiltered {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [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), CategoryStruct.comp (F.map t) s = 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 final. The converse is also true, see initial_iff_of_isCofiltered.

The inclusion of an initial object is initial.

The inclusion of the initial object is initial.

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

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

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

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

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

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

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

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

Implementation; use Functor.Final.exists_coeq instead.

theorem CategoryTheory.Functor.final_iff_of_isFiltered {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [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'), CategoryStruct.comp s (F.map t) = 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 u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [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), CategoryStruct.comp (F.map t) s = 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 u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [IsFilteredOrEmpty C] [F.Final] {d : D} {c : C} (s s' : d F.obj c) :
∃ (c' : C) (t : c c'), CategoryStruct.comp s (F.map t) = CategoryStruct.comp s' (F.map t)
theorem CategoryTheory.Functor.Initial.exists_eq {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [IsCofilteredOrEmpty C] [F.Initial] {d : D} {c : C} (s s' : F.obj c d) :
∃ (c' : C) (t : c' c), CategoryStruct.comp (F.map t) s = CategoryStruct.comp (F.map t) s'

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

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

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

The diagonal functor on any filtered category is final.

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

The diagonal functor on any cofiltered category is initial.

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

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

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

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

instance CategoryTheory.StructuredArrow.final_map₂_id {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [IsFiltered C] {E : Type u₃} [Category.{v₃, u₃} E] {T : Functor C D} [T.Final] {S : Functor D E} [S.Final] {T' : Functor C E} {d : D} {e : E} (u : e S.obj d) (α : T.comp S T') [IsIso α] :
(map₂ u α).Final

The functor StructuredArrow d T ⥤ StructuredArrow e (T ⋙ S) that u : e ⟶ S.obj d induces via StructuredArrow.map₂ is final, if T and S are final and the domain of T is filtered.

instance CategoryTheory.StructuredArrow.final_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [IsFiltered C] {S S' : D} (f : S S') (T : Functor C D) [T.Final] :

StructuredArrow.map is final if the functor T is final` and its domain is filtered.

instance CategoryTheory.StructuredArrow.final_post {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [IsFiltered C] {E : Type u₃} [Category.{v₃, u₃} E] (X : D) (T : Functor C D) [T.Final] (S : Functor D E) [S.Final] :
(post X T S).Final

StructuredArrow.post X T S is final if T and S are final and the domain of T is filtered.

instance CategoryTheory.CostructuredArrow.initial_map₂_id {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [IsCofiltered C] {E : Type u₃} [Category.{v₃, u₃} E] (T : Functor C D) [T.Initial] (S : Functor D E) [S.Initial] (d : D) (e : E) (u : S.obj d e) :

The functor CostructuredArrow T d ⥤ CostructuredArrow (T ⋙ S) e that u : S.obj d ⟶ e induces via CostructuredArrow.map₂ is initial, if T and S are initial and the domain of T is filtered.

instance CategoryTheory.CostructuredArrow.initial_post {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [IsCofiltered C] {E : Type u₃} [Category.{v₃, u₃} E] (X : D) (T : Functor C D) [T.Initial] (S : Functor D E) [S.Initial] :
(post T S X).Initial

CostructuredArrow.post T S X is initial if T and S are initial and the domain of T is cofiltered.

instance CategoryTheory.final_eval {α : Type u₁} {I : αType u₂} [(s : α) → Category.{v₂, u₂} (I s)] [∀ (s : α), IsFiltered (I s)] (s : α) :
instance CategoryTheory.initial_eval {α : Type u₁} {I : αType u₂} [(s : α) → Category.{v₂, u₂} (I s)] [∀ (s : α), IsCofiltered (I s)] (s : α) :