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.

The functorial version of ULift.up.

Equations
@[simp]
theorem CategoryTheory.ULift.upFunctor_map {C : Type u₁} [Category.{v₁, u₁} C] {X✝ Y✝ : C} (f : X✝ Y✝) :
upFunctor.map f = f
@[simp]
theorem CategoryTheory.ULift.upFunctor_obj_down {C : Type u₁} [Category.{v₁, u₁} C] (down : C) :
(upFunctor.obj down).down = down

The functorial version of ULift.down.

Equations
@[simp]
@[simp]
theorem CategoryTheory.ULift.downFunctor_map {C : Type u₁} [Category.{v₁, u₁} C] {X✝ Y✝ : ULift.{u₂, u₁} C} (f : X✝ Y✝) :
downFunctor.map f = f

The categorical equivalence between C and ULift C.

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

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

The obvious function ULiftHom C → C.

Equations
  • A.objDown = A

The obvious function C → ULiftHom C.

Equations
@[simp]
theorem CategoryTheory.objDown_objUp {C : Type u_1} (A : C) :
(ULiftHom.objUp A).objDown = A
@[simp]
theorem CategoryTheory.objUp_objDown {C : Type u_1} (A : ULiftHom C) :
ULiftHom.objUp A.objDown = A

One half of the quivalence between C and ULiftHom C.

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

One half of the quivalence between C and ULiftHom C.

Equations
@[simp]
theorem CategoryTheory.ULiftHom.down_obj {C : Type u₁} [Category.{v₁, u₁} C] (A : ULiftHom C) :
down.obj A = A.objDown
@[simp]
theorem CategoryTheory.ULiftHom.down_map {C : Type u₁} [Category.{v₁, u₁} C] {X✝ Y✝ : ULiftHom C} (f : X✝ Y✝) :
down.map f = f.down

The equivalence between C and ULiftHom C.

Equations
  • One or more equations did not get rendered due to their size.
def CategoryTheory.AsSmall (D : Type u) [Category.{v, u} D] :
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.

Equations

One half of the equivalence between C and AsSmall C.

Equations
  • CategoryTheory.AsSmall.up = { obj := fun (X : C) => { down := X }, map := fun {X Y : C} (f : X Y) => { down := f }, map_id := , map_comp := }
@[simp]
theorem CategoryTheory.AsSmall.up_map_down {C : Type u₁} [Category.{v₁, u₁} C] {X✝ Y✝ : C} (f : X✝ Y✝) :
(up.map f).down = f
@[simp]
theorem CategoryTheory.AsSmall.up_obj_down {C : Type u₁} [Category.{v₁, u₁} C] (X : C) :
(up.obj X).down = X

One half of the equivalence between C and AsSmall C.

Equations
@[simp]
theorem CategoryTheory.AsSmall.down_map {C : Type u₁} [Category.{v₁, u₁} C] {X✝ Y✝ : AsSmall C} (f : X✝ Y✝) :
down.map f = f.down
@[simp]
theorem CategoryTheory.AsSmall.down_obj {C : Type u₁} [Category.{v₁, u₁} C] (X : AsSmall C) :
down.obj X = X.down
theorem CategoryTheory.down_comp {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : AsSmall C} (f : X Y) (g : Y Z) :
(CategoryStruct.comp f g).down = CategoryStruct.comp f.down g.down
theorem CategoryTheory.down_comp_assoc {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : AsSmall C} (f : X Y) (g : Y Z) {Z✝ : C} (h : Z.down Z✝) :
@[simp]
theorem CategoryTheory.eqToHom_down {C : Type u₁} [Category.{v₁, u₁} C] {X Y : AsSmall C} (h : X = Y) :
(eqToHom h).down = eqToHom

The equivalence between C and AsSmall C.

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