# mathlibdocumentation

category_theory.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. category_theory.ulift.up is the functorial version of the usual ulift.up.
2. category_theory.ulift.down is the functorial version of the usual ulift.down.
3. category_theory.ulift.equivalence is the categorical equivalence between C and ulift C.

# ulift_hom #

Given a type C : Type u, ulift_hom.{w} C is just an alias for C. If we have category.{v} C, then ulift_hom.{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 ulift_hom.up, the backward direction is ulift_hom.donw and the equivalence is ulift_hom.equiv.

# as_small #

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 as_small.{w} C : Type (max w v u) equivalent to C.

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

@[simp]
theorem category_theory.ulift.up_map {C : Type u₁} (X Y : C) (f : X Y) :
def category_theory.ulift.up {C : Type u₁}  :
C

The functorial version of ulift.up.

Equations
@[simp]
theorem category_theory.ulift.up_obj_down {C : Type u₁} (down : C) :
@[simp]
theorem category_theory.ulift.down_obj {C : Type u₁} (self : ulift C) :
= self.down
def category_theory.ulift.down {C : Type u₁}  :
C

The functorial version of ulift.down.

Equations
@[simp]
theorem category_theory.ulift.down_map {C : Type u₁} (X Y : ulift C) (f : X Y) :
@[simp]
@[simp]
theorem category_theory.ulift.equivalence_counit_iso_inv_app {C : Type u₁} (X : ulift C) :
= 𝟙 ((𝟭 (ulift C)).obj X).down
@[simp]
@[simp]
theorem category_theory.ulift.equivalence_counit_iso_hom_app {C : Type u₁} (X : ulift C) :
@[simp]
@[simp]
def category_theory.ulift.equivalence {C : Type u₁}  :
C

The categorical equivalence between C and ulift C.

Equations
@[instance]
def category_theory.ulift.is_filtered {C : Type u₁}  :
@[instance]
def category_theory.ulift_hom (C : Type u) :
Type u

ulift_hom.{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
@[instance]
Equations
def category_theory.ulift_hom.obj_down {C : Type u_1}  :
C

The obvious function ulift_hom C → C.

Equations
def category_theory.ulift_hom.obj_up {C : Type u_1} (A : C) :

The obvious function C → ulift_hom C.

Equations
@[simp]
theorem category_theory.obj_down_obj_up {C : Type u_1} (A : C) :
@[simp]
theorem category_theory.obj_up_obj_down {C : Type u_1}  :
@[instance]
Equations
@[simp]
theorem category_theory.ulift_hom.up_obj {C : Type u₁} (A : C) :
def category_theory.ulift_hom.up {C : Type u₁}  :

One half of the quivalence between C and ulift_hom C.

Equations
@[simp]
theorem category_theory.ulift_hom.up_map_down {C : Type u₁} (X Y : C) (f : X Y) :
def category_theory.ulift_hom.down {C : Type u₁}  :

One half of the quivalence between C and ulift_hom C.

Equations
@[simp]
theorem category_theory.ulift_hom.down_map {C : Type u₁} (X Y : category_theory.ulift_hom C) (f : X Y) :
@[simp]
theorem category_theory.ulift_hom.down_obj {C : Type u₁}  :
def category_theory.ulift_hom.equiv {C : Type u₁}  :

The equivalence between C and ulift_hom C.

Equations
@[instance]
@[instance]
@[nolint]
def category_theory.as_small (C : Type u)  :
Type (max u w v)

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

The objects and morphisms of as_small 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
@[instance]
Equations
@[simp]
theorem category_theory.as_small.up_obj_down {C : Type u₁} (X : C) :
@[simp]
theorem category_theory.as_small.up_map_down {C : Type u₁} (X Y : C) (f : X Y) :
def category_theory.as_small.up {C : Type u₁}  :

One half of the equivalence between C and as_small C.

Equations
def category_theory.as_small.down {C : Type u₁}  :

One half of the equivalence between C and as_small C.

Equations
@[simp]
theorem category_theory.as_small.down_map {C : Type u₁} (X Y : category_theory.as_small C) (f : X Y) :
@[simp]
theorem category_theory.as_small.down_obj {C : Type u₁} (X : category_theory.as_small C) :
def category_theory.as_small.equiv {C : Type u₁}  :

The equivalence between C and as_small C.

Equations
@[simp]
@[simp]
@[simp]
theorem category_theory.as_small.equiv_counit_iso {C : Type u₁}  :
category_theory.as_small.equiv.counit_iso = category_theory.as_small.equiv._proof_4
@[simp]
theorem category_theory.as_small.equiv_unit_iso {C : Type u₁}  :
category_theory.as_small.equiv.unit_iso = category_theory.as_small.equiv._proof_2
@[instance]
def category_theory.as_small.inhabited {C : Type u₁} [inhabited C] :
Equations
@[instance]
@[instance]