Documentation

Mathlib.CategoryTheory.Limits.Preserves.Opposites

Limit preservation properties of functor.op and related constructions #

We formulate conditions about F which imply that F.op, F.unop, F.left_op and F.right_op preserve certain (co)limits.

Future work #

If F : C ⥤ D preserves colimits of K.left_op : Jᵒᵖ ⥤ C, then F.op : Cᵒᵖ ⥤ Dᵒᵖ preserves limits of K : J ⥤ Cᵒᵖ.

Instances For

    If F : C ⥤ Dᵒᵖ preserves colimits of K.left_op : Jᵒᵖ ⥤ C, then F.left_op : Cᵒᵖ ⥤ D preserves limits of K : J ⥤ Cᵒᵖ.

    Instances For

      If F : Cᵒᵖ ⥤ D preserves colimits of K.op : Jᵒᵖ ⥤ Cᵒᵖ, then F.right_op : C ⥤ Dᵒᵖ preserves limits of K : J ⥤ C.

      Instances For

        If F : Cᵒᵖ ⥤ Dᵒᵖ preserves colimits of K.op : Jᵒᵖ ⥤ Cᵒᵖ, then F.unop : C ⥤ D preserves limits of K : J ⥤ C.

        Instances For

          If F : C ⥤ D preserves limits of K.left_op : Jᵒᵖ ⥤ C, then F.op : Cᵒᵖ ⥤ Dᵒᵖ preserves colimits of K : J ⥤ Cᵒᵖ.

          Instances For

            If F : C ⥤ Dᵒᵖ preserves limits of K.left_op : Jᵒᵖ ⥤ C, then F.left_op : Cᵒᵖ ⥤ D preserves colimits of K : J ⥤ Cᵒᵖ.

            Instances For

              If F : Cᵒᵖ ⥤ D preserves limits of K.op : Jᵒᵖ ⥤ Cᵒᵖ, then F.right_op : C ⥤ Dᵒᵖ preserves colimits of K : J ⥤ C.

              Instances For

                If F : Cᵒᵖ ⥤ Dᵒᵖ preserves limits of K.op : Jᵒᵖ ⥤ Cᵒᵖ, then F.unop : C ⥤ D preserves colimits of K : J ⥤ C.

                Instances For

                  If F : C ⥤ D preserves colimits of shape Jᵒᵖ, then F.op : Cᵒᵖ ⥤ Dᵒᵖ preserves limits of shape J.

                  Instances For

                    If F : C ⥤ Dᵒᵖ preserves colimits of shape Jᵒᵖ, then F.left_op : Cᵒᵖ ⥤ D preserves limits of shape J.

                    Instances For

                      If F : Cᵒᵖ ⥤ D preserves colimits of shape Jᵒᵖ, then F.right_op : C ⥤ Dᵒᵖ preserves limits of shape J.

                      Instances For

                        If F : C ⥤ D preserves limits of shape Jᵒᵖ, then F.op : Cᵒᵖ ⥤ Dᵒᵖ preserves colimits of shape J.

                        Instances For

                          If F : C ⥤ Dᵒᵖ preserves limits of shape Jᵒᵖ, then F.left_op : Cᵒᵖ ⥤ D preserves colimits of shape J.

                          Instances For

                            If F : Cᵒᵖ ⥤ D preserves limits of shape Jᵒᵖ, then F.right_op : C ⥤ Dᵒᵖ preserves colimits of shape J.

                            Instances For

                              If F : C ⥤ D preserves colimits, then F.op : Cᵒᵖ ⥤ Dᵒᵖ preserves limits.

                              Instances For

                                If F : C ⥤ Dᵒᵖ preserves colimits, then F.left_op : Cᵒᵖ ⥤ D preserves limits.

                                Instances For

                                  If F : Cᵒᵖ ⥤ D preserves colimits, then F.right_op : C ⥤ Dᵒᵖ preserves limits.

                                  Instances For

                                    If F : C ⥤ D preserves limits, then F.op : Cᵒᵖ ⥤ Dᵒᵖ preserves colimits.

                                    Instances For

                                      If F : C ⥤ Dᵒᵖ preserves limits, then F.left_op : Cᵒᵖ ⥤ D preserves colimits.

                                      Instances For

                                        If F : Cᵒᵖ ⥤ D preserves limits, then F.right_op : C ⥤ Dᵒᵖ preserves colimits.

                                        Instances For

                                          If F : C ⥤ D preserves finite colimits, then F.op : Cᵒᵖ ⥤ Dᵒᵖ preserves finite limits.

                                          Instances For

                                            If F : C ⥤ Dᵒᵖ preserves finite colimits, then F.left_op : Cᵒᵖ ⥤ D preserves finite limits.

                                            Instances For

                                              If F : Cᵒᵖ ⥤ D preserves finite colimits, then F.right_op : C ⥤ Dᵒᵖ preserves finite limits.

                                              Instances For

                                                If F : C ⥤ D preserves finite limits, then F.op : Cᵒᵖ ⥤ Dᵒᵖ preserves finite colimits.

                                                Instances For

                                                  If F : C ⥤ Dᵒᵖ preserves finite limits, then F.left_op : Cᵒᵖ ⥤ D preserves finite colimits.

                                                  Instances For

                                                    If F : Cᵒᵖ ⥤ D preserves finite limits, then F.right_op : C ⥤ Dᵒᵖ preserves finite colimits.

                                                    Instances For