Documentation

Mathlib.CategoryTheory.Limits.Preserves.Ulift

ULift creates small (co)limits #

This file shows that uliftFunctor.{v, u} creates (and hence preserves) limits and colimits indexed by J with [Category.{u, u} J].

It also shows that uliftFunctor.{v, u} preserves "all" limits (i.e. of size max u v, potentially too big to exist in Type u).

The equivalence between the ulift of the explicit limit cone of a functor K and the explicit limit cone of K ⋙ uliftFunctor.

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

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

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

      The equivalence between the ulift of the explicit colimit cocone of a functor K and the explicit colimit cocone of K ⋙ uliftFunctor.

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