mathlib3 documentation

category_theory.limits.shapes.finite_limits

Categories with finite limits. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

@[class]

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
@[class]

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]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[class]

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

@[class]

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

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