ULift in concrete categories

Stream: Is there code for X?

[Christian Merten]

Currently there is docs#CategoryTheory.uliftFunctor for universe lifting functorially from Type u to Type (max u v) and docs#CategoryTheory.ULift.upFunctor for general categories. Is there a convenient way to obtain for example:

import Mathlib

universe u₁ u₂

def MonCat.uliftFunctor : MonCat.{u₁} ⥤ MonCat.{max u₁ u₂} where
  obj X := MonCat.of (ULift.{max u₁ u₂, u₁} X)
  map {X Y} f := MonCat.ofHom <|
    ⟨⟨fun x ↦ ULift.up (f x.down), by simp; rfl⟩, fun x y ↦ by simp; rfl⟩
  map_id X := by simp; rfl
  map_comp {X Y Z} f g := by simp; rfl

[Eric Wieser]

Maybe slightly better:

import Mathlib

universe u₁ u₂

open CategoryTheory

def MonCat.uliftFunctor : MonCat.{u₁} ⥤ MonCat.{max u₁ u₂} where
  obj X := MonCat.of (ULift.{max u₁ u₂, u₁} X)
  map {X Y} f := MonCat.ofHom <|
    MulEquiv.ulift.symm.toMonoidHom.comp <| f.comp MulEquiv.ulift.toMonoidHom
  map_id X := by rfl
  map_comp {X Y Z} f g := by rfl

[Eric Wieser]

There should be something akin to docs#MulEquiv.ulift for each category you care about, so the pattern is at least easy to repeat

[Christian Merten]

Thanks, so no general construction in sight? Having this for MonCat, CommMonCat, GroupCat, CommGroupCat seems quite messy.

[Christian Merten]

Maybe there could be a "faithful ULift" typeclass on bundled categories.

[Eric Wieser]

Do you mean bundled categories, or concrete categories?

[Christian Merten]

I was actually thinking bundled categories, and thought of something along the lines of

import Mathlib

set_option checkBinderAnnotations false

universe u v

def ClassFactory := Type u → Type u

def HomFactory (c : ClassFactory.{u}) (c' : ClassFactory.{v}) :=
  ∀ ⦃α : Type u⦄ ⦃β : Type v⦄ (_ : c α) (_ : c' β), Type (max u v)

variable {c : ClassFactory.{u}} {c' : ClassFactory.{max u v}}
  (hom : HomFactory c c)
  (homLiftUp : HomFactory c c')
  (homLiftDown : HomFactory c' c)
  (homUp : HomFactory c' c')

class FaithfulULift where
  uliftInst (x : Type u) (s : c x) : c' (ULift.{max u v, u} x)
  uliftHom (x : Type u) (s : c x) : homLiftUp s (uliftInst x s)
  uliftInv (x : Type u) (s : c x) : homLiftDown (uliftInst x s) s
  -- a condition on composition of uliftHom and uliftInv, needs some inter-universal BundledHom maybe?

variable [BundledHom hom] [BundledHom homUp]

def BundledHom.uliftFunctor [inst : FaithfulULift.{u, v} homLiftUp homLiftDown] : (Bundled c) ⥤ (Bundled c') where
  obj X := @Bundled.of c' (ULift.{max u v, u} X) (inst.uliftInst X X.str)
  map {X Y} f := by
    show @homUp (ULift.{max u v, u} X) (ULift.{max u v, u} Y) (inst.uliftInst X X.str) (inst.uliftInst Y Y.str)
    -- inter-universal BundledHom might yield: uliftHom ∘ f ∘ uliftInv
    admit
  map_id := sorry
  map_comp := sorry

To make this work, I need some inter-universal BundledHom that allows composing homs between objects in different universes, as it is the case for MonoidHom. But for this I would like to quantify over universes, which I think is not possible?