# mathlibdocumentation

category_theory.limits.shapes.finite_limits

# Categories with finite limits. #

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

@[class]
structure category_theory.limits.has_finite_limits (C : Type u)  :
Prop
• out : ∀ (J : Type) [𝒥 : [_inst_2 : ,

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

This is often called 'finitely complete'.

Instances of this typeclass
@[protected, instance]
@[protected, instance]
@[protected, instance]

If C has all limits, it has finite limits.

theorem category_theory.limits.has_finite_limits_of_has_finite_limits_of_size (C : Type u) (h : ∀ (J : Type w) {𝒥 : , ) :

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

@[class]
structure category_theory.limits.has_finite_colimits (C : Type u)  :
Prop
• out : ∀ (J : Type) [𝒥 : [_inst_2 : ,

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

This is often called 'finitely cocomplete'.

Instances of this typeclass
@[protected, instance]
@[protected, instance]
theorem category_theory.limits.has_finite_colimits_of_has_finite_colimits_of_size (C : Type u) (h : ∀ (J : Type w) {𝒥 : , ) :

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

@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
noncomputable def category_theory.limits.wide_pullback_shape.fintype_hom {J : Type v}  :
fintype (j j')
Equations
@[protected, instance]
Equations
@[protected, instance]
noncomputable def category_theory.limits.wide_pushout_shape.fintype_hom {J : Type v}  :
fintype (j j')
Equations
@[protected, instance]
noncomputable def category_theory.limits.fin_category_wide_pullback {J : Type v} [fintype J] :
Equations
@[protected, instance]
noncomputable def category_theory.limits.fin_category_wide_pushout {J : Type v} [fintype J] :
Equations
@[class]
structure category_theory.limits.has_finite_wide_pullbacks (C : Type u)  :
Prop
• out : ∀ (J : Type) [_inst_2 : fintype J],

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

@[protected, instance]
@[class]
structure category_theory.limits.has_finite_wide_pushouts (C : Type u)  :
Prop
• out : ∀ (J : Type) [_inst_2 : fintype J],

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

@[protected, 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

@[protected, instance]
Equations