mathlib documentation

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₁} [category_theory.category C] (X Y : C) (f : X Y) :

The functorial version of ulift.up.

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

The functorial version of ulift.down.

Equations
@[simp]
theorem category_theory.ulift.down_map {C : Type u₁} [category_theory.category C] (X Y : ulift C) (f : X Y) :
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

The obvious function ulift_hom C → C.

Equations

The obvious function C → ulift_hom C.

Equations
@[simp]

One half of the quivalence between C and ulift_hom C.

Equations
@[simp]

One half of the quivalence between C and ulift_hom C.

Equations

The equivalence between C and ulift_hom C.

Equations
@[nolint]
def category_theory.as_small (C : Type u) [category_theory.category C] :
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
@[simp]

One half of the equivalence between C and as_small C.

Equations

One half of the equivalence between C and as_small C.

Equations

The equivalence between C and as_small C.

Equations