Documentation

Mathlib.CategoryTheory.Category.ULift

Basic API for ULift #

This file contains a very basic API for working with the categorical instance on ULift C where C is a type with a category instance.

  1. CategoryTheory.ULift.upFunctor is the functorial version of the usual ULift.up.
  2. CategoryTheory.ULift.downFunctor is the functorial version of the usual ULift.down.
  3. CategoryTheory.ULift.equivalence is the categorical equivalence between C and ULift C.

ULiftHom #

Given a type C : Type u, ULiftHom.{w} C is just an alias for C. If we have category.{v} C, then ULiftHom.{w} C is endowed with a category instance whose morphisms are obtained by applying ULift.{w} to the morphisms from C.

This is a category equivalent to C. The forward direction of the equivalence is ULiftHom.up, the backward direction is ULiftHom.down and the equivalence is ULiftHom.equiv.

AsSmall #

This file also contains a construction which takes a type C : Type u with a category instance Category.{v} C and makes a small category AsSmall.{w} C : Type (max w v u) equivalent to C.

The forward direction of the equivalence, C ⥤ AsSmall C, is denoted AsSmall.up and the backward direction is AsSmall.down. The equivalence itself is AsSmall.equiv.

@[simp]
theorem CategoryTheory.ULift.upFunctor_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :
∀ {X Y : C} (f : X Y), CategoryTheory.ULift.upFunctor.map f = f
@[simp]
theorem CategoryTheory.ULift.upFunctor_obj_down {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (down : C) :
(CategoryTheory.ULift.upFunctor.obj down).down = down
@[simp]
theorem CategoryTheory.ULift.downFunctor_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :
∀ {X Y : ULift.{u₂, u₁} C} (f : X Y), CategoryTheory.ULift.downFunctor.map f = f
@[simp]
theorem CategoryTheory.ULift.downFunctor_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (self : ULift.{u₂, u₁} C) :
CategoryTheory.ULift.downFunctor.obj self = self.down
@[simp]
theorem CategoryTheory.ULift.equivalence_functor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :
CategoryTheory.ULift.equivalence.functor = CategoryTheory.ULift.upFunctor
@[simp]
theorem CategoryTheory.ULift.equivalence_inverse {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :
CategoryTheory.ULift.equivalence.inverse = CategoryTheory.ULift.downFunctor
@[simp]
theorem CategoryTheory.ULift.equivalence_unitIso_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :
CategoryTheory.ULift.equivalence.unitIso.inv = CategoryTheory.CategoryStruct.id (CategoryTheory.Functor.comp CategoryTheory.ULift.upFunctor CategoryTheory.ULift.downFunctor)
@[simp]
theorem CategoryTheory.ULift.equivalence_counitIso_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : ULift.{u₂, u₁} C) :
CategoryTheory.ULift.equivalence.counitIso.hom.app X = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.comp CategoryTheory.ULift.downFunctor CategoryTheory.ULift.upFunctor).obj X)

The categorical equivalence between C and ULift C.

Instances For

    ULiftHom.{w} C is an alias for C, which is endowed with a category instance whose morphisms are obtained by applying ULift.{w} to the morphisms from C.

    Instances For

      The obvious function ULiftHom C → C.

      Instances For

        The obvious function C → ULiftHom C.

        Instances For
          @[simp]
          theorem CategoryTheory.ULiftHom.up_map_down {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :
          ∀ {X Y : C} (f : X Y), (CategoryTheory.ULiftHom.up.map f).down = f
          @[simp]
          theorem CategoryTheory.ULiftHom.up_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (A : C) :
          CategoryTheory.ULiftHom.up.obj A = CategoryTheory.ULiftHom.objUp A

          One half of the quivalence between C and ULiftHom C.

          Instances For
            @[simp]
            theorem CategoryTheory.ULiftHom.down_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :
            ∀ {X Y : CategoryTheory.ULiftHom C} (f : X Y), CategoryTheory.ULiftHom.down.map f = f.down

            One half of the quivalence between C and ULiftHom C.

            Instances For

              The equivalence between C and ULiftHom C.

              Instances For

                AsSmall C is a small category equivalent to C. More specifically, if C : Type u is endowed with Category.{v} C, then AsSmall.{w} C : Type (max w v u) is endowed with an instance of a small category.

                The objects and morphisms of AsSmall C are defined by applying ULift to the objects and morphisms of C.

                Note: We require a category instance for this definition in order to have direct access to the universe level v.

                Instances For
                  @[simp]
                  theorem CategoryTheory.AsSmall.up_map_down {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :
                  ∀ {X Y : C} (f : X Y), (CategoryTheory.AsSmall.up.map f).down = f
                  @[simp]
                  theorem CategoryTheory.AsSmall.up_obj_down {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) :
                  (CategoryTheory.AsSmall.up.obj X).down = X

                  One half of the equivalence between C and AsSmall C.

                  Instances For
                    @[simp]
                    theorem CategoryTheory.AsSmall.down_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : CategoryTheory.AsSmall C) :
                    CategoryTheory.AsSmall.down.obj X = X.down
                    @[simp]
                    theorem CategoryTheory.AsSmall.down_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :
                    ∀ {X Y : CategoryTheory.AsSmall C} (f : X Y), CategoryTheory.AsSmall.down.map f = f.down

                    One half of the equivalence between C and AsSmall C.

                    Instances For
                      @[simp]
                      theorem CategoryTheory.AsSmall.equiv_functor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :
                      CategoryTheory.AsSmall.equiv.functor = CategoryTheory.AsSmall.up
                      @[simp]
                      theorem CategoryTheory.AsSmall.equiv_counitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :
                      CategoryTheory.AsSmall.equiv.counitIso = CategoryTheory.NatIso.ofComponents fun X => CategoryTheory.eqToIso (_ : (CategoryTheory.Functor.comp CategoryTheory.AsSmall.down CategoryTheory.AsSmall.up).obj X = (CategoryTheory.Functor.id (CategoryTheory.AsSmall C)).obj X)
                      @[simp]
                      theorem CategoryTheory.AsSmall.equiv_inverse {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :
                      CategoryTheory.AsSmall.equiv.inverse = CategoryTheory.AsSmall.down

                      The equivalence between C and AsSmall C.

                      Instances For