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.

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.

    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.

      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.

        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.

              Instances For

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

                Instances For

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

                  Instances For

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

                    Instances For

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

                      Instances For

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

                        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

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

                            Instances For

                              Eta rule for cones.

                              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.

                                Instances For

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

                                  Instances For

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

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

                                      Instances For

                                        Forget the cone structure and obtain just the cone point.

                                        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.

                                          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.

                                              Instances For

                                                Eta rule for cocones.

                                                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.

                                                  Instances For

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

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

                                                      Instances For

                                                        Forget the cocone structure and obtain just the cocone point.

                                                        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.

                                                          Instances For

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

                                                            Instances For

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

                                                              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.

                                                                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.

                                                                  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.

                                                                    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.

                                                                      Instances For

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

                                                                        Instances For

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

                                                                          Instances For

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

                                                                            Instances For

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

                                                                              Instances For

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

                                                                                Instances For

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

                                                                                  Instances For

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

                                                                                    Instances For

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

                                                                                      Instances For

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

                                                                                        Instances For

                                                                                          The opposite cocone of the image of a cone is the image of the opposite cocone.

                                                                                          Instances For

                                                                                            The opposite cone of the image of a cocone is the image of the opposite cone.

                                                                                            Instances For