Documentation

Mathlib.CategoryTheory.Limits.Final

Final and initial functors #

A functor F : C ⥤ D is final if for every d : D, the comma category of morphisms d ⟶ F.obj c is connected.

Dually, a functor F : C ⥤ D is initial if for every d : D, the comma category of morphisms F.obj c ⟶ d is connected.

We show that right adjoints are examples of final functors, while left adjoints are examples of initial functors.

For final functors, we prove that the following three statements are equivalent:

  1. F : C ⥤ D is final.
  2. Every functor G : D ⥤ E has a colimit if and only if F ⋙ G does, and these colimits are isomorphic via colimit.pre G F.
  3. colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.

Starting at 1. we show (in coconesEquiv) that the categories of cocones over G : D ⥤ E and over F ⋙ G are equivalent. (In fact, via an equivalence which does not change the cocone point.) This readily implies 2., as comp_hasColimit, hasColimit_of_comp, and colimitIso.

From 2. we can specialize to G = coyoneda.obj (op d) to obtain 3., as colimitCompCoyonedaIso.

From 3., we prove 1. directly in cofinal_of_colimit_comp_coyoneda_iso_pUnit.

Dually, we prove that if a functor F : C ⥤ D is initial, then any functor G : D ⥤ E has a limit if and only if F ⋙ G does, and these limits are isomorphic via limit.pre G F.

Naming #

There is some discrepancy in the literature about naming; some say 'cofinal' instead of 'final'. The explanation for this is that the 'co' prefix here is not the usual category-theoretic one indicating duality, but rather indicating the sense of "along with".

Future work #

Dualise condition 3 above and the implications 2 ⇒ 3 and 3 ⇒ 1 to initial functors.

References #

A functor F : C ⥤ D is final if for every d : D, the comma category of morphisms d ⟶ F.obj c is connected.

See https://stacks.math.columbia.edu/tag/04E6

