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.

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.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 : J) :
    (F.cones.map f a✝).app X = CategoryTheory.CategoryStruct.comp f.unop (a✝.app X)

    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.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 : J) :
      (F.cocones.map f a✝).app X = CategoryTheory.CategoryStruct.comp (a✝.app X) f

      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.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 : Cᵒᵖ) (a✝ : (CategoryTheory.yoneda.obj X✝).obj ((CategoryTheory.Functor.const J).op.obj X)) (X✝¹ : J) :
        (((CategoryTheory.cones J C).map f).app X a✝).app X✝¹ = CategoryTheory.CategoryStruct.comp (a✝.app X✝¹) (f.app X✝¹)
        @[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 : J) :
        (((CategoryTheory.cones J C).obj F).map f a✝).app X = CategoryTheory.CategoryStruct.comp f.unop (a✝.app X)

        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
          @[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 : J) :
          (((CategoryTheory.cocones J C).obj F).map f a✝).app X = CategoryTheory.CategoryStruct.comp (a✝.app X) 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 : C) (a✝ : (CategoryTheory.coyoneda.obj X✝).obj ((CategoryTheory.Functor.const J).obj X)) (X✝¹ : J) :
          (((CategoryTheory.cocones J C).map f).app X a✝).app X✝¹ = CategoryTheory.CategoryStruct.comp (f.unop.app X✝¹) (a✝.app X✝¹)

          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

            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
                  • c.extend f = { pt := X, π := c.extensions.app (Opposite.op X) { down := f } }
                  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 }

                    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
                        • c.extend f = { pt := Y, ι := c.extensions.app Y { down := f } }
                        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 }

                          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
                              def CategoryTheory.Limits.Cones.ext {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {c c' : CategoryTheory.Limits.Cone F} (φ : c.pt c'.pt) (w : ∀ (j : J), c.app j = CategoryTheory.CategoryStruct.comp φ.hom (c'.app j) := by aesop_cat) :
                              c c'

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

                              Equations
                              Instances For
                                @[simp]
                                theorem CategoryTheory.Limits.Cones.ext_inv_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {c c' : CategoryTheory.Limits.Cone F} (φ : c.pt c'.pt) (w : ∀ (j : J), c.app j = CategoryTheory.CategoryStruct.comp φ.hom (c'.app j) := by aesop_cat) :
                                (CategoryTheory.Limits.Cones.ext φ w).inv.hom = φ.inv
                                @[simp]
                                theorem CategoryTheory.Limits.Cones.ext_hom_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {c c' : CategoryTheory.Limits.Cone F} (φ : c.pt c'.pt) (w : ∀ (j : J), c.app j = CategoryTheory.CategoryStruct.comp φ.hom (c'.app j) := by aesop_cat) :
                                (CategoryTheory.Limits.Cones.ext φ w).hom.hom = φ.hom

                                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.

                                                          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
                                                            def CategoryTheory.Limits.Cocones.ext {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {c c' : CategoryTheory.Limits.Cocone F} (φ : c.pt c'.pt) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (c.app j) φ.hom = c'.app j := by aesop_cat) :
                                                            c c'

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

                                                            Equations
                                                            Instances For
                                                              @[simp]
                                                              theorem CategoryTheory.Limits.Cocones.ext_inv_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {c c' : CategoryTheory.Limits.Cocone F} (φ : c.pt c'.pt) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (c.app j) φ.hom = c'.app j := by aesop_cat) :
                                                              (CategoryTheory.Limits.Cocones.ext φ w).inv.hom = φ.inv
                                                              @[simp]
                                                              theorem CategoryTheory.Limits.Cocones.ext_hom_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {c c' : CategoryTheory.Limits.Cocone F} (φ : c.pt c'.pt) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (c.app j) φ.hom = c'.app j := by aesop_cat) :
                                                              (CategoryTheory.Limits.Cocones.ext φ w).hom.hom = φ.hom

                                                              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.

                                                                                        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