Categories with finite limits.

A typeclass for categories with all finite (co)limits.

class CategoryTheory.Limits.HasFiniteLimits (C : Type u) [Category.{v, u} C] : Prop

A category has all finite limits if every functor J ⥤ C with a FinCategory J instance and J : Type has a limit.

This is often called 'finitely complete'.

• out (J : Type) [𝒥 : SmallCategory J] [FinCategory J] : HasLimitsOfShape J C

  C has all limits over any type J whose objects and morphisms lie in the same universe and which has FinType objects and morphisms

@[instance 100]

instance CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits (C : Type u) [Category.{v, u} C] [HasFiniteLimits C] (J : Type w) [SmallCategory J] [FinCategory J] : HasLimitsOfShape J C

theorem CategoryTheory.Limits.hasFiniteLimits_of_hasLimitsOfSize (C : Type u) [Category.{v, u} C] [HasLimitsOfSize.{v', u', v, u} C] : HasFiniteLimits C

@[instance 100]

instance CategoryTheory.Limits.hasFiniteLimits_of_hasLimits (C : Type u) [Category.{v, u} C] [HasLimits C] : HasFiniteLimits C

If C has all limits, it has finite limits.

@[instance 90]

instance CategoryTheory.Limits.hasFiniteLimits_of_hasLimitsOfSize₀ (C : Type u) [Category.{v, u} C] [HasLimitsOfSize.{0, 0, v, u} C] : HasFiniteLimits C

@[implicit_reducible]

instance CategoryTheory.Limits.instCategoryULiftHomULiftOfSmallCategory (J : Type) [hJ : SmallCategory J] : Category.{u_1, u_2} (ULiftHom (ULift.{u_2, 0} J))

Equations

• CategoryTheory.Limits.instCategoryULiftHomULiftOfSmallCategory J = CategoryTheory.ULiftHom.category

theorem CategoryTheory.Limits.hasFiniteLimits_of_hasFiniteLimits_of_size (C : Type u) [Category.{v, u} C] (h : ∀ (J : Type w) {𝒥 : SmallCategory J} (x : FinCategory J), HasLimitsOfShape J C) : HasFiniteLimits C

We can always derive HasFiniteLimits C by providing limits at an arbitrary universe.

class CategoryTheory.Limits.HasFiniteColimits (C : Type u) [Category.{v, u} C] : Prop

A category has all finite colimits if every functor J ⥤ C with a FinCategory J instance and J : Type has a colimit.

This is often called 'finitely cocomplete'.

• out (J : Type) [𝒥 : SmallCategory J] [FinCategory J] : HasColimitsOfShape J C

  C has all colimits over any type J whose objects and morphisms lie in the same universe and which has Fintype objects and morphisms

@[instance 100]

instance CategoryTheory.Limits.hasColimitsOfShape_of_hasFiniteColimits (C : Type u) [Category.{v, u} C] [HasFiniteColimits C] (J : Type w) [SmallCategory J] [FinCategory J] : HasColimitsOfShape J C

theorem CategoryTheory.Limits.hasFiniteColimits_of_hasColimitsOfSize (C : Type u) [Category.{v, u} C] [HasColimitsOfSize.{v', u', v, u} C] : HasFiniteColimits C

@[instance 100]

instance CategoryTheory.Limits.hasFiniteColimits_of_hasColimits (C : Type u) [Category.{v, u} C] [HasColimits C] : HasFiniteColimits C

@[instance 90]

instance CategoryTheory.Limits.hasFiniteColimits_of_hasColimitsOfSize₀ (C : Type u) [Category.{v, u} C] [HasColimitsOfSize.{0, 0, v, u} C] : HasFiniteColimits C

theorem CategoryTheory.Limits.hasFiniteColimits_of_hasFiniteColimits_of_size (C : Type u) [Category.{v, u} C] (h : ∀ (J : Type w) {𝒥 : SmallCategory J} (x : FinCategory J), HasColimitsOfShape J C) : HasFiniteColimits C

We can always derive HasFiniteColimits C by providing colimits at an arbitrary universe.

@[implicit_reducible]

instance CategoryTheory.Limits.fintypeWalkingParallelPair : Fintype WalkingParallelPair

Equations

• CategoryTheory.Limits.fintypeWalkingParallelPair = { elems := [CategoryTheory.Limits.WalkingParallelPair.zero, CategoryTheory.Limits.WalkingParallelPair.one].toFinset, complete := ⋯ }

