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.{w, u} J].

It also shows that uliftFunctor.{v, u} preserves "all" limits, potentially too big to exist in Type u).

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

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

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

    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.

    Given a subset of the cocone point of a cocone over the lifted functor, produce a cocone over the original functor.

    Equations
    Instances For

      Given a subset of the cocone point of a cocone over the lifted functor, produce a subset of the cocone point of a colimit cocone over the original functor.

      Equations
      Instances For
        theorem CategoryTheory.Limits.Types.descSet_spec {J : Type u_1} [CategoryTheory.Category.{u_2, u_1} J] {K : CategoryTheory.Functor J (Type u)} {c : CategoryTheory.Limits.Cocone K} (hc : CategoryTheory.Limits.IsColimit c) {lc : CategoryTheory.Limits.Cocone (K.comp CategoryTheory.uliftFunctor.{v, u} )} (s : Set c.pt) (ls : Set lc.pt) :
        CategoryTheory.Limits.Types.descSet hc ls = s ∀ (j : J) (x : K.obj j), lc.app j { down := x } ls c.app j x s

        Characterization the map descSet hc: the image of an element in a vertex of the original diagram in the cocone point lies in descSet hc ls if and only if the image of the corresponding element in the lifted diagram lie in ls.

        Given a colimit cocone in Type u and an arbitrary cocone over the diagram lifted to Type (max u v), produce a function from the cocone point of the colimit cocone to the cocone point of the other cocone, that witnesses the colimit cocone also being a colimit in the higher universe.

        Equations
        Instances For

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

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

          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.