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.leftOp and F.rightOp preserve certain (co)limits and vice versa.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

source
theorem CategoryTheory.Limits.preservesLimitsOfSize_op {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] :
PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.op

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

source
theorem CategoryTheory.Limits.preservesLimitsOfSize_leftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) [PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] :
PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.leftOp

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

source
theorem CategoryTheory.Limits.preservesLimitsOfSize_rightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) [PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] :
PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.rightOp

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

source
theorem CategoryTheory.Limits.preservesLimitsOfSize_unop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) [PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] :
PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.unop

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

source
theorem CategoryTheory.Limits.preservesColimitsOfSize_op {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] :
PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.op

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

source
theorem CategoryTheory.Limits.preservesColimitsOfSize_leftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) [PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] :
PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.leftOp

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

source
theorem CategoryTheory.Limits.preservesColimitsOfSize_rightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) [PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] :
PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.rightOp

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

source
theorem CategoryTheory.Limits.preservesColimitsOfSize_unop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) [PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] :
PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.unop

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

source
theorem CategoryTheory.Limits.preservesLimitsOfSize_of_op {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.op] :
PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

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

source
theorem CategoryTheory.Limits.preservesLimitsOfSize_of_leftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) [PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.leftOp] :
PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

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

source
theorem CategoryTheory.Limits.preservesLimitsOfSize_of_rightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) [PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.rightOp] :
PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

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

source
theorem CategoryTheory.Limits.preservesLimitsOfSize_of_unop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) [PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.unop] :
PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

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

source
theorem CategoryTheory.Limits.preservesColimitsOfSize_of_op {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.op] :
PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

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

source
theorem CategoryTheory.Limits.preservesColimitsOfSize_of_leftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) [PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.leftOp] :
PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

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

source
theorem CategoryTheory.Limits.preservesColimitsOfSize_of_rightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) [PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.rightOp] :
PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

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

source
theorem CategoryTheory.Limits.preservesColimitsOfSize_of_unop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) [PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.unop] :
PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

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

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

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

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

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

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

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

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

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

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

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

source
@[deprecated CategoryTheory.Limits.preservesColimits_op (since := "2024-12-25")]
theorem CategoryTheory.Limits.perservesColimits_op {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [PreservesLimits F] :
PreservesColimits F.op

Alias of CategoryTheory.Limits.preservesColimits_op.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

source
theorem CategoryTheory.Limits.preservesFiniteProducts_op {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [PreservesFiniteCoproducts F] :
PreservesFiniteProducts F.op

If F : C ⥤ D preserves finite coproducts, then F.op : Cᵒᵖ ⥤ Dᵒᵖ preserves finite products.

source
theorem CategoryTheory.Limits.preservesFiniteProducts_leftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) [PreservesFiniteCoproducts F] :
PreservesFiniteProducts F.leftOp

If F : C ⥤ Dᵒᵖ preserves finite coproducts, then F.leftOp : Cᵒᵖ ⥤ D preserves finite products.

source
theorem CategoryTheory.Limits.preservesFiniteProducts_rightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) [PreservesFiniteCoproducts F] :
PreservesFiniteProducts F.rightOp

If F : Cᵒᵖ ⥤ D preserves finite coproducts, then F.rightOp : C ⥤ Dᵒᵖ preserves finite products.

source
theorem CategoryTheory.Limits.preservesFiniteProducts_unop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) [PreservesFiniteCoproducts F] :
PreservesFiniteProducts F.unop

If F : Cᵒᵖ ⥤ Dᵒᵖ preserves finite coproducts, then F.unop : C ⥤ D preserves finite products.

source
theorem CategoryTheory.Limits.preservesFiniteCoproducts_op {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [PreservesFiniteProducts F] :
PreservesFiniteCoproducts F.op

If F : C ⥤ D preserves finite products, then F.op : Cᵒᵖ ⥤ Dᵒᵖ preserves finite coproducts.

source
theorem CategoryTheory.Limits.preservesFiniteCoproducts_leftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) [PreservesFiniteProducts F] :
PreservesFiniteCoproducts F.leftOp

If F : C ⥤ Dᵒᵖ preserves finite products, then F.leftOp : Cᵒᵖ ⥤ D preserves finite coproducts.

source
theorem CategoryTheory.Limits.preservesFiniteCoproducts_rightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) [PreservesFiniteProducts F] :
PreservesFiniteCoproducts F.rightOp

If F : Cᵒᵖ ⥤ D preserves finite products, then F.rightOp : C ⥤ Dᵒᵖ preserves finite coproducts.

source
theorem CategoryTheory.Limits.preservesFiniteCoproducts_unop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) [PreservesFiniteProducts F] :
PreservesFiniteCoproducts F.unop

If F : Cᵒᵖ ⥤ Dᵒᵖ preserves finite products, then F.unop : C ⥤ D preserves finite coproducts.