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 #

source
def CategoryTheory.Limits.preservesLimitOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J Cᵒᵖ) (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimit K.leftOp F] :
CategoryTheory.Limits.PreservesLimit K F.op

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
    source
    def CategoryTheory.Limits.preservesLimitLeftOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J Cᵒᵖ) (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.PreservesColimit K.leftOp F] :
    CategoryTheory.Limits.PreservesLimit K F.leftOp

    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
      source
      def CategoryTheory.Limits.preservesLimitRightOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C) (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.PreservesColimit K.op F] :
      CategoryTheory.Limits.PreservesLimit K F.rightOp

      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
        source
        def CategoryTheory.Limits.preservesLimitUnop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C) (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.PreservesColimit K.op F] :
        CategoryTheory.Limits.PreservesLimit K (CategoryTheory.Functor.unop F)

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

        Instances For
          source
          def CategoryTheory.Limits.preservesColimitOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J Cᵒᵖ) (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimit K.leftOp F] :
          CategoryTheory.Limits.PreservesColimit K F.op

          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
            source
            def CategoryTheory.Limits.preservesColimitLeftOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J Cᵒᵖ) (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.PreservesLimit K.leftOp F] :
            CategoryTheory.Limits.PreservesColimit K F.leftOp

            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
              source
              def CategoryTheory.Limits.preservesColimitRightOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C) (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.PreservesLimit K.op F] :
              CategoryTheory.Limits.PreservesColimit K F.rightOp

              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
                source
                def CategoryTheory.Limits.preservesColimitUnop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C) (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.PreservesLimit K.op F] :
                CategoryTheory.Limits.PreservesColimit K (CategoryTheory.Functor.unop F)

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

                Instances For
                  source
                  def CategoryTheory.Limits.preservesLimitsOfShapeOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (J : Type w) [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimitsOfShape Jᵒᵖ F] :
                  CategoryTheory.Limits.PreservesLimitsOfShape J F.op

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

                  Instances For
                    source
                    def CategoryTheory.Limits.preservesLimitsOfShapeLeftOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (J : Type w) [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.PreservesColimitsOfShape Jᵒᵖ F] :
                    CategoryTheory.Limits.PreservesLimitsOfShape J F.leftOp

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

                    Instances For
                      source
                      def CategoryTheory.Limits.preservesLimitsOfShapeRightOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (J : Type w) [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.PreservesColimitsOfShape Jᵒᵖ F] :
                      CategoryTheory.Limits.PreservesLimitsOfShape J F.rightOp

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

                      Instances For
                        source
                        def CategoryTheory.Limits.preservesLimitsOfShapeUnop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (J : Type w) [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.PreservesColimitsOfShape Jᵒᵖ F] :
                        CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.Functor.unop F)

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

                        Instances For
                          source
                          def CategoryTheory.Limits.preservesColimitsOfShapeOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (J : Type w) [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimitsOfShape Jᵒᵖ F] :
                          CategoryTheory.Limits.PreservesColimitsOfShape J F.op

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

                          Instances For
                            source
                            def CategoryTheory.Limits.preservesColimitsOfShapeLeftOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (J : Type w) [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.PreservesLimitsOfShape Jᵒᵖ F] :
                            CategoryTheory.Limits.PreservesColimitsOfShape J F.leftOp

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

                            Instances For
                              source
                              def CategoryTheory.Limits.preservesColimitsOfShapeRightOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (J : Type w) [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.PreservesLimitsOfShape Jᵒᵖ F] :
                              CategoryTheory.Limits.PreservesColimitsOfShape J F.rightOp

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

                              Instances For
                                source
                                def CategoryTheory.Limits.preservesColimitsOfShapeUnop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (J : Type w) [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.PreservesLimitsOfShape Jᵒᵖ F] :
                                CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.Functor.unop F)

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

                                Instances For
                                  source
                                  def CategoryTheory.Limits.preservesLimitsOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimits F] :
                                  CategoryTheory.Limits.PreservesLimits F.op

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

                                  Instances For
                                    source
                                    def CategoryTheory.Limits.preservesLimitsLeftOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.PreservesColimits F] :
                                    CategoryTheory.Limits.PreservesLimits F.leftOp

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

                                    Instances For
                                      source
                                      def CategoryTheory.Limits.preservesLimitsRightOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.PreservesColimits F] :
                                      CategoryTheory.Limits.PreservesLimits F.rightOp

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

                                      Instances For
                                        source
                                        def CategoryTheory.Limits.preservesLimitsUnop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.PreservesColimits F] :
                                        CategoryTheory.Limits.PreservesLimits (CategoryTheory.Functor.unop F)

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

                                        Instances For
                                          source
                                          def CategoryTheory.Limits.perservesColimitsOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimits F] :
                                          CategoryTheory.Limits.PreservesColimits F.op

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

                                          Instances For
                                            source
                                            def CategoryTheory.Limits.preservesColimitsLeftOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.PreservesLimits F] :
                                            CategoryTheory.Limits.PreservesColimits F.leftOp

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

                                            Instances For
                                              source
                                              def CategoryTheory.Limits.preservesColimitsRightOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.PreservesLimits F] :
                                              CategoryTheory.Limits.PreservesColimits F.rightOp

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

                                              Instances For
                                                source
                                                def CategoryTheory.Limits.preservesColimitsUnop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.PreservesLimits F] :
                                                CategoryTheory.Limits.PreservesColimits (CategoryTheory.Functor.unop F)

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

                                                Instances For
                                                  source
                                                  def CategoryTheory.Limits.preservesFiniteLimitsOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteColimits F] :
                                                  CategoryTheory.Limits.PreservesFiniteLimits F.op

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

                                                  Instances For
                                                    source
                                                    def CategoryTheory.Limits.preservesFiniteLimitsLeftOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.PreservesFiniteColimits F] :
                                                    CategoryTheory.Limits.PreservesFiniteLimits F.leftOp

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

                                                    Instances For
                                                      source
                                                      def CategoryTheory.Limits.preservesFiniteLimitsRightOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.PreservesFiniteColimits F] :
                                                      CategoryTheory.Limits.PreservesFiniteLimits F.rightOp

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

                                                      Instances For
                                                        source
                                                        def CategoryTheory.Limits.preservesFiniteLimitsUnop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.PreservesFiniteColimits F] :
                                                        CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.Functor.unop F)

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

                                                        Instances For
                                                          source
                                                          def CategoryTheory.Limits.preservesFiniteColimitsOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteLimits F] :
                                                          CategoryTheory.Limits.PreservesFiniteColimits F.op

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

                                                          Instances For
                                                            source
                                                            def CategoryTheory.Limits.preservesFiniteColimitsLeftOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.PreservesFiniteLimits F] :
                                                            CategoryTheory.Limits.PreservesFiniteColimits F.leftOp

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

                                                            Instances For
                                                              source
                                                              def CategoryTheory.Limits.preservesFiniteColimitsRightOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.PreservesFiniteLimits F] :
                                                              CategoryTheory.Limits.PreservesFiniteColimits F.rightOp

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

                                                              Instances For
                                                                source
                                                                def CategoryTheory.Limits.preservesFiniteColimitsUnop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.PreservesFiniteLimits F] :
                                                                CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.Functor.unop F)

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

                                                                Instances For