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