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_obj_down {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (down : C) :
(CategoryTheory.ULift.upFunctor.obj down).down = down
@[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

The functorial version of ULift.up.

Equations
  • CategoryTheory.ULift.upFunctor = { toPrefunctor := { obj := ULift.up, map := fun {X Y : C} (f : X Y) => f }, map_id := , map_comp := }
Instances For
    @[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.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

    The functorial version of ULift.down.

    Equations
    • CategoryTheory.ULift.downFunctor = { toPrefunctor := { obj := ULift.down, map := fun {X Y : ULift.{u₂, u₁} C} (f : X Y) => f }, map_id := , map_comp := }
    Instances For
      @[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)
      @[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)

      The categorical equivalence between C and ULift C.

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

        Equations
        Instances For
          Equations
          • CategoryTheory.instInhabitedULiftHom = { default := default }

          The obvious function ULiftHom C → C.

          Equations
          Instances For

            The obvious function C → ULiftHom C.

            Equations
            Instances For
              @[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
              @[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

              One half of the quivalence between C and ULiftHom C.

              Equations
              • CategoryTheory.ULiftHom.up = { toPrefunctor := { obj := CategoryTheory.ULiftHom.objUp, map := fun {X Y : C} (f : X Y) => { down := f } }, map_id := , map_comp := }
              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.

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

                  The equivalence between C and ULiftHom C.

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

                    Equations
                    Instances For
                      @[simp]
                      theorem CategoryTheory.AsSmall.up_obj_down {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) :
                      (CategoryTheory.AsSmall.up.obj X).down = X
                      @[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

                      One half of the equivalence between C and AsSmall C.

                      Equations
                      • CategoryTheory.AsSmall.up = { toPrefunctor := { obj := fun (X : C) => { down := X }, map := fun {X Y : C} (f : X Y) => { down := f } }, map_id := , map_comp := }
                      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.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[simp]
                          theorem CategoryTheory.AsSmall.equiv_unitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :
                          CategoryTheory.AsSmall.equiv.unitIso = CategoryTheory.NatIso.ofComponents (fun (X : C) => CategoryTheory.eqToIso )
                          @[simp]
                          theorem CategoryTheory.AsSmall.equiv_inverse {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :
                          CategoryTheory.AsSmall.equiv.inverse = CategoryTheory.AsSmall.down
                          @[simp]
                          theorem CategoryTheory.AsSmall.equiv_functor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :
                          CategoryTheory.AsSmall.equiv.functor = CategoryTheory.AsSmall.up

                          The equivalence between C and AsSmall C.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            Equations
                            • CategoryTheory.instInhabitedAsSmall = { default := { down := default } }

                            The equivalence between C and ULiftHom (ULift C).

                            Equations
                            Instances For