Limit creation properties of Functor.op and related constructions

We formulate conditions about F which imply that F.op, F.unop, F.leftOp and F.rightOp create certain (co)limits and vice versa.

@[implicit_reducible]

def CategoryTheory.Limits.createsLimitOp {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) [CreatesColimit K.leftOp F] : CreatesLimit K F.op

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsLimitOfOp {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) [CreatesColimit K.op F.op] : CreatesLimit K F

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsLimitLeftOp {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ᵒᵖ) [CreatesColimit K.leftOp F] : CreatesLimit K F.leftOp

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsLimitOfLeftOp {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ᵒᵖ) [CreatesColimit K.op F.leftOp] : CreatesLimit K F

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsLimitRightOp {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) [CreatesColimit K.op F] : CreatesLimit K F.rightOp

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsLimitOfRightOp {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) [CreatesColimit K.leftOp F.rightOp] : CreatesLimit K F

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsLimitUnop {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ᵒᵖ) [CreatesColimit K.op F] : CreatesLimit K F.unop

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsLimitOfUnop {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ᵒᵖ) [CreatesColimit K.leftOp F.unop] : CreatesLimit K F

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsColimitOp {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) [CreatesLimit K.leftOp F] : CreatesColimit K F.op

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsColimitOfOp {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) [CreatesLimit K.op F.op] : CreatesColimit K F

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsColimitLeftOp {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ᵒᵖ) [CreatesLimit K.leftOp F] : CreatesColimit K F.leftOp

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsColimitOfLeftOp {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ᵒᵖ) [CreatesLimit K.op F.leftOp] : CreatesColimit K F

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsColimitRightOp {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) [CreatesLimit K.op F] : CreatesColimit K F.rightOp

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsColimitOfRightOp {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) [CreatesLimit K.leftOp F.rightOp] : CreatesColimit K F

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsColimitUnop {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ᵒᵖ) [CreatesLimit K.op F] : CreatesColimit K F.unop

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsColimitOfUnop {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ᵒᵖ) [CreatesLimit K.leftOp F.unop] : CreatesColimit K F

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsLimitsOfShapeOp {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) [CreatesColimitsOfShape Jᵒᵖ F] : CreatesLimitsOfShape J F.op

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

Equations

• CategoryTheory.Limits.createsLimitsOfShapeOp J F = { CreatesLimit := fun {K : CategoryTheory.Functor J Cᵒᵖ} => CategoryTheory.Limits.createsLimitOp K F }

@[implicit_reducible]

def CategoryTheory.Limits.createsLimitsOfShapeLeftOp {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ᵒᵖ) [CreatesColimitsOfShape Jᵒᵖ F] : CreatesLimitsOfShape J F.leftOp

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

Equations

• CategoryTheory.Limits.createsLimitsOfShapeLeftOp J F = { CreatesLimit := fun {K : CategoryTheory.Functor J Cᵒᵖ} => CategoryTheory.Limits.createsLimitLeftOp K F }

@[implicit_reducible]

def CategoryTheory.Limits.createsLimitsOfShapeRightOp {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) [CreatesColimitsOfShape Jᵒᵖ F] : CreatesLimitsOfShape J F.rightOp

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

Equations

• CategoryTheory.Limits.createsLimitsOfShapeRightOp J F = { CreatesLimit := fun {K : CategoryTheory.Functor J C} => CategoryTheory.Limits.createsLimitRightOp K F }

@[implicit_reducible]

def CategoryTheory.Limits.createsLimitsOfShapeUnop {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ᵒᵖ) [CreatesColimitsOfShape Jᵒᵖ F] : CreatesLimitsOfShape J F.unop

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

Equations

• CategoryTheory.Limits.createsLimitsOfShapeUnop J F = { CreatesLimit := fun {K : CategoryTheory.Functor J C} => CategoryTheory.Limits.createsLimitUnop K F }

@[implicit_reducible]

def CategoryTheory.Limits.createsColimitsOfShapeOp {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) [CreatesLimitsOfShape Jᵒᵖ F] : CreatesColimitsOfShape J F.op

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

Equations