@[implicit_reducible]

noncomputable instance CategoryTheory.Limits.instFintypeWalkingParallelPairHom (j j' : WalkingParallelPair) : Fintype (WalkingParallelPairHom j j')

Equations

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

@[implicit_reducible]

noncomputable instance CategoryTheory.Limits.instFinCategoryWalkingParallelPair : FinCategory WalkingParallelPair

Equations

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

@[implicit_reducible]

instance CategoryTheory.Limits.WidePullbackShape.fintypeObj {J : Type v} [Fintype J] : Fintype (WidePullbackShape J)

Equations

• CategoryTheory.Limits.WidePullbackShape.fintypeObj = { elems := CategoryTheory.Limits.WidePullbackShape.fintypeObj._aux_1, complete := ⋯ }

@[implicit_reducible]

noncomputable instance CategoryTheory.Limits.WidePullbackShape.fintypeHom {J : Type v} (j j' : WidePullbackShape J) : Fintype (j ⟶ j')

Equations

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

@[implicit_reducible]

instance CategoryTheory.Limits.WidePushoutShape.fintypeObj {J : Type v} [Fintype J] : Fintype (WidePushoutShape J)

Equations

• CategoryTheory.Limits.WidePushoutShape.fintypeObj = { elems := CategoryTheory.Limits.WidePushoutShape.fintypeObj._aux_1, complete := ⋯ }

@[implicit_reducible]

noncomputable instance CategoryTheory.Limits.WidePushoutShape.fintypeHom {J : Type v} (j j' : WidePushoutShape J) : Fintype (j ⟶ j')

Equations

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

@[implicit_reducible]

noncomputable instance CategoryTheory.Limits.finCategoryWidePullback {J : Type v} [Fintype J] : FinCategory (WidePullbackShape J)

Equations

• CategoryTheory.Limits.finCategoryWidePullback = { fintypeObj := inferInstance, fintypeHom := CategoryTheory.Limits.WidePullbackShape.fintypeHom }

@[implicit_reducible]

noncomputable instance CategoryTheory.Limits.finCategoryWidePushout {J : Type v} [Fintype J] : FinCategory (WidePushoutShape J)

Equations

• CategoryTheory.Limits.finCategoryWidePushout = { fintypeObj := inferInstance, fintypeHom := CategoryTheory.Limits.WidePushoutShape.fintypeHom }

class CategoryTheory.Limits.HasFiniteWidePullbacks (C : Type u) [Category.{v, u} C] : Prop

A category HasFiniteWidePullbacks if it has all limits of shape WidePullbackShape J for finite J, i.e. if it has a wide pullback for every finite collection of morphisms with the same codomain.

• out (J : Type) [Finite J] : HasLimitsOfShape (WidePullbackShape J) C

  C has all wide pullbacks for any Finite J

instance CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape (C : Type u) [Category.{v, u} C] (J : Type) [Finite J] [HasFiniteWidePullbacks C] : HasLimitsOfShape (WidePullbackShape J) C

class CategoryTheory.Limits.HasFiniteWidePushouts (C : Type u) [Category.{v, u} C] : Prop

A category HasFiniteWidePushouts if it has all colimits of shape WidePushoutShape J for finite J, i.e. if it has a wide pushout for every finite collection of morphisms with the same domain.

• out (J : Type) [Finite J] : HasColimitsOfShape (WidePushoutShape J) C

  C has all wide pushouts for any Finite J

instance CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape (C : Type u) [Category.{v, u} C] (J : Type) [Finite J] [HasFiniteWidePushouts C] : HasColimitsOfShape (WidePushoutShape J) C

@[instance 900]

instance CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits (C : Type u) [Category.{v, u} C] [HasFiniteLimits C] : HasFiniteWidePullbacks C

Finite wide pullbacks are finite limits, so if C has all finite limits, it also has finite wide pullbacks

@[instance 900]

instance CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits (C : Type u) [Category.{v, u} C] [HasFiniteColimits C] : HasFiniteWidePushouts C

Finite wide pushouts are finite colimits, so if C has all finite colimits, it also has finite wide pushouts

@[implicit_reducible]

instance CategoryTheory.Limits.fintypeWalkingPair : Fintype WalkingPair

Equations

• CategoryTheory.Limits.fintypeWalkingPair = { elems := {CategoryTheory.Limits.WalkingPair.left, CategoryTheory.Limits.WalkingPair.right}, complete := ⋯ }