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), (F.cones.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), (F.cocones.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_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)
        @[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 (Opposite.unop F))).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

        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
                  @[simp]
                  theorem CategoryTheory.Limits.Cone.extend_π {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) {X : C} (f : X c.pt) :
                  (c.extend f) = c.extensions.app (Opposite.op X) { down := f }

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

                  Equations
                  • c.extend f = { pt := X, π := c.extensions.app (Opposite.op X) { down := f } }
                  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
                        @[simp]
                        theorem CategoryTheory.Limits.Cocone.extend_ι {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) {Y : C} (f : c.pt Y) :
                        (c.extend f) = c.extensions.app Y { down := f }

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

                        Equations
                        • c.extend f = { pt := Y, ι := c.extensions.app Y { down := f } }
                        Instances For

                          Whisker a cocone by precomposition of a functor. See whiskering for a functorial version.

                          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
                              @[simp]

                              The triangle consisting of the two natural transformations and hom commutes

                              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

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

                                  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

                                                          If F reflects isomorphisms, then Cones.functoriality F reflects isomorphisms as well.

                                                          Equations
                                                          • =

                                                          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
                                                            @[simp]

                                                            The triangle made from the two natural transformations and hom commutes

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

                                                                                        If F reflects isomorphisms, then Cocones.functoriality F reflects isomorphisms as well.

                                                                                        Equations
                                                                                        • =

                                                                                        The image of a cone in C under a functor G : C ⥤ D is a cone in D.

                                                                                        Equations
                                                                                        Instances For

                                                                                          The image of a cocone in C under a functor G : C ⥤ D is a cocone in D.

                                                                                          Equations
                                                                                          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

                                                                                                If H is an equivalence, we invert H.mapCone and get a cone for F from a cone for F ⋙ H.

                                                                                                Equations
                                                                                                Instances For
                                                                                                  noncomputable def CategoryTheory.Functor.mapConeMapConeInv {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J D} (H : CategoryTheory.Functor D C) [H.IsEquivalence] (c : CategoryTheory.Limits.Cone (F.comp H)) :
                                                                                                  H.mapCone (H.mapConeInv c) c

                                                                                                  mapCone is the left inverse to mapConeInv.

                                                                                                  Equations
                                                                                                  Instances For

                                                                                                    MapCone is the right inverse to mapConeInv.

                                                                                                    Equations
                                                                                                    Instances For

                                                                                                      If H is an equivalence, we invert H.mapCone and get a cone for F from a cone for F ⋙ H.

                                                                                                      Equations
                                                                                                      Instances For
                                                                                                        noncomputable def CategoryTheory.Functor.mapCoconeMapCoconeInv {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J D} (H : CategoryTheory.Functor D C) [H.IsEquivalence] (c : CategoryTheory.Limits.Cocone (F.comp H)) :
                                                                                                        H.mapCocone (H.mapCoconeInv c) c

                                                                                                        mapCocone is the left inverse to mapCoconeInv.

                                                                                                        Equations
                                                                                                        Instances For

                                                                                                          mapCocone is the right inverse to mapCoconeInv.

                                                                                                          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 cone on F : Jᵒᵖ ⥤ C to a cocone on F.rightOp : Jᵒᵖ ⥤ C.

                                                                                                                              Equations
                                                                                                                              Instances For

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

                                                                                                                                Equations
                                                                                                                                Instances For

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

                                                                                                                                  Equations
                                                                                                                                  Instances For

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

                                                                                                                                    Equations
                                                                                                                                    Instances For