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".

See also #

In CategoryTheory.Filtered.Final we give additional equivalent conditions in the case that C is filtered.

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

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).

      Equations
      Instances For

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

        Equations
        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.

          Equations
          Instances For

            Given a cocone over F ⋙ G, we can construct a Cocone G with the same cocone point.

            Equations
            • One or more equations did not get rendered due to their size.
            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.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

                Given a colimit cocone over G : D ⥤ E we can construct a colimit cocone over F ⋙ G.

                Equations
                • One or more equations did not get rendered due to their size.
                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

                  Equations
                  Instances For

                    Given a colimit cocone over F ⋙ G we can construct a colimit cocone over G.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    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.)

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

                      A variant of cofinal_of_colimit_comp_coyoneda_iso_pUnit where we bind the various claims about colimit (F ⋙ coyoneda.obj (Opposite.op d)) for each d : D into a single claim about the presheaf colimit (F ⋙ yoneda).

                      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).

                      Equations
                      • One or more equations did not get rendered due to their size.
                      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.

                        Equations
                        Instances For

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

                          Equations
                          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.

                            Equations
                            Instances For

                              Given a cone over F ⋙ G, we can construct a Cone G with the same cocone point.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              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.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For

                                  Given a limit cone over G : D ⥤ E we can construct a limit cone over F ⋙ G.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  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

                                    Equations
                                    Instances For

                                      Given a limit cone over F ⋙ G we can construct a limit cone over G.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      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.)

                                        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.