# 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₁} [] :
∀ {X Y : C} (f : X Y), CategoryTheory.ULift.upFunctor.map f = f
@[simp]
theorem CategoryTheory.ULift.upFunctor_obj_down {C : Type u₁} [] (down : C) :
(CategoryTheory.ULift.upFunctor.obj down).down = down

The functorial version of ULift.up.

Instances For
@[simp]
theorem CategoryTheory.ULift.downFunctor_map {C : Type u₁} [] :
∀ {X Y : } (f : X Y), CategoryTheory.ULift.downFunctor.map f = f
@[simp]
theorem CategoryTheory.ULift.downFunctor_obj {C : Type u₁} [] (self : ) :
CategoryTheory.ULift.downFunctor.obj self = self.down

The functorial version of ULift.down.

Instances For
@[simp]
theorem CategoryTheory.ULift.equivalence_functor {C : Type u₁} [] :
CategoryTheory.ULift.equivalence.functor = CategoryTheory.ULift.upFunctor
@[simp]
theorem CategoryTheory.ULift.equivalence_unitIso_hom {C : Type u₁} [] :
CategoryTheory.ULift.equivalence.unitIso.hom =
@[simp]
theorem CategoryTheory.ULift.equivalence_inverse {C : Type u₁} [] :
CategoryTheory.ULift.equivalence.inverse = CategoryTheory.ULift.downFunctor
@[simp]
theorem CategoryTheory.ULift.equivalence_unitIso_inv {C : Type u₁} [] :
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₁} [] (X : ) :
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_counitIso_inv_app {C : Type u₁} [] (X : ) :
CategoryTheory.ULift.equivalence.counitIso.inv.app X = CategoryTheory.CategoryStruct.id (().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
def CategoryTheory.ULiftHom.objDown {C : Type u_1} (A : ) :
C

The obvious function ULiftHom C → C.

Instances For
def CategoryTheory.ULiftHom.objUp {C : Type u_1} (A : C) :

The obvious function C → ULiftHom C.

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

One half of the quivalence between C and ULiftHom C.

Instances For
@[simp]
theorem CategoryTheory.ULiftHom.down_obj {C : Type u₁} [] (A : ) :
CategoryTheory.ULiftHom.down.obj A =
@[simp]
theorem CategoryTheory.ULiftHom.down_map {C : Type u₁} [] :
∀ {X Y : } (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
def CategoryTheory.AsSmall (D : Type u) :
Type (max u w v)

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₁} [] :
∀ {X Y : C} (f : X Y), (CategoryTheory.AsSmall.up.map f).down = f
@[simp]
theorem CategoryTheory.AsSmall.up_obj_down {C : Type u₁} [] (X : C) :
(CategoryTheory.AsSmall.up.obj X).down = X
def CategoryTheory.AsSmall.up {C : Type u₁} [] :

One half of the equivalence between C and AsSmall C.

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

One half of the equivalence between C and AsSmall C.

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

The equivalence between C and AsSmall C.

Instances For

The equivalence between C and ULiftHom (ULift C).

Instances For