Documentation

Mathlib.CategoryTheory.Limits.Preserves.Ulift

ULift creates small (co)limits #

This file shows that uliftFunctor.{v, u} preserves all limits and colimits, including those potentially too big to exist in Type u.

As this functor is fully faithful, we also deduce that it creates u-small limits and colimits.

source
def CategoryTheory.Limits.Types.sectionsEquiv {J : Type u_1} [Category.{u_2, u_1} J] (K : Functor J (Type u)) :
↑K.sections ≃ ↑(K.comp uliftFunctor.{v, u}).sections

The equivalence between K.sections and (K ⋙ uliftFunctor.{v, u}).sections. This is used to show that uliftFunctor preserves limits that are potentially too large to exist in the source category.

Equations
    Instances For
      source
      instance CategoryTheory.Limits.Types.instPreservesLimitsOfSizeUliftFunctor :
      PreservesLimitsOfSize.{w', w, u, max u v, u + 1, max (u + 1) (v + 1)} uliftFunctor.{v, u}

      The functor uliftFunctor : Type u ⥤ Type (max u v) preserves limits of arbitrary size.

      source
      noncomputable instance CategoryTheory.Limits.Types.instCreatesLimitsOfSizeUliftFunctor :
      CreatesLimitsOfSize.{w, u, u, max u v, u + 1, max (u + 1) (v + 1)} uliftFunctor.{v, u}

      The functor uliftFunctor : Type u ⥤ Type (max u v) creates u-small limits.

      Equations
        source
        instance CategoryTheory.Limits.Types.instPreservesColimitsOfSizeUliftFunctor :
        PreservesColimitsOfSize.{w', w, u, max u v, u + 1, max (u + 1) (v + 1)} uliftFunctor.{v, u}

        The functor uliftFunctor : Type u ⥤ Type (max u v) preserves colimits of arbitrary size.

        source
        noncomputable instance CategoryTheory.Limits.Types.instCreatesColimitsOfSizeUliftFunctor :
        CreatesColimitsOfSize.{w, u, u, max u v, u + 1, max (u + 1) (v + 1)} uliftFunctor.{v, u}

        The functor uliftFunctor : Type u ⥤ Type (max u v) creates u-small colimits.

        Equations