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.

def CategoryTheory.ULift.upFunctor {C : Type u₁} [Category.{v₁, u₁} C] : Functor C (ULift.{u₂, u₁} C)

The functorial version of ULift.up.

Equations

• CategoryTheory.ULift.upFunctor = { obj := ULift.up, map := fun {X Y : C} (f : X ⟶ Y) => f, map_id := ⋯, map_comp := ⋯ }

@[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

def CategoryTheory.ULift.downFunctor {C : Type u₁} [Category.{v₁, u₁} C] : Functor (ULift.{u₂, u₁} C) C

The functorial version of ULift.down.

Equations

• CategoryTheory.ULift.downFunctor = { obj := ULift.down, map := fun {X Y : ULift.{?u.17, ?u.18} C} (f : X ⟶ Y) => f, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem CategoryTheory.ULift.downFunctor_obj {C : Type u₁} [Category.{v₁, u₁} C] (self : ULift.{u₂, u₁} C) : downFunctor.obj self = self.down

@[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

def CategoryTheory.ULift.equivalence {C : Type u₁} [Category.{v₁, u₁} C] : C ≌ ULift.{u₂, u₁} C

The categorical equivalence between C and ULift C.

Equations

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

@[simp]

theorem CategoryTheory.ULift.equivalence_unitIso_hom {C : Type u₁} [Category.{v₁, u₁} C] : equivalence.unitIso.hom = CategoryStruct.id (Functor.id C)

@[simp]

theorem CategoryTheory.ULift.equivalence_unitIso_inv {C : Type u₁} [Category.{v₁, u₁} C] : equivalence.unitIso.inv = CategoryStruct.id (upFunctor.comp downFunctor)

@[simp]

theorem CategoryTheory.ULift.equivalence_functor {C : Type u₁} [Category.{v₁, u₁} C] : equivalence.functor = upFunctor

@[simp]

theorem CategoryTheory.ULift.equivalence_inverse {C : Type u₁} [Category.{v₁, u₁} C] : equivalence.inverse = downFunctor

@[simp]

theorem CategoryTheory.ULift.equivalence_counitIso_hom_app {C : Type u₁} [Category.{v₁, u₁} C] (x✝ : ULift.{u₂, u₁} C) : equivalence.counitIso.hom.app x✝ = CategoryStruct.id ((downFunctor.comp upFunctor).obj x✝)

@[simp]

theorem CategoryTheory.ULift.equivalence_counitIso_inv_app {C : Type u₁} [Category.{v₁, u₁} C] (x✝ : ULift.{u₂, u₁} C) : equivalence.counitIso.inv.app x✝ = CategoryStruct.id ((Functor.id (ULift.{u₂, u₁} C)).obj x✝)

def CategoryTheory.ULiftHom (C : Type u) : Type u

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

• CategoryTheory.ULiftHom C = C

instance CategoryTheory.instInhabitedULiftHom {C : Type u_1} [Inhabited C] : Inhabited (ULiftHom C)

Equations

• CategoryTheory.instInhabitedULiftHom = { default := default }

def CategoryTheory.ULiftHom.objDown {C : Type u_1} (A : ULiftHom C) : C

The obvious function ULiftHom C → C.

Equations

• A.objDown = A

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

The obvious function C → ULiftHom C.

Equations

• CategoryTheory.ULiftHom.objUp A = A

@[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

instance CategoryTheory.ULiftHom.category {C : Type u₁} [Category.{v₁, u₁} C] : Category.{max v₂ v₁, u₁} (ULiftHom C)

Equations

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

def CategoryTheory.ULiftHom.up {C : Type u₁} [Category.{v₁, u₁} C] : Functor C (ULiftHom C)

One half of the equivalence between C and ULiftHom C.

Equations

• CategoryTheory.ULiftHom.up = { obj := CategoryTheory.ULiftHom.objUp, map := fun {X Y : C} (f : X ⟶ Y) => { down := f }, map_id := ⋯, map_comp := ⋯ }

@[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

def CategoryTheory.ULiftHom.down {C : Type u₁} [Category.{v₁, u₁} C] : Functor (ULiftHom C) C

One half of the equivalence between C and ULiftHom C.

Equations

• CategoryTheory.ULiftHom.down = { obj := CategoryTheory.ULiftHom.objDown, map := fun {X Y : CategoryTheory.ULiftHom C} (f : X ⟶ Y) => f.down, map_id := ⋯, map_comp := ⋯ }

@[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

def CategoryTheory.ULiftHom.equiv {C : Type u₁} [Category.{v₁, u₁} C] : C ≌ ULiftHom C

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

• CategoryTheory.AsSmall D = ULift.{max ?u.12 ?u.11, ?u.10} D

instance CategoryTheory.instSmallCategoryAsSmall {C : Type u₁} [Category.{v₁, u₁} C] : SmallCategory (AsSmall C)

Equations

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

def CategoryTheory.AsSmall.up {C : Type u₁} [Category.{v₁, u₁} C] : Functor C (AsSmall C)

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

def CategoryTheory.AsSmall.down {C : Type u₁} [Category.{v₁, u₁} C] : Functor (AsSmall C) C

One half of the equivalence between C and AsSmall C.

Equations

• CategoryTheory.AsSmall.down = { obj := fun (X : CategoryTheory.AsSmall C) => X.down, map := fun {X Y : CategoryTheory.AsSmall C} (f : X ⟶ Y) => f.down, map_id := ⋯, map_comp := ⋯ }

@[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✝) : CategoryStruct.comp (CategoryStruct.comp f g).down h = CategoryStruct.comp f.down (CategoryStruct.comp g.down h)

@[simp]

theorem CategoryTheory.eqToHom_down {C : Type u₁} [Category.{v₁, u₁} C] {X Y : AsSmall C} (h : X = Y) : (eqToHom h).down = eqToHom ⋯

def CategoryTheory.AsSmall.equiv {C : Type u₁} [Category.{v₁, u₁} C] : C ≌ AsSmall C

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_functor {C : Type u₁} [Category.{v₁, u₁} C] : equiv.functor = up

@[simp]

theorem CategoryTheory.AsSmall.equiv_unitIso {C : Type u₁} [Category.{v₁, u₁} C] : equiv.unitIso = NatIso.ofComponents (fun (x : C) => eqToIso ⋯) ⋯

@[simp]

theorem CategoryTheory.AsSmall.equiv_counitIso {C : Type u₁} [Category.{v₁, u₁} C] : equiv.counitIso = NatIso.ofComponents (fun (x : AsSmall C) => eqToIso ⋯) ⋯

@[simp]

theorem CategoryTheory.AsSmall.equiv_inverse {C : Type u₁} [Category.{v₁, u₁} C] : equiv.inverse = down

instance CategoryTheory.instInhabitedAsSmall {C : Type u₁} [Category.{v₁, u₁} C] [Inhabited C] : Inhabited (AsSmall C)

Equations

• CategoryTheory.instInhabitedAsSmall = { default := { down := default } }

def CategoryTheory.ULiftHomULiftCategory.equiv (C : Type u) [Category.{v, u} C] : C ≌ ULiftHom (ULift.{u', u} C)

The equivalence between C and ULiftHom (ULift C).

Equations

• CategoryTheory.ULiftHomULiftCategory.equiv C = CategoryTheory.ULift.equivalence.trans CategoryTheory.ULiftHom.equiv