mathlib3 documentation

category_theory.category.ulift

Basic API for ulift #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

The functorial version of ulift.up.

Equations

The functorial version of ulift.down.

Equations

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
Instances for category_theory.ulift_hom

The obvious function ulift_hom C → C.

Equations

The obvious function C → ulift_hom C.

Equations

One half of the quivalence between C and ulift_hom C.

Equations

One half of the quivalence between C and ulift_hom C.

Equations
@[nolint]

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
Instances for category_theory.as_small

One half of the equivalence between C and as_small C.

Equations

One half of the equivalence between C and as_small C.

Equations