Documentation

Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite

Creation of finite limits #

This file defines the classes CreatesFiniteLimits, CreatesFiniteColimits, CreatesFiniteProducts and CreatesFiniteCoproducts.

class CategoryTheory.Limits.CreatesFiniteLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) :
Type (max (max (max (max 1 u₁) u₂) v₁) v₂)

We say that a functor creates finite limits if it creates all limits of shape J where J : Type is a finite category.

Instances

If F creates limits of any size, it creates finite limits.

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

If F creates finite limits in any universe, then it creates finite limits.

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

Transfer creation of finite limits along a natural isomorphism in the functor.

Equations
  • One or more equations did not get rendered due to their size.
class CategoryTheory.Limits.CreatesFiniteProducts {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) :
Type (max (max (max (max 1 u₁) u₂) v₁) v₂)

We say that a functor creates finite products if it creates all limits of shape Discrete J where J : Type is finite.

Instances

Transfer creation of finite products along a natural isomorphism in the functor.

Equations
class CategoryTheory.Limits.CreatesFiniteColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) :
Type (max (max (max (max 1 u₁) u₂) v₁) v₂)

We say that a functor creates finite colimits if it creates all colimits of shape J where J : Type is a finite category.

Instances

If F creates colimits of any size, it creates finite colimits.

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

If F creates finite colimits in any universe, then it creates finite colimits.

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

Transfer creation of finite colimits along a natural isomorphism in the functor.

Equations
  • One or more equations did not get rendered due to their size.
class CategoryTheory.Limits.CreatesFiniteCoproducts {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) :
Type (max (max (max (max 1 u₁) u₂) v₁) v₂)

We say that a functor creates finite limits if it creates all limits of shape J where J : Type is a finite category.

Instances

Transfer creation of finite limits along a natural isomorphism in the functor.

Equations