Instances

    A functor F : C ⥤ D is initial if for every d : D, the comma category of morphisms F.obj c ⟶ d is connected.

    Instances

      If a functor R : D ⥤ C is a right adjoint, it is final.

      If a functor L : C ⥤ D is a left adjoint, it is initial.

      When F : C ⥤ D is cofinal, we denote by lift F d an arbitrary choice of object in C such that there exists a morphism d ⟶ F.obj (lift F d).

      Instances For

        When F : C ⥤ D is cofinal, we denote by homToLift an arbitrary choice of morphism d ⟶ F.obj (lift F d).

        Instances For
          def CategoryTheory.Functor.Final.induction {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Final F] {d : D} (Z : (X : C) → (d F.obj X) → Sort u_1) (h₁ : (X₁ X₂ : C) → (k₁ : d F.obj X₁) → (k₂ : d F.obj X₂) → (f : X₁ X₂) → CategoryTheory.CategoryStruct.comp k₁ (F.map f) = k₂Z X₁ k₁Z X₂ k₂) (h₂ : (X₁ X₂ : C) → (k₁ : d F.obj X₁) → (k₂ : d F.obj X₂) → (f : X₁ X₂) → CategoryTheory.CategoryStruct.comp k₁ (F.map f) = k₂Z X₂ k₂Z X₁ k₁) {X₀ : C} {k₀ : d F.obj X₀} (z : Z X₀ k₀) :

          We provide an induction principle for reasoning about lift and homToLift. We want to perform some construction (usually just a proof) about the particular choices lift F d and homToLift F d, it suffices to perform that construction for some other pair of choices (denoted X₀ : C and k₀ : d ⟶ F.obj X₀ below), and to show how to transport such a construction both directions along a morphism between such choices.

          Instances For

            If F is cofinal, the category of cocones on F ⋙ G is equivalent to the category of cocones on G, for any G : D ⥤ E.

            Instances For

              When F is cofinal, and t : Cocone (F ⋙ G), extendCocone.obj t is a colimit cocone exactly when t is.

              Instances For

                When F : C ⥤ D is cofinal, and G : D ⥤ E has a colimit, then F ⋙ G has a colimit also and colimit (F ⋙ G) ≅ colimit G

                https://stacks.math.columbia.edu/tag/04E7

                Instances For

                  When F is cofinal, and F ⋙ G has a colimit, then G has a colimit also.

                  We can't make this an instance, because F is not determined by the goal. (Even if this weren't a problem, it would cause a loop with comp_hasColimit.)

                  When F is cofinal, and F ⋙ G has a colimit, then G has a colimit also and colimit (F ⋙ G) ≅ colimit G

                  https://stacks.math.columbia.edu/tag/04E7

                  Instances For

                    If colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit for all d : D, then F is cofinal.

                    If the universal morphism colimit (F ⋙ coyoneda.obj (op d)) ⟶ colimit (coyoneda.obj (op d)) is an isomorphism (as it always is when F is cofinal), then colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit (simply because colimit (coyoneda.obj (op d)) ≅ PUnit).

                    Instances For

                      When F : C ⥤ D is initial, we denote by lift F d an arbitrary choice of object in C such that there exists a morphism F.obj (lift F d) ⟶ d.

                      Instances For

                        When F : C ⥤ D is initial, we denote by homToLift an arbitrary choice of morphism F.obj (lift F d) ⟶ d.

                        Instances For
                          def CategoryTheory.Functor.Initial.induction {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Initial F] {d : D} (Z : (X : C) → (F.obj X d) → Sort u_1) (h₁ : (X₁ X₂ : C) → (k₁ : F.obj X₁ d) → (k₂ : F.obj X₂ d) → (f : X₁ X₂) → CategoryTheory.CategoryStruct.comp (F.map f) k₂ = k₁Z X₁ k₁Z X₂ k₂) (h₂ : (X₁ X₂ : C) → (k₁ : F.obj X₁ d) → (k₂ : F.obj X₂ d) → (f : X₁ X₂) → CategoryTheory.CategoryStruct.comp (F.map f) k₂ = k₁Z X₂ k₂Z X₁ k₁) {X₀ : C} {k₀ : F.obj X₀ d} (z : Z X₀ k₀) :

                          We provide an induction principle for reasoning about lift and homToLift. We want to perform some construction (usually just a proof) about the particular choices lift F d and homToLift F d, it suffices to perform that construction for some other pair of choices (denoted X₀ : C and k₀ : F.obj X₀ ⟶ d below), and to show how to transport such a construction both directions along a morphism between such choices.

                          Instances For

                            If F is initial, the category of cones on F ⋙ G is equivalent to the category of cones on G, for any G : D ⥤ E.

                            Instances For

                              When F is initial, and t : Cone (F ⋙ G), extendCone.obj t is a limit cone exactly when t is.

                              Instances For

                                When F : C ⥤ D is initial, and G : D ⥤ E has a limit, then F ⋙ G has a limit also and limit (F ⋙ G) ≅ limit G

                                https://stacks.math.columbia.edu/tag/04E7

                                Instances For

                                  When F is initial, and F ⋙ G has a limit, then G has a limit also.

                                  We can't make this an instance, because F is not determined by the goal. (Even if this weren't a problem, it would cause a loop with comp_hasLimit.)

                                  When F is initial, and F ⋙ G has a limit, then G has a limit also and limit (F ⋙ G) ≅ limit G

                                  https://stacks.math.columbia.edu/tag/04E7

                                  Instances For

                                    Final functors preserve filteredness.

                                    This can be seen as a generalization of IsFiltered.of_right_adjoint (which states that right adjoints preserve filteredness), as right adjoints are always final, see final_of_adjunction.

                                    Final functors preserve filteredness.

                                    This can be seen as a generalization of IsFiltered.of_right_adjoint (which states that right adjoints preserve filteredness), as right adjoints are always final, see final_of_adjunction.

                                    Initial functors preserve cofilteredness.

                                    This can be seen as a generalization of IsCofiltered.of_left_adjoint (which states that left adjoints preserve cofilteredness), as right adjoints are always initial, see intial_of_adjunction.

                                    Initial functors preserve cofilteredness.

                                    This can be seen as a generalization of IsCofiltered.of_left_adjoint (which states that left adjoints preserve cofilteredness), as right adjoints are always initial, see intial_of_adjunction.