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

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

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

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

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

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

                        Equations
                        Instances For

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

                          • hom : A.pt B.pt

                            A morphism between the two vertex objects of the cones

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

                            The triangle consisting of the two natural transformations and hom commutes

                          Instances For

                            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.

                              There is a morphism from an extended cone to the original cone.

                              Equations
                              Instances For

                                A cone extended by an isomorphism is isomorphic to the original cone.

                                Equations
                                Instances For

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

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

                                                      • hom : A.pt B.pt

                                                        A morphism between the (co)vertex objects in C

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

                                                        The triangle made from the two natural transformations and hom commutes

                                                      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.

                                                          There is a morphism from a cocone to its extension.

                                                          Equations
                                                          Instances For

                                                            Extending a cocone by a composition is the same as extending the cone twice.

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

                                                              A cocone extended by an isomorphism is isomorphic to the original cone.

                                                              Equations
                                                              Instances For

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