# mathlibdocumentation

category_theory.limits.shapes.finite_limits

# Categories with finite limits.

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

@[class]
def category_theory.limits.has_finite_limits (C : Type u)  :
Prop

A category has all finite limits if every functor J ⥤ C with a fin_category J instance has a limit.

This is often called 'finitely complete'.

Equations
• = ∀ (J : Type v) [𝒥 : [_inst_2 : ,
Instances
@[instance]

If C has all limits, it has finite limits.

@[class]
def category_theory.limits.has_finite_colimits (C : Type u)  :
Prop

A category has all finite colimits if every functor J ⥤ C with a fin_category J instance has a colimit.

This is often called 'finitely cocomplete'.

Equations
• = ∀ (J : Type v) [𝒥 : [_inst_2 : ,
Instances
@[instance]

If C has all colimits, it has finite colimits.

@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[class]

has_finite_wide_pullbacks represents a choice of wide pullback for every finite collection of morphisms

Equations
• = ∀ (J : Type v) [_inst_2 : [_inst_3 : fintype J],
@[instance]

@[class]

has_finite_wide_pushouts represents a choice of wide pushout for every finite collection of morphisms

Equations
• = ∀ (J : Type v) [_inst_2 : [_inst_3 : fintype J],
@[instance]

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

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

@[instance]

Equations