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
  • One or more equations did not get rendered due to their size.
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
    • One or more equations did not get rendered due to their size.
    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
    • One or more equations did not get rendered due to their size.