• CategoryTheory.Limits.createsColimitsOfShapeOp J F = { CreatesColimit := fun {K : CategoryTheory.Functor J Cᵒᵖ} => CategoryTheory.Limits.createsColimitOp K F }

@[implicit_reducible]

def CategoryTheory.Limits.createsColimitsOfShapeLeftOp {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ᵒᵖ) [CreatesLimitsOfShape Jᵒᵖ F] : CreatesColimitsOfShape J F.leftOp

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

Equations

• CategoryTheory.Limits.createsColimitsOfShapeLeftOp J F = { CreatesColimit := fun {K : CategoryTheory.Functor J Cᵒᵖ} => CategoryTheory.Limits.createsColimitLeftOp K F }

@[implicit_reducible]

def CategoryTheory.Limits.createsColimitsOfShapeRightOp {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) [CreatesLimitsOfShape Jᵒᵖ F] : CreatesColimitsOfShape J F.rightOp

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

Equations

• CategoryTheory.Limits.createsColimitsOfShapeRightOp J F = { CreatesColimit := fun {K : CategoryTheory.Functor J C} => CategoryTheory.Limits.createsColimitRightOp K F }

@[implicit_reducible]

def CategoryTheory.Limits.createsColimitsOfShapeUnop {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ᵒᵖ) [CreatesLimitsOfShape Jᵒᵖ F] : CreatesColimitsOfShape J F.unop

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

Equations

• CategoryTheory.Limits.createsColimitsOfShapeUnop J F = { CreatesColimit := fun {K : CategoryTheory.Functor J C} => CategoryTheory.Limits.createsColimitUnop K F }

@[implicit_reducible]

def CategoryTheory.Limits.createsLimitsOfShapeOfOp {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) [CreatesColimitsOfShape Jᵒᵖ F.op] : CreatesLimitsOfShape J F

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

Equations

• CategoryTheory.Limits.createsLimitsOfShapeOfOp J F = { CreatesLimit := fun {K : CategoryTheory.Functor J C} => CategoryTheory.Limits.createsLimitOfOp K F }

@[implicit_reducible]

def CategoryTheory.Limits.createsLimitsOfShapeOfLeftOp {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ᵒᵖ) [CreatesColimitsOfShape Jᵒᵖ F.leftOp] : CreatesLimitsOfShape J F

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

Equations

• CategoryTheory.Limits.createsLimitsOfShapeOfLeftOp J F = { CreatesLimit := fun {K : CategoryTheory.Functor J C} => CategoryTheory.Limits.createsLimitOfLeftOp K F }

@[implicit_reducible]

def CategoryTheory.Limits.createsLimitsOfShapeOfRightOp {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) [CreatesColimitsOfShape Jᵒᵖ F.rightOp] : CreatesLimitsOfShape J F

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

Equations

• CategoryTheory.Limits.createsLimitsOfShapeOfRightOp J F = { CreatesLimit := fun {K : CategoryTheory.Functor J Cᵒᵖ} => CategoryTheory.Limits.createsLimitOfRightOp K F }

@[implicit_reducible]

def CategoryTheory.Limits.createsLimitsOfShapeOfUnop {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ᵒᵖ) [CreatesColimitsOfShape Jᵒᵖ F.unop] : CreatesLimitsOfShape J F

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

Equations

• CategoryTheory.Limits.createsLimitsOfShapeOfUnop J F = { CreatesLimit := fun {K : CategoryTheory.Functor J Cᵒᵖ} => CategoryTheory.Limits.createsLimitOfUnop K F }

@[implicit_reducible]

def CategoryTheory.Limits.createsColimitsOfShapeOfOp {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) [CreatesLimitsOfShape Jᵒᵖ F.op] : CreatesColimitsOfShape J F

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

Equations

• CategoryTheory.Limits.createsColimitsOfShapeOfOp J F = { CreatesColimit := fun {K : CategoryTheory.Functor J C} => CategoryTheory.Limits.createsColimitOfOp K F }

@[implicit_reducible]

def CategoryTheory.Limits.createsColimitsOfShapeOfLeftOp {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ᵒᵖ) [CreatesLimitsOfShape Jᵒᵖ F.leftOp] : CreatesColimitsOfShape J F

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

Equations

• CategoryTheory.Limits.createsColimitsOfShapeOfLeftOp J F = { CreatesColimit := fun {K : CategoryTheory.Functor J C} => CategoryTheory.Limits.createsColimitOfLeftOp K F }

@[implicit_reducible]

def CategoryTheory.Limits.createsColimitsOfShapeOfRightOp {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) [CreatesLimitsOfShape Jᵒᵖ F.rightOp] : CreatesColimitsOfShape J F

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

Equations

• CategoryTheory.Limits.createsColimitsOfShapeOfRightOp J F = { CreatesColimit := fun {K : CategoryTheory.Functor J Cᵒᵖ} => CategoryTheory.Limits.createsColimitOfRightOp K F }

@[implicit_reducible]

def CategoryTheory.Limits.createsColimitsOfShapeOfUnop {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ᵒᵖ) [CreatesLimitsOfShape Jᵒᵖ F.unop] : CreatesColimitsOfShape J F

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

Equations

• CategoryTheory.Limits.createsColimitsOfShapeOfUnop J F = { CreatesColimit := fun {K : CategoryTheory.Functor J Cᵒᵖ} => CategoryTheory.Limits.createsColimitOfUnop K F }

@[implicit_reducible]

def CategoryTheory.Limits.createsLimitsOfSizeOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.op

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsLimitsOfSizeLeftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) [CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.leftOp

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsLimitsOfSizeRightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) [CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.rightOp

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsLimitsOfSizeUnop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) [CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.unop

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsColimitsOfSizeOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.op

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsColimitsOfSizeLeftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) [CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.leftOp

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsColimitsOfSizeRightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) [CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.rightOp

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsColimitsOfSizeUnop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) [CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.unop

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsLimitsOfSizeOfOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.op] : CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsLimitsOfSizeOfLeftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) [CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.leftOp] : CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsLimitsOfSizeOfRightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) [CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.rightOp] : CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsLimitsOfSizeOfUnop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) [CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.unop] : CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsColimitsOfSizeOfOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.op] : CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsColimitsOfSizeOfLeftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) [CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.leftOp] : CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsColimitsOfSizeOfRightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) [CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.rightOp] : CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsColimitsOfSizeOfUnop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) [CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.unop] : CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

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

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev CategoryTheory.Limits.createsLimitsOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [CreatesColimits F] : CreatesLimits F.op

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

Equations

• CategoryTheory.Limits.createsLimitsOp F = CategoryTheory.Limits.createsLimitsOfSizeOp F

@[reducible, inline]

abbrev CategoryTheory.Limits.createsLimitsLeftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) [CreatesColimits F] : CreatesLimits F.leftOp

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

Equations

• CategoryTheory.Limits.createsLimitsLeftOp F = CategoryTheory.Limits.createsLimitsOfSizeLeftOp F

@[reducible, inline]

abbrev CategoryTheory.Limits.createsLimitsRightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) [CreatesColimits F] : CreatesLimits F.rightOp

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

Equations

• CategoryTheory.Limits.createsLimitsRightOp F = CategoryTheory.Limits.createsLimitsOfSizeRightOp F

@[reducible, inline]

abbrev CategoryTheory.Limits.createsLimitsUnop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) [CreatesColimits F] : CreatesLimits F.unop

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

Equations

• CategoryTheory.Limits.createsLimitsUnop F = CategoryTheory.Limits.createsLimitsOfSizeUnop F

@[reducible, inline]

abbrev CategoryTheory.Limits.createsColimitsOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [CreatesLimits F] : CreatesColimits F.op

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

Equations

• CategoryTheory.Limits.createsColimitsOp F = CategoryTheory.Limits.createsColimitsOfSizeOp F

@[reducible, inline]

abbrev CategoryTheory.Limits.createsColimitsLeftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) [CreatesLimits F] : CreatesColimits F.leftOp

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

Equations

• CategoryTheory.Limits.createsColimitsLeftOp F = CategoryTheory.Limits.createsColimitsOfSizeLeftOp F

@[reducible, inline]

abbrev CategoryTheory.Limits.createsColimitsRightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) [CreatesLimits F] : CreatesColimits F.rightOp

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

Equations

• CategoryTheory.Limits.createsColimitsRightOp F = CategoryTheory.Limits.createsColimitsOfSizeRightOp F

@[reducible, inline]

abbrev CategoryTheory.Limits.createsColimitsUnop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) [CreatesLimits F] : CreatesColimits F.unop

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

Equations

• CategoryTheory.Limits.createsColimitsUnop F = CategoryTheory.Limits.createsColimitsOfSizeUnop F

@[reducible, inline]

abbrev CategoryTheory.Limits.createsLimitsOfOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [CreatesColimits F.op] : CreatesLimits F

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

Equations

• CategoryTheory.Limits.createsLimitsOfOp F = CategoryTheory.Limits.createsLimitsOfSizeOfOp F

@[reducible, inline]

abbrev CategoryTheory.Limits.createsLimitsOfLeftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) [CreatesColimits F.leftOp] : CreatesLimits F

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

Equations

• CategoryTheory.Limits.createsLimitsOfLeftOp F = CategoryTheory.Limits.createsLimitsOfSizeOfLeftOp F

@[reducible, inline]

abbrev CategoryTheory.Limits.createsLimitsOfRightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) [CreatesColimits F.rightOp] : CreatesLimits F

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

Equations

• CategoryTheory.Limits.createsLimitsOfRightOp F = CategoryTheory.Limits.createsLimitsOfSizeOfRightOp F

@[reducible, inline]

abbrev CategoryTheory.Limits.createsLimitsOfUnop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) [CreatesColimits F.unop] : CreatesLimits F

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

Equations

• CategoryTheory.Limits.createsLimitsOfUnop F = CategoryTheory.Limits.createsLimitsOfSizeOfUnop F

@[reducible, inline]

abbrev CategoryTheory.Limits.createsColimitsOfOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [CreatesLimits F.op] : CreatesColimits F

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

Equations

• CategoryTheory.Limits.createsColimitsOfOp F = CategoryTheory.Limits.createsColimitsOfSizeOfOp F

@[reducible, inline]

abbrev CategoryTheory.Limits.createsColimitsOfLeftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) [CreatesLimits F.leftOp] : CreatesColimits F

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

Equations

• CategoryTheory.Limits.createsColimitsOfLeftOp F = CategoryTheory.Limits.createsColimitsOfSizeOfLeftOp F

@[reducible, inline]

abbrev CategoryTheory.Limits.createsColimitsOfRightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) [CreatesLimits F.rightOp] : CreatesColimits F

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

Equations

• CategoryTheory.Limits.createsColimitsOfRightOp F = CategoryTheory.Limits.createsColimitsOfSizeOfRightOp F

@[reducible, inline]

abbrev CategoryTheory.Limits.createsColimitsOfUnop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) [CreatesLimits F.unop] : CreatesColimits F

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

Equations

• CategoryTheory.Limits.createsColimitsOfUnop F = CategoryTheory.Limits.createsColimitsOfSizeOfUnop F

@[implicit_reducible]

def CategoryTheory.Limits.createsFiniteLimitsOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [CreatesFiniteColimits F] : CreatesFiniteLimits F.op

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsFiniteLimitsLeftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) [CreatesFiniteColimits F] : CreatesFiniteLimits F.leftOp

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsFiniteLimitsRightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) [CreatesFiniteColimits F] : CreatesFiniteLimits F.rightOp

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsFiniteLimitsUnop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) [CreatesFiniteColimits F] : CreatesFiniteLimits F.unop

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsFiniteColimitsOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [CreatesFiniteLimits F] : CreatesFiniteColimits F.op

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsFiniteColimitsLeftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) [CreatesFiniteLimits F] : CreatesFiniteColimits F.leftOp

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsFiniteColimitsRightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) [CreatesFiniteLimits F] : CreatesFiniteColimits F.rightOp

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsFiniteColimitsUnop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) [CreatesFiniteLimits F] : CreatesFiniteColimits F.unop

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsFiniteLimitsOfOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [CreatesFiniteColimits F.op] : CreatesFiniteLimits F

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsFiniteLimitsOfLeftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) [CreatesFiniteColimits F.leftOp] : CreatesFiniteLimits F

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsFiniteLimitsOfRightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) [CreatesFiniteColimits F.rightOp] : CreatesFiniteLimits F

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsFiniteLimitsOfUnop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) [CreatesFiniteColimits F.unop] : CreatesFiniteLimits F

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsFiniteColimitsOfOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [CreatesFiniteLimits F.op] : CreatesFiniteColimits F

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsFiniteColimitsOfLeftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) [CreatesFiniteLimits F.leftOp] : CreatesFiniteColimits F

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsFiniteColimitsOfRightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) [CreatesFiniteLimits F.rightOp] : CreatesFiniteColimits F

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsFiniteColimitsOfUnop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) [CreatesFiniteLimits F.unop] : CreatesFiniteColimits F

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsFiniteProductsOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [CreatesFiniteCoproducts F] : CreatesFiniteProducts F.op

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

Equations

• CategoryTheory.Limits.createsFiniteProductsOp F = { creates := fun (x : Type) (x_1 : Fintype x) => CategoryTheory.Limits.createsLimitsOfShapeOp (CategoryTheory.Discrete x) F }

@[implicit_reducible]

def CategoryTheory.Limits.createsFiniteProductsLeftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) [CreatesFiniteCoproducts F] : CreatesFiniteProducts F.leftOp

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

Equations

• CategoryTheory.Limits.createsFiniteProductsLeftOp F = { creates := fun (x : Type) (x_1 : Fintype x) => CategoryTheory.Limits.createsLimitsOfShapeLeftOp (CategoryTheory.Discrete x) F }

@[implicit_reducible]

def CategoryTheory.Limits.createsFiniteProductsRightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) [CreatesFiniteCoproducts F] : CreatesFiniteProducts F.rightOp

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

Equations

• CategoryTheory.Limits.createsFiniteProductsRightOp F = { creates := fun (x : Type) (x_1 : Fintype x) => CategoryTheory.Limits.createsLimitsOfShapeRightOp (CategoryTheory.Discrete x) F }

@[implicit_reducible]

def CategoryTheory.Limits.createsFiniteProductsUnop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) [CreatesFiniteCoproducts F] : CreatesFiniteProducts F.unop

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

Equations

• CategoryTheory.Limits.createsFiniteProductsUnop F = { creates := fun (x : Type) (x_1 : Fintype x) => CategoryTheory.Limits.createsLimitsOfShapeUnop (CategoryTheory.Discrete x) F }

@[implicit_reducible]

def CategoryTheory.Limits.createsFiniteCoproductsOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [CreatesFiniteProducts F] : CreatesFiniteCoproducts F.op

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

Equations

• CategoryTheory.Limits.createsFiniteCoproductsOp F = { creates := fun (x : Type) (x_1 : Fintype x) => CategoryTheory.Limits.createsColimitsOfShapeOp (CategoryTheory.Discrete x) F }

@[implicit_reducible]

def CategoryTheory.Limits.createsFiniteCoproductsLeftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) [CreatesFiniteProducts F] : CreatesFiniteCoproducts F.leftOp

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

Equations

• CategoryTheory.Limits.createsFiniteCoproductsLeftOp F = { creates := fun (x : Type) (x_1 : Fintype x) => CategoryTheory.Limits.createsColimitsOfShapeLeftOp (CategoryTheory.Discrete x) F }

@[implicit_reducible]

def CategoryTheory.Limits.createsFiniteCoproductsRightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) [CreatesFiniteProducts F] : CreatesFiniteCoproducts F.rightOp

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def CategoryTheory.Limits.createsFiniteCoproductsUnop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) [CreatesFiniteProducts F] : CreatesFiniteCoproducts F.unop

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

Equations

• CategoryTheory.Limits.createsFiniteCoproductsUnop F = { creates := fun (x : Type) (x_1 : Fintype x) => CategoryTheory.Limits.createsColimitsOfShapeUnop (CategoryTheory.Discrete x) F }