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

      @[instance 100]
      Equations
      • =
      @[instance 100]
      Equations
      • =

      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) [F.Final] {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
            @[simp]
            theorem CategoryTheory.Functor.Final.extendCocone_map_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [F.Final] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor D E} :
            ∀ {X Y : CategoryTheory.Limits.Cocone (F.comp G)} (f : X Y), (CategoryTheory.Functor.Final.extendCocone.map f).hom = f.hom
            @[simp]
            theorem CategoryTheory.Functor.Final.extendCocone_obj_pt {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [F.Final] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor D E} (c : CategoryTheory.Limits.Cocone (F.comp G)) :
            (CategoryTheory.Functor.Final.extendCocone.obj c).pt = c.pt

            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

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

                    theorem CategoryTheory.Functor.Final.zigzag_of_eqvGen_quot_rel {C : Type v} [CategoryTheory.Category.{v, v} C] {D : Type u₁} [CategoryTheory.Category.{v, u₁} D] {F : CategoryTheory.Functor C D} {d : D} {f₁ : (X : C) × (d F.obj X)} {f₂ : (X : C) × (d F.obj X)} (t : EqvGen (CategoryTheory.Limits.Types.Quot.Rel (F.comp (CategoryTheory.coyoneda.obj (Opposite.op d)))) f₁ f₂) :

                    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) [F.Initial] {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
                            @[simp]
                            theorem CategoryTheory.Functor.Initial.extendCone_map_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [F.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor D E} :
                            ∀ {X Y : CategoryTheory.Limits.Cone (F.comp G)} (f : X Y), (CategoryTheory.Functor.Initial.extendCone.map f).hom = f.hom
                            @[simp]
                            theorem CategoryTheory.Functor.Initial.extendCone_obj_pt {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [F.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor D E} (c : CategoryTheory.Limits.Cone (F.comp G)) :
                            (CategoryTheory.Functor.Initial.extendCone.obj c).pt = c.pt

                            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

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

                                    The hypotheses also imply that G is final, see final_of_comp_full_faithful'.

                                    The hypotheses also imply that G is initial, see initial_of_comp_full_faithful'.

                                    See also the strictly more general final_comp below.

                                    See also the strictly more general initial_comp below.

                                    See also the strictly more general final_comp below.

                                    See also the strictly more general inital_comp below.

                                    See also the strictly more general final_of_final_comp below.

                                    See also the strictly more general initial_of_initial_comp below.

                                    See also the strictly more general final_iff_final_comp below.

                                    See also the strictly more general initial_iff_initial_comp below.

                                    Equations
                                    • =
                                    Equations
                                    • =

                                    The hypotheses also imply that F is final, see final_of_comp_full_faithful.

                                    The hypotheses also imply that F is initial, see initial_of_comp_full_faithful.

                                    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.