Documentation

Mathlib.CategoryTheory.Limits.Cones

Cones and cocones #

We define Cone F, a cone over a functor F, and F.cones : Cᵒᵖ ⥤ Type, the functor associating to X the cones over F with cone point X.

A cone c is defined by specifying its cone point c.pt and a natural transformation c.π from the constant c.pt valued functor to F.

We provide c.w f : c.π.app j ≫ F.map f = c.π.app j' for any f : j ⟶ j' as a wrapper for c.π.naturality f avoiding unneeded identity morphisms.

We define c.extend f, where c : cone F and f : Y ⟶ c.pt for some other Y, which replaces the cone point by Y and inserts f into each of the components of the cone. Similarly we have c.whisker F producing a Cone (E ⋙ F)

We define morphisms of cones, and the category of cones.

We define Cone.postcompose α : cone F ⥤ cone G for α a natural transformation F ⟶ G.

And, of course, we dualise all this to cocones as well.

For more results about the category of cones, see cone_category.lean.

@[simp]
theorem CategoryTheory.Functor.cones_map_app {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) :
∀ {X Y : Cᵒᵖ} (f : X Y) (a : (CategoryTheory.yoneda.obj F).obj ((CategoryTheory.Functor.const J).op.obj X)) (X_1 : J), ((CategoryTheory.Functor.cones F).map f a).app X_1 = CategoryTheory.CategoryStruct.comp f.unop (a.app X_1)

If F : J ⥤ C then F.cones is the functor assigning to an object X : C the type of natural transformations from the constant functor with value X to F. An object representing this functor is a limit of F.

Equations
Instances For
    @[simp]
    theorem CategoryTheory.Functor.cocones_map_app {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) :
    ∀ {X Y : C} (f : X Y) (a : (CategoryTheory.coyoneda.obj (Opposite.op F)).obj ((CategoryTheory.Functor.const J).obj X)) (X_1 : J), ((CategoryTheory.Functor.cocones F).map f a).app X_1 = CategoryTheory.CategoryStruct.comp (a.app X_1) f

    If F : J ⥤ C then F.cocones is the functor assigning to an object (X : C) the type of natural transformations from F to the constant functor with value X. An object corepresenting this functor is a colimit of F.

    Equations
    Instances For
      @[simp]
      theorem CategoryTheory.cones_map_app_app (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] :
      ∀ {X Y : CategoryTheory.Functor J C} (f : X Y) (X_1 : Cᵒᵖ) (a : (CategoryTheory.yoneda.obj X).obj ((CategoryTheory.Functor.const J).op.obj X_1)) (X_2 : J), (((CategoryTheory.cones J C).map f).app X_1 a).app X_2 = CategoryTheory.CategoryStruct.comp (a.app X_2) (f.app X_2)
      @[simp]
      theorem CategoryTheory.cones_obj_map_app (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) :
      ∀ {X Y : Cᵒᵖ} (f : X Y) (a : (CategoryTheory.yoneda.obj F).obj ((CategoryTheory.Functor.const J).op.obj X)) (X_1 : J), (((CategoryTheory.cones J C).obj F).map f a).app X_1 = CategoryTheory.CategoryStruct.comp f.unop (a.app X_1)

      Functorially associated to each functor J ⥤ C, we have the C-presheaf consisting of cones with a given cone point.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem CategoryTheory.cocones_obj_map_app (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] (F : (CategoryTheory.Functor J C)ᵒᵖ) :
        ∀ {X Y : C} (f : X Y) (a : (CategoryTheory.coyoneda.obj (Opposite.op F.unop)).obj ((CategoryTheory.Functor.const J).obj X)) (X_1 : J), (((CategoryTheory.cocones J C).obj F).map f a).app X_1 = CategoryTheory.CategoryStruct.comp (a.app X_1) f
        @[simp]
        theorem CategoryTheory.cocones_map_app_app (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] :
        ∀ {X Y : (CategoryTheory.Functor J C)ᵒᵖ} (f : X Y) (X_1 : C) (a : (CategoryTheory.coyoneda.obj X).obj ((CategoryTheory.Functor.const J).obj X_1)) (X_2 : J), (((CategoryTheory.cocones J C).map f).app X_1 a).app X_2 = CategoryTheory.CategoryStruct.comp (f.unop.app X_2) (a.app X_2)

        Contravariantly associated to each functor J ⥤ C, we have the C-copresheaf consisting of cocones with a given cocone point.

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

          A c : Cone F is:

          • an object c.pt and
          • a natural transformation c.π : c.pt ⟶ F from the constant c.pt functor to F.

          Example: if J is a category coming from a poset then the data required to make a term of type Cone F is morphisms πⱼ : c.pt ⟶ F j for all j : J and, for all i ≤ j in J, morphisms πᵢⱼ : F i ⟶ F j such that πᵢ ≫ πᵢⱼ = πᵢ.

          Cone F is equivalent, via cone.equiv below, to Σ X, F.cones.obj X.

          Instances For
            @[simp]

            A c : Cocone F is

            • an object c.pt and
            • a natural transformation c.ι : F ⟶ c.pt from F to the constant c.pt functor.

            For example, if the source J of F is a partially ordered set, then to give c : Cocone F is to give a collection of morphisms ιⱼ : F j ⟶ c.pt and, for all j ≤ k in J, morphisms ιⱼₖ : F j ⟶ F k such that Fⱼₖ ≫ Fₖ = Fⱼ for all j ≤ k.

            Cocone F is equivalent, via Cone.equiv below, to Σ X, F.cocones.obj X.

            Instances For

              The isomorphism between a cone on F and an element of the functor F.cones.

              Equations
              Instances For

                A map to the vertex of a cone induces a cone by composition.

                Equations
                Instances For

                  The isomorphism between a cocone on F and an element of the functor F.cocones.

                  Equations
                  Instances For

                    A map from the vertex of a cocone induces a cocone by composition.

                    Equations
                    Instances For
                      • hom : A.pt B.pt

                        A morphism between the two vertex objects of the cones

                      • w : ∀ (j : J), CategoryTheory.CategoryStruct.comp s.hom (B.app j) = A.app j

                        The triangle consisting of the two natural transformations and hom commutes

                      A cone morphism between two cones for the same diagram is a morphism of the cone points which commutes with the cone legs.

                      Instances For

                        The category of cones on a given diagram.

                        Equations
                        • CategoryTheory.Limits.Cone.category = CategoryTheory.Category.mk

                        To give an isomorphism between cones, it suffices to give an isomorphism between their vertices which commutes with the cone maps.

                        Equations
                        Instances For

                          Given a cone morphism whose object part is an isomorphism, produce an isomorphism of cones.

                          Functorially postcompose a cone for F by a natural transformation F ⟶ G to give a cone for G.

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

                            Postcomposing a cone by the composite natural transformation α ≫ β is the same as postcomposing by α and then by β.

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

                              Postcomposing by the identity does not change the cone up to isomorphism.

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

                                If F and G are naturally isomorphic functors, then they have equivalent categories of cones.

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

                                  Whiskering on the left by E : K ⥤ J gives a functor from Cone F to Cone (E ⋙ F).

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

                                    Whiskering by an equivalence gives an equivalence between categories of cones.

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

                                      The categories of cones over F and G are equivalent if F and G are naturally isomorphic (possibly after changing the indexing category by an equivalence).

                                      Equations
                                      Instances For

                                        Forget the cone structure and obtain just the cone point.

                                        Equations
                                        Instances For

                                          A functor G : C ⥤ D sends cones over F to cones over F ⋙ G functorially.

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

                                            If e : C ≌ D is an equivalence of categories, then functoriality F e.functor induces an equivalence between cones over F and cones over F ⋙ e.functor.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              • hom : A.pt B.pt

                                                A morphism between the (co)vertex objects in C

                                              • w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (A.app j) s.hom = B.app j

                                                The triangle made from the two natural transformations and hom commutes

                                              A cocone morphism between two cocones for the same diagram is a morphism of the cocone points which commutes with the cocone legs.

                                              Instances For

                                                To give an isomorphism between cocones, it suffices to give an isomorphism between their vertices which commutes with the cocone maps.

                                                Equations
                                                Instances For

                                                  Given a cocone morphism whose object part is an isomorphism, produce an isomorphism of cocones.

                                                  Functorially precompose a cocone for F by a natural transformation G ⟶ F to give a cocone for G.

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

                                                    Precomposing a cocone by the composite natural transformation α ≫ β is the same as precomposing by β and then by α.

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

                                                      Precomposing by the identity does not change the cocone up to isomorphism.

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

                                                        If F and G are naturally isomorphic functors, then they have equivalent categories of cocones.

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

                                                          Whiskering on the left by E : K ⥤ J gives a functor from Cocone F to Cocone (E ⋙ F).

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

                                                            Whiskering by an equivalence gives an equivalence between categories of cones.

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

                                                              The categories of cocones over F and G are equivalent if F and G are naturally isomorphic (possibly after changing the indexing category by an equivalence).

                                                              Equations
                                                              Instances For

                                                                Forget the cocone structure and obtain just the cocone point.

                                                                Equations
                                                                Instances For

                                                                  A functor G : C ⥤ D sends cocones over F to cocones over F ⋙ G functorially.

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

                                                                    If e : C ≌ D is an equivalence of categories, then functoriality F e.functor induces an equivalence between cocones over F and cocones over F ⋙ e.functor.

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

                                                                      Given a cone morphism c ⟶ c', construct a cone morphism on the mapped cones functorially.

                                                                      Equations
                                                                      Instances For

                                                                        Given a cocone morphism c ⟶ c', construct a cocone morphism on the mapped cocones functorially.

                                                                        Equations
                                                                        Instances For

                                                                          For F : J ⥤ C, given a cone c : Cone F, and a natural isomorphism α : H ≅ H' for functors H H' : C ⥤ D, the postcomposition of the cone H.mapCone using the isomorphism α is isomorphic to the cone H'.mapCone.

                                                                          Equations
                                                                          Instances For

                                                                            mapCone commutes with postcompose. In particular, for F : J ⥤ C, given a cone c : Cone F, a natural transformation α : F ⟶ G and a functor H : C ⥤ D, we have two obvious ways of producing a cone over G ⋙ H, and they are both isomorphic.

                                                                            Equations
                                                                            Instances For

                                                                              For F : J ⥤ C, given a cocone c : Cocone F, and a natural isomorphism α : H ≅ H' for functors H H' : C ⥤ D, the precomposition of the cocone H.mapCocone using the isomorphism α is isomorphic to the cocone H'.mapCocone.

                                                                              Equations
                                                                              Instances For

                                                                                map_cocone commutes with precompose. In particular, for F : J ⥤ C, given a cocone c : Cocone F, a natural transformation α : F ⟶ G and a functor H : C ⥤ D, we have two obvious ways of producing a cocone over G ⋙ H, and they are both isomorphic.

                                                                                Equations
                                                                                Instances For

                                                                                  The category of cocones on F is equivalent to the opposite category of the category of cones on the opposite of F.

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

                                                                                    Change a cocone on F.leftOp : Jᵒᵖ ⥤ C to a cocone on F : J ⥤ Cᵒᵖ.

                                                                                    Equations
                                                                                    Instances For

                                                                                      Change a cone on F : J ⥤ Cᵒᵖ to a cocone on F.leftOp : Jᵒᵖ ⥤ C.

                                                                                      Equations
                                                                                      Instances For

                                                                                        Change a cone on F.leftOp : Jᵒᵖ ⥤ C to a cocone on F : J ⥤ Cᵒᵖ.

                                                                                        Equations
                                                                                        Instances For

                                                                                          Change a cocone on F : J ⥤ Cᵒᵖ to a cone on F.leftOp : Jᵒᵖ ⥤ C.

                                                                                          Equations
                                                                                          Instances For

                                                                                            Change a cocone on F.rightOp : J ⥤ Cᵒᵖ to a cone on F : Jᵒᵖ ⥤ C.

                                                                                            Equations
                                                                                            Instances For

                                                                                              Change a cone on F : Jᵒᵖ ⥤ C to a cocone on F.rightOp : Jᵒᵖ ⥤ C.

                                                                                              Equations
                                                                                              Instances For

                                                                                                Change a cone on F.rightOp : J ⥤ Cᵒᵖ to a cocone on F : Jᵒᵖ ⥤ C.

                                                                                                Equations
                                                                                                Instances For

                                                                                                  Change a cocone on F : Jᵒᵖ ⥤ C to a cone on F.rightOp : J ⥤ Cᵒᵖ.

                                                                                                  Equations
                                                                                                  Instances For