Coend increases universe too much ?

Stream: new members

[Nicolas Rolland]

My composition of distributors P : A -/-> B and Q: B -/-> C has this signature

def comp (P : Dist.{u} A B) (Q: Dist.{u} B C) : Dist.{max u u₂ v₂} A C

where

abbrev Dist.{u, v₂, u₂, v₁, u₁} (A : Type u₁) [Category.{v₁} A]
(B : Type u₂ ) [Category.{v₂} B] :=
Bᵒᵖ × A ⥤ Type u

and

variable {B : Type u₂ } [Category.{v₂} B]

So each time I compose two distributors, composition increases the universes by the category B quantified out .

This is unlike functor composition whose resulting type's universe does not mention the intermediate category's universes

CategoryTheory.comp.{v₁, v₂, v₃, u₁, u₂, u₃} {A : Type u₁} [Category.{v₁, u₁} A]
{B : Type u₂}[Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C]
(F : A ⥤ B) (G : B ⥤ C) : A ⥤ C

Is it going to be a problem for using distributors with lean ?

---

It comes from my implementation of a coend which has this signature (forced upon me by the implementation)

def mycoend : (Bᵒᵖ × B ⥤ Type u) ⥤  Type (max u u₂ v₂) :=
  (CategoryTheory.whiskeringLeft _ _ _ ).obj (CategoryOfElements.π (Functor.hom B)) ⋙ mycolimit

is this universe increase a code smell ?

[Robert Maxton]

That seems strange, yes. Do you have a #mwe?

[Robert Maxton]

Mm. Actually, I suspect it boils down to your definition of coend, indeed; either this is mathematically required and the universe bump is 'real', or you've picked a poor choice of proof/definition for coend and in fact you can get away with something more "forgetful"

[Nicolas Rolland]

Here is the implementation

import Mathlib.CategoryTheory.Category.Cat.Adjunction
import Mathlib.CategoryTheory.Elements

open CategoryTheory

universe v₂ u₂ u
variable {B : Type u₂ } [Category.{v₂} B]

def Functor.ElementsFunctor  : (B ⥤ Type u) ⥤ Cat.{v₂, max u₂ u} where
  obj F := Cat.of.{v₂, max u₂ u} (F.Elements :  Type (max u₂ u) )
  map {F G} n := {
    obj := fun ⟨X,x⟩ ↦  ⟨X, n.app X x ⟩
    map := fun ⟨X, x⟩ {Y} ⟨f,_⟩ ↦
    match Y with | ⟨Y, y⟩ => ⟨f, by have := congrFun (n.naturality f) x;aesop_cat⟩
  }

def mycolimit  : (B ⥤ Type u) ⥤ Type (max u₂ u)
  := @Functor.ElementsFunctor B _ ⋙ Cat.connectedComponents

def mycoend : (Bᵒᵖ × B ⥤ Type u) ⥤  Type (max u u₂ v₂) :=
  (CategoryTheory.whiskeringLeft _ _ _ ).obj (CategoryOfElements.π (Functor.hom B)) ⋙ mycolimit

Not that this computes the colimit, it is not given non constructively by some UP.
Maybe there is another implementation for coend which does not have this shortcoming (is it one?), but that would mean we don't have coend F = colim (F . pi) in general, which would be bad news for abstracting all the way up and use recipes from category theory.

PS : is there an API to tell the universe checker to not bump when we know it's not really necessary ?

[Joël Riou]

Nicolas Rolland said:

PS : is there an API to tell the universe checker to not bump when we know it's not really necessary ?

I do not know this particular example, but Lean does not bump universe unnecessarily. What may happen is that certain types, which are in Type (max u v), may actually be Small.{u} (i.e. in bijection with a type in Type u), so that we may shrink the type to an equivalent type in Type u. We have Shrink.{u} for this.

For some applications, statements may look nicer if you assume that certain categories are small. However, it is also useful to develop the API for more general universes. It may be unclear what is the best/convenient thing to do...

[Nicolas Rolland]

Here's a complete example.
In the end, I do not have coend F = colim (F . pi) unconditionally.

This seems like a big caveat to keep in mind : It holds, modulo some reverse engineering for universes.
Which might be easy to do. Here I force v2 to be equal to u2 for that max v2 u2 u = max u2 u and that is simple enough.

I wonder how annoying this is in practice, and if so, if quantifying over universes would be a solution

import Mathlib.CategoryTheory.Category.Cat.Adjunction
import Mathlib.CategoryTheory.Elements

open CategoryTheory

universe v₂ u₂ u vm um
variable {B : Type u₂ } [Category.{v₂} B]
variable {M : Type vm } [Category.{um} M]
variable (F : (Bᵒᵖ×B) ⥤ M)

structure CoWedge : Type (max (max um u₂) vm) where
  pt : M
  leg (b:B) : F.obj (Opposite.op b,b) ⟶ pt
  cowedgeCondition : ∀ ⦃c c' : B⦄ (f : c ⟶ c'),
     (F.map (f.op, 𝟙 c) ≫ leg c : F.obj (Opposite.op c', c) ⟶  pt)  =
     (F.map ((𝟙 c').op, f) ≫ leg c'  : F.obj (Opposite.op c', c)  ⟶  pt) := by aesop_cat

structure CoWedgeMorphism (x y : CoWedge F) where
  Hom : x.pt ⟶ y.pt
  cowedgeCondition : ∀ (c : B), x.leg c ≫ Hom = y.leg c := by aesop_cat

attribute [simp] CoWedgeMorphism.cowedgeCondition

instance : Category (CoWedge F) where
  Hom := fun x y => CoWedgeMorphism _ x y
  id := fun x => {Hom := 𝟙 x.pt}
  comp := fun {X Y Z} f g => {
    Hom := f.Hom ≫ g.Hom
    cowedgeCondition := fun c => by rw [<- Category.assoc]; aesop_cat }

def NatTrans.mapElements {F G : B ⥤ Type _} (φ : F ⟶ G) : F.Elements ⥤ G.Elements where
  obj := fun ⟨X, x⟩ ↦ ⟨_, φ.app X x⟩
  map {p q} := fun ⟨f,h⟩ ↦ ⟨f, by have hb := congrFun (φ.naturality f) p.2; aesop_cat⟩

def Functor.ElementsFunctor : (B ⥤ Type u) ⥤ Cat.{v₂, max u₂ u} where
  obj F := Cat.of.{v₂, max u₂ u} (F.Elements :  Type (max u₂ u) )
  map {F G} n := {
    obj := fun ⟨X,x⟩ ↦  ⟨X, n.app X x ⟩
    map := fun ⟨X, x⟩ {Y} ⟨f,_⟩ ↦
    match Y with | ⟨Y, y⟩ => ⟨f, by have := congrFun (n.naturality f) x;aesop_cat⟩
  }

def myColimitPt : (B ⥤ Type u) ⥤ Type (max u₂ u)
  := @Functor.ElementsFunctor B _ ⋙ Cat.connectedComponents

----

def myCoendPt : (Bᵒᵖ × B ⥤  Type u) ⥤  Type (max u u₂) where
  obj F := ConnectedComponents F.Elements
  map {f g} n :=
    let as :  Cat.of f.Elements ⟶ Cat.of  g.Elements := NatTrans.mapElements n
    Cat.connectedComponents.map (as)
  map_id f := funext fun xq ↦ by obtain ⟨x,rfl⟩ := Quotient.exists_rep xq; rfl
  map_comp {f g h } n m := funext fun xq ↦ by obtain ⟨x,rfl⟩ := Quotient.exists_rep xq; rfl


def they_might_be_equal  {B : Type u₂} [Category.{u₂, u₂} B] :
  @myCoendPt.{u₂, u₂, u} B _ = @myOtherCoendPt.{u₂, u₂, u} B _ :=  sorry

def they_can't_be_equal  {B : Type u₂} [Category.{v₂, u₂} B] :
  @myCoendPt.{v₂, u₂, u} B _ = @myOtherCoendPt.{v₂, u₂, u} B _  := sorry
-- type mismatch
--   myOtherCoendPt
-- has type
--   (Bᵒᵖ × B ⥤ Type u) ⥤ Type (max u u₂ v₂) : Type (max (max u u₂) (max (max u u₂) v₂) (max (max (max (u + 1) u₂) u) v₂) (max (u + 1) (u₂ + 1)) (v₂ + 1))
-- but is expected to have type
--   (Bᵒᵖ × B ⥤ Type u) ⥤ Type (max u u₂) : Type (max (max u u₂) (max (max (max (u + 1) u₂) u) v₂) (u + 1) (u₂ + 1))L

[Joël Riou]

Could you clarify what exactly is your question? (There may have been issues when copy-pasting: there are unused chunks of code, and undefined terms.)

Universes are necessary. When doing a coend, you consider a quotient of a type that is a disjoint union indexed by the objects in a certain category. In informal mathematics, if that category is large, the "type" may no longer be a set, which can be problematic. On the one hand, universes in Lean offer a way to consider these types as first class citizens, but on the other hand, it requires some care from the user.

[Nicolas Rolland]

This code meant to show that it is not true, in general, that we have coend F = colimit (F . pi) when using what seem to be the most straightforward implementation in lean, because they do not have the same universe constraints.

Not only do you need to jump to a potentially higher universe in both case, but the higher universe you jump to depends on which one you use.So we cannot simply swap a call to one with a call to another.

In (informal?) category theory, we always do have coend F = colimit (F. pi) I think

It's just a surprising caveat I wanted to underline, unless I made a mistake....
So my question would be : does it makes sense ? is it a sign of something fishy ?

[Nicolas Rolland]

(deleted)

[Joël Riou]

There might be something fishy in informal mathematics when we take colimits indexed by large categories.

In Lean/mathlib, we can write colimit only when the colimit is known to exist: this may require suitable assumptions on the universes.

[Joël Riou]

One may to prove something is a colimit is to construct a "cocone" and construct a IsColimit structure. Have you tried this?