Module docstring

{"# 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.

CategoryTheory.ULift.upFunctor is the functorial version of the usual ULift.up.
CategoryTheory.ULift.downFunctor is the functorial version of the usual ULift.down.
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. "}

CategoryTheory.ULift.upFunctor definition

: C ⥤ ULift.{u₂} C

Full source

/-- The functorial version of `ULift.up`. -/
@[simps]
def ULift.upFunctor : C ⥤ ULift.{u₂} C where
  obj := ULift.up
  map f := f

Up functor for lifted category

Informal description

The functor that lifts objects and morphisms from a category $C$ to its lifted version $\mathrm{ULift}_{\{u_2\}} C$ by applying the $\mathrm{ULift.up}$ operation. On objects, it sends $X$ to $\mathrm{ULift.up}\, X$, and on morphisms, it acts as the identity.

CategoryTheory.ULift.downFunctor definition

: ULift.{u₂} C ⥤ C

Full source

/-- The functorial version of `ULift.down`. -/
@[simps]
def ULift.downFunctor : ULiftULift.{u₂} C ⥤ C where
  obj := ULift.down
  map f := f

Down functor for lifted category

Informal description

The functor from the lifted category `ULift.{u₂} C` back to the original category `C`, which maps objects via the `ULift.down` operation and acts as the identity on morphisms.

CategoryTheory.ULift.equivalence definition

: C ≌ ULift.{u₂} C

Full source

/-- The categorical equivalence between `C` and `ULift C`. -/
@[simps]
def ULift.equivalence : C ≌ ULift.{u₂} C where
  functor := ULift.upFunctor
  inverse := ULift.downFunctor
  unitIso :=
    { hom := 𝟙 _
      inv := 𝟙 _ }
  counitIso :=
    { hom := { app := fun _ => 𝟙 _ }
      inv := { app := fun _ => 𝟙 _ } }

Equivalence between a category and its lifted version

Informal description

The categorical equivalence between a category $C$ and its lifted version $\mathrm{ULift}_{\{u_2\}} C$, consisting of: - The functor $\mathrm{upFunctor} \colon C \to \mathrm{ULift}_{\{u_2\}} C$ that lifts objects and morphisms via $\mathrm{ULift.up}$, - The functor $\mathrm{downFunctor} \colon \mathrm{ULift}_{\{u_2\}} C \to C$ that projects objects and morphisms via $\mathrm{ULift.down}$, - The identity natural isomorphism $\eta \colon \mathrm{id}_C \cong \mathrm{downFunctor} \circ \mathrm{upFunctor}$, - The identity natural isomorphism $\epsilon \colon \mathrm{upFunctor} \circ \mathrm{downFunctor} \cong \mathrm{id}_{\mathrm{ULift}_{\{u_2\}} C}$.

CategoryTheory.ULiftHom definition

(C : Type u) : Type u

Full source

/-- `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`.
-/
def ULiftHom.{w,u} (C : Type u) : Type u :=
  let _ := ULift.{w} C
  C

ULiftHom category construction

Informal description

Given a type `C` in universe `u`, `ULiftHom.{w} C` is an alias for `C` that is endowed with a category structure where the morphisms are obtained by applying `ULift.{w}` to the morphisms from `C`. This construction provides a category equivalent to `C`.

CategoryTheory.instInhabitedULiftHom instance

{C} [Inhabited C] : Inhabited (ULiftHom C)

Full source

instance {C} [Inhabited C] : Inhabited (ULiftHom C) :=
  ⟨(default : C)⟩

Inhabitedness of ULiftHom Categories

Informal description

For any type $C$ with a distinguished element (i.e., $C$ is inhabited), the category `ULiftHom C` is also inhabited.

CategoryTheory.ULiftHom.objDown definition

{C} (A : ULiftHom C) : C

Full source

/-- The obvious function `ULiftHom C → C`. -/
def ULiftHom.objDown {C} (A : ULiftHom C) : C :=
  A

Downward object map from ULiftHom

Informal description

The function maps an object $A$ in the category `ULiftHom C` back to its corresponding object in the original category $C$.

CategoryTheory.ULiftHom.objUp definition

{C} (A : C) : ULiftHom C

Full source

/-- The obvious function `C → ULiftHom C`. -/
def ULiftHom.objUp {C} (A : C) : ULiftHom C :=
  A

Object lifting to ULiftHom category

Informal description

The function that lifts an object $A$ from a category $C$ to the category $\mathrm{ULiftHom}\, C$, which is equivalent to $C$ but with morphisms lifted to a higher universe.

CategoryTheory.objDown_objUp theorem

{C} (A : C) : (ULiftHom.objUp A).objDown = A

Full source

@[simp]
theorem objDown_objUp {C} (A : C) : (ULiftHom.objUp A).objDown = A :=
  rfl

Inverse Property of ULiftHom Object Maps: $\mathrm{objDown} \circ \mathrm{objUp} = \mathrm{id}$

Informal description

For any object $A$ in a category $C$, applying the upward object map $\mathrm{objUp}$ followed by the downward object map $\mathrm{objDown}$ returns $A$ itself, i.e., $\mathrm{objDown}(\mathrm{objUp}(A)) = A$.

CategoryTheory.objUp_objDown theorem

{C} (A : ULiftHom C) : ULiftHom.objUp A.objDown = A

Full source

@[simp]
theorem objUp_objDown {C} (A : ULiftHom C) : ULiftHom.objUp A.objDown = A :=
  rfl

Inverse Property of ULiftHom Object Maps

Informal description

For any object $A$ in the category $\mathrm{ULiftHom}\, C$, the composition of the downward object map followed by the upward object map returns $A$ itself, i.e., $\mathrm{objUp}(\mathrm{objDown}(A)) = A$.

CategoryTheory.ULiftHom.category instance

: Category.{max v₂ v₁} (ULiftHom.{v₂} C)

Full source

instance ULiftHom.category : Category.{max v₂ v₁} (ULiftHom.{v₂} C) where
  Hom A B := ULift.{v₂} <| A.objDown ⟶ B.objDown
  id _ := ⟨𝟙 _⟩
  comp f g := ⟨f.down ≫ g.down⟩

Category Structure on ULiftHom

Informal description

For any category $C$ with morphisms in universe $v₁$, the category `ULiftHom.{v₂} C` has morphisms lifted to universe $\max(v₂, v₁)$ and forms a valid category structure.

CategoryTheory.ULiftHom.up definition

: C ⥤ ULiftHom C

Full source

/-- One half of the equivalence between `C` and `ULiftHom C`. -/
@[simps]
def ULiftHom.up : C ⥤ ULiftHom C where
  obj := ULiftHom.objUp
  map f := ⟨f⟩

Upward functor to ULiftHom category

Informal description

The functor that lifts objects and morphisms from a category $C$ to the category $\mathrm{ULiftHom}\, C$. On objects, it applies $\mathrm{objUp}$ to lift an object from $C$ to $\mathrm{ULiftHom}\, C$. On morphisms, it wraps a morphism $f$ in $C$ into a $\mathrm{ULift}$ structure to obtain a morphism in $\mathrm{ULiftHom}\, C$.

CategoryTheory.ULiftHom.down definition

: ULiftHom C ⥤ C

Full source

/-- One half of the equivalence between `C` and `ULiftHom C`. -/
@[simps]
def ULiftHom.down : ULiftHomULiftHom C ⥤ C where
  obj := ULiftHom.objDown
  map f := f.down

Downward functor from ULiftHom to original category

Informal description

The functor that maps objects and morphisms from the category `ULiftHom C` back to the original category `C`. Specifically, it sends an object `A` in `ULiftHom C` to its corresponding object in `C` via `ULiftHom.objDown`, and a morphism `f` in `ULiftHom C` to its underlying morphism in `C` via the projection `f.down`.

CategoryTheory.ULiftHom.equiv definition

: C ≌ ULiftHom C

Full source

/-- The equivalence between `C` and `ULiftHom C`. -/
def ULiftHom.equiv : C ≌ ULiftHom C where
  functor := ULiftHom.up
  inverse := ULiftHom.down
  unitIso := NatIso.ofComponents fun _ => eqToIso rfl
  counitIso := NatIso.ofComponents fun _ => eqToIso rfl

Equivalence between $C$ and its universe-lifted category $\mathrm{ULiftHom}\, C$

Informal description

The equivalence of categories between a category $C$ and its universe-lifted version $\mathrm{ULiftHom}\, C$, where: - The functor $\mathrm{ULiftHom.up} \colon C \to \mathrm{ULiftHom}\, C$ lifts objects and morphisms to the higher universe. - The inverse functor $\mathrm{ULiftHom.down} \colon \mathrm{ULiftHom}\, C \to C$ projects them back. - The unit and counit natural isomorphisms are identity isomorphisms (induced by equality proofs).

CategoryTheory.AsSmall definition

(D : Type u) [Category.{v} D]

Full source

/-- `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`.
-/
@[nolint unusedArguments]
def AsSmall.{w, v, u} (D : Type u) [Category.{v} D] := ULift.{max w v} D

Small category equivalent to C via universe lifting

Informal description

Given a category `C` of type `Type u` with a category structure `Category.{v} C`, the construction `AsSmall.{w} C` produces a small category equivalent to `C`. The objects and morphisms of `AsSmall C` are obtained by applying the universe lifting operation `ULift` to the objects and morphisms of `C`. The resulting type is `Type (max w v u)`.

CategoryTheory.instSmallCategoryAsSmall instance

: SmallCategory (AsSmall.{w₁} C)

Full source

instance : SmallCategory (AsSmall.{w₁} C) where
  Hom X Y := ULift.{max w₁ u₁} <| X.down ⟶ Y.down
  id _ := ⟨𝟙 _⟩
  comp f g := ⟨f.down ≫ g.down⟩

Small Category Structure on Universe-Lifted Category

Informal description

The category `AsSmall.{w₁} C` is a small category, where `C` is a category in a higher universe. This instance provides the category structure on `AsSmall C`, which is obtained by universe lifting the objects and morphisms of `C`.

CategoryTheory.AsSmall.up definition

: C ⥤ AsSmall C

Full source

/-- One half of the equivalence between `C` and `AsSmall C`. -/
@[simps]
def AsSmall.up : C ⥤ AsSmall C where
  obj X := ⟨X⟩
  map f := ⟨f⟩

Universe-lifting functor from $C$ to $\text{AsSmall} C$

Informal description

The functor `AsSmall.up` maps an object $X$ in category $C$ to its universe-lifted counterpart $\langle X \rangle$ in the small category $\text{AsSmall} C$, and similarly lifts morphisms $f$ in $C$ to $\langle f \rangle$ in $\text{AsSmall} C$.

CategoryTheory.AsSmall.down definition

: AsSmall C ⥤ C

Full source

/-- One half of the equivalence between `C` and `AsSmall C`. -/
@[simps]
def AsSmall.down : AsSmallAsSmall C ⥤ C where
  obj X := ULift.down X
  map f := f.down

Universe-lowering functor from $\text{AsSmall} C$ to $C$

Informal description

The functor that maps an object $X$ in the universe-lifted category $\text{AsSmall} C$ back to its original object $\text{ULift.down} X$ in $C$, and similarly maps a morphism $f$ in $\text{AsSmall} C$ back to its original morphism $f.\text{down}$ in $C$.

CategoryTheory.down_comp theorem

{X Y Z : AsSmall C} (f : X ⟶ Y) (g : Y ⟶ Z) : (f ≫ g).down = f.down ≫ g.down

Full source

@[reassoc]
theorem down_comp {X Y Z : AsSmall C} (f : X ⟶ Y) (g : Y ⟶ Z) : (f ≫ g).down = f.down ≫ g.down :=
  rfl

Compatibility of Composition with Universe-Lowering Functor

Informal description

For any objects $X, Y, Z$ in the universe-lifted category $\mathrm{AsSmall}\, C$ and morphisms $f : X \to Y$, $g : Y \to Z$, the composition of $f$ and $g$ in $\mathrm{AsSmall}\, C$ satisfies $(f \circ g).\mathrm{down} = f.\mathrm{down} \circ g.\mathrm{down}$ in $C$.

CategoryTheory.eqToHom_down theorem

{X Y : AsSmall C} (h : X = Y) : (eqToHom h).down = eqToHom (congrArg ULift.down h)

Full source

@[simp]
theorem eqToHom_down {X Y : AsSmall C} (h : X = Y) :
    (eqToHom h).down = eqToHom (congrArg ULift.down h) := by
  subst h
  rfl

Compatibility of `eqToHom` with universe-lifting down functor

Informal description

For any objects $X$ and $Y$ in the universe-lifted category $\mathrm{AsSmall}\, C$ and any equality $h : X = Y$, the morphism $\mathrm{eqToHom}\, h$ in $\mathrm{AsSmall}\, C$ satisfies $(\mathrm{eqToHom}\, h).\mathrm{down} = \mathrm{eqToHom}\, (\mathrm{congrArg}\, \mathrm{ULift.down}\, h)$ in $C$.

CategoryTheory.AsSmall.equiv definition

: C ≌ AsSmall C

Full source

/-- The equivalence between `C` and `AsSmall C`. -/
@[simps]
def AsSmall.equiv : C ≌ AsSmall C where
  functor := AsSmall.up
  inverse := AsSmall.down
  unitIso := NatIso.ofComponents fun _ => eqToIso rfl
  counitIso := NatIso.ofComponents fun _ => eqToIso <| ULift.ext _ _ rfl

Equivalence between $C$ and its universe-lifted version $\text{AsSmall}\, C$

Informal description

The equivalence of categories between $C$ and $\text{AsSmall}\, C$, where: - The forward functor $\text{AsSmall.up}$ lifts objects and morphisms from $C$ to $\text{AsSmall}\, C$ via universe lifting, - The backward functor $\text{AsSmall.down}$ projects objects and morphisms back from $\text{AsSmall}\, C$ to $C$, - The unit isomorphism is the identity (since $\text{down} \circ \text{up}$ is definitionally the identity on $C$), - The counit isomorphism is induced by the equality $\text{ULift.down} (\text{ULift.up} X) = X$ for any object $X$ in $\text{AsSmall}\, C$.

CategoryTheory.instInhabitedAsSmall instance

[Inhabited C] : Inhabited (AsSmall C)

Full source

instance [Inhabited C] : Inhabited (AsSmall C) :=
  ⟨⟨default⟩⟩

Inhabitedness of Universe-Lifted Categories

Informal description

For any inhabited category $C$, the universe-lifted category $\mathrm{AsSmall}\, C$ is also inhabited.

CategoryTheory.ULiftHomULiftCategory.equiv definition

(C : Type u) [Category.{v} C] : C ≌ ULiftHom.{v'} (ULift.{u'} C)

Full source

/-- The equivalence between `C` and `ULiftHom (ULift C)`. -/
def ULiftHomULiftCategory.equiv.{v', u', v, u} (C : Type u) [Category.{v} C] :
    C ≌ ULiftHom.{v'} (ULift.{u'} C) :=
  ULift.equivalence.trans ULiftHom.equiv

Equivalence between a category and its double-lifted version

Informal description

The categorical equivalence between a category $C$ and the universe-lifted category $\mathrm{ULiftHom}_{\{v'\}} (\mathrm{ULift}_{\{u'\}} C)$, constructed as the composition of: 1. The equivalence $C \simeq \mathrm{ULift}_{\{u'\}} C$ (via $\mathrm{ULift.equivalence}$), and 2. The equivalence $\mathrm{ULift}_{\{u'\}} C \simeq \mathrm{ULiftHom}_{\{v'\}} (\mathrm{ULift}_{\{u'\}} C)$ (via $\mathrm{ULiftHom.equiv}$). This equivalence lifts both objects (via $\mathrm{ULift}$) and morphisms (via $\mathrm{ULiftHom}$) to higher universes while preserving the categorical structure.