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).

source
def CategoryTheory.Limits.Types.sectionsEquiv {J : Type u} [CategoryTheory.Category.{u, u} J] (K : CategoryTheory.Functor J (Type u)) :
CategoryTheory.uliftFunctor.{v, u} .obj ↑(CategoryTheory.Functor.sections K) ≃ ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp K CategoryTheory.uliftFunctor.{v, 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
    source
    noncomputable instance CategoryTheory.Limits.Types.instCreatesLimitsOfSizeTypeTypesTypeTypesUliftFunctor :
    CategoryTheory.CreatesLimitsOfSize.{u, u, u, max u v, u + 1, max (u + 1) (v + 1)} CategoryTheory.uliftFunctor.{v, u}

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

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

    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
      source
      noncomputable instance CategoryTheory.Limits.Types.instPreservesLimitsTypeTypesTypeTypesUliftFunctor :
      CategoryTheory.Limits.PreservesLimits CategoryTheory.uliftFunctor.{v, u}

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

      Equations
      source
      def CategoryTheory.Limits.Types.quotEquiv {J : Type u} [CategoryTheory.Category.{u, u} J] (K : CategoryTheory.Functor J (Type u)) :
      CategoryTheory.uliftFunctor.{v, u} .obj (CategoryTheory.Limits.Types.Quot K) ≃ CategoryTheory.Limits.Types.Quot (CategoryTheory.Functor.comp K CategoryTheory.uliftFunctor.{v, u} )

      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
        source
        noncomputable instance CategoryTheory.Limits.Types.instCreatesColimitsOfSizeTypeTypesTypeTypesUliftFunctor :
        CategoryTheory.CreatesColimitsOfSize.{u, u, u, max u v, u + 1, max (u + 1) (v + 1)} CategoryTheory.uliftFunctor.{v, u}

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

        Equations