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.

theorem CategoryTheory.Limits.preservesLimit_op {C : Type u₁} [Category C] {D : Type u₂} [Category D] {J : Type w} [Category J] (K : Functor J (Opposite C)) (F : Functor C D) [PreservesColimit K.leftOp F] :

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

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

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

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

theorem CategoryTheory.Limits.preservesLimit_of_leftOp {C : Type u₁} [Category C] {D : Type u₂} [Category D] {J : Type w} [Category J] (K : Functor J C) (F : Functor C (Opposite D)) [PreservesColimit K.op F.leftOp] :

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

theorem CategoryTheory.Limits.preservesLimit_rightOp {C : Type u₁} [Category C] {D : Type u₂} [Category D] {J : Type w} [Category J] (K : Functor J C) (F : Functor (Opposite C) D) [PreservesColimit K.op F] :

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

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

theorem CategoryTheory.Limits.preservesLimit_unop {C : Type u₁} [Category C] {D : Type u₂} [Category D] {J : Type w} [Category J] (K : Functor J C) (F : Functor (Opposite C) (Opposite D)) [PreservesColimit K.op F] :

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

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

theorem CategoryTheory.Limits.preservesColimit_op {C : Type u₁} [Category C] {D : Type u₂} [Category D] {J : Type w} [Category J] (K : Functor J (Opposite C)) (F : Functor C D) [PreservesLimit K.leftOp F] :

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

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

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

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

theorem CategoryTheory.Limits.preservesColimit_of_leftOp {C : Type u₁} [Category C] {D : Type u₂} [Category D] {J : Type w} [Category J] (K : Functor J C) (F : Functor C (Opposite D)) [PreservesLimit K.op F.leftOp] :

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

theorem CategoryTheory.Limits.preservesColimit_rightOp {C : Type u₁} [Category C] {D : Type u₂} [Category D] {J : Type w} [Category J] (K : Functor J C) (F : Functor (Opposite C) D) [PreservesLimit K.op F] :

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

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

theorem CategoryTheory.Limits.preservesColimit_unop {C : Type u₁} [Category C] {D : Type u₂} [Category D] {J : Type w} [Category J] (K : Functor J C) (F : Functor (Opposite C) (Opposite D)) [PreservesLimit K.op F] :

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[deprecated CategoryTheory.Limits.preservesColimits_op (since := "2024-12-25")]

Alias of CategoryTheory.Limits.preservesColimits_op.


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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