Universes of simplicial sets

Stream: maths

[Brendan Seamas Murphy]

I've been doing some stuff with singular homology and have run into universe issues. I think the problem is that the functor Top.to_sSet has no universe parameter, it always has type Top.{0} ⥤ sSet.{0}. Is there a good reason for this/am I misunderstanding something here? If not, I guess I'll have to edit mathlib's simplicial sets files

[Thomas Browning]

Make a PR :grinning:

[Brendan Seamas Murphy]

Sure, I'll look into it. Also, just for my future reference if I am making a PR to fix universe stuff, it seems like lemma Module.cokernel_π_ext has also overspecialized universes (the carrier type of the category of modules over R is forced to live in the same universe as R)

[Brendan Seamas Murphy]

also, category_theory.nat_trans.app_zero requires [preadditive D] when it really only needs [has_zero_morphisms D]

[Brendan Seamas Murphy]

also also, algebraic_topology.topological_simplex.simplex_category.to_Top_obj should probably be defined in terms of analysis.convex.basic.std_simplex

[Adam Topaz]

Ha, yeah I noticed these universe issues when I was playing with singular homology a while ago
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Ext.20and.20Tor/near/246037632
but I never got around to relaxing the universes for Top.to_sSet. Please(!) open a PR for this @Brendan Seamas Murphy ! (I can try to do it soon if you prefer)

[Brendan Seamas Murphy]

Sure, I'll start on it tonight. Could you give me permission to submit PRs to mathlib? My github username is Shamrock-Frost

[Kyle Miller]

@Brendan Seamas Murphy Just sent an invite

[Brendan Seamas Murphy]

thanks!

[Brendan Seamas Murphy]

I'm working on this now and I've pinpointed the source of the universe issues. If we add in some implicit arguments, the standard simplex is defined by this:

def standard_simplex : simplex_category ⥤ sSet :=
  @yoneda.{0 0} simplex_category simplex_category.small_category

This doesn't immediately generalize to simplex_category ⥤ sSet.{u}, but we could change it to

def standard_simplex : simplex_category ⥤ sSet.{u} :=
  (@yoneda.{0 0} simplex_category simplex_category.small_category)
  ⋙ whiskering_right.obj (ulift_functor.{u 0})

which sends [n] to the (Type u)-valued presheaf it represents. This does make things sort of awkward when using the standard n simplex, since we need to insert ulift.up and ulift.down in places, but it's the best workaround I could think of. It seems like this is a more general thing though, turning an object in a small category into presheaf of large sets. Would it be a good idea to generalize the definition of yoneda in category_theory.yoneda by adding another universe parameter? Or maybe to define a new functor like ulift_yoneda to be this composition and prove various lemmas about it like those in category_theory.yoneda? I'm not sure what the right move is here, suggestions are appreciated

[Brendan Seamas Murphy]

Also I couldn't find whiskering_right at first and so I defined the left and right composition composition functors of a bicategory, then specialized them to Cat, then found out this doesn't work! We can't take "whiskering in Cat" as a special case of whiskering in an arbitrary bicategory because category_theory.whiskering_left is polymorphic in the universes of the various categories. I'm sure someone has noticed this before, but I thought it was interesting. I'm planning to submit a pr for the bicategory stuff after I finish resolving the sSet universe issues

[Brendan Seamas Murphy]

Oh nevermind, it looks like what I did has been added on the bicategory branch

[Brendan Seamas Murphy]

Changing yoneda would break a lot of code and require clients of the code to insert ulift.up and ulift.down everywhere, but if we don't do it this way it seems like we'd have a bunch of duplicate code? I don't really know what the right option is here

[Thomas Browning]

Could you deduce the usual Yoneda from the universe-generalized Yoneda?

[Thomas Browning]

If so, then having a couple versions of Yoneda seems fine to me, as long as there are docstrings explaining the differences.

[Brendan Seamas Murphy]

I don't think so, since universe generalized yoneda involves ulifting

[Yaël Dillies]

You can still transfer properties across ulift, though.

[Reid Barton]

Another strategy would be to first lift simplex_category into the target universe

[Adam Topaz]

docs#category_theory.as_small.up would help with that, for example

[Adam Topaz]

But I think

def standard_simplex : simplex_category ⥤ sSet.{u} :=
yoneda ⋙ (whiskering_right _ _ _).obj ulift_functor

is the right approach here.

[Brendan Seamas Murphy]

Gave a shot at using the definition you gave here. I figured we'll want to use this universe generalized yoneda lemma for other things (eg cubical or dendroidal sets) so I defined a "uyoneda" function. It got pretty hairy, do people think the changes I made here are viable? I don't want to spend more time on this approach if it's a dead end https://github.com/leanprover-community/mathlib4/tree/simplicial-set-fixes

[Reid Barton]

It does look a bit hairy. I would prefer not to duplicate so much of the API.
I wonder how viable it would be to have a single yoneda that is universe-polymorphic. The ULift.up/down stuff is a bit annoying, but what I'm more worried about is that we might need to specify universe levels in many places. Maybe we can hold out for universe level inequalities?

[Reid Barton]

Did this kind of issue ever show up in LTE? viewing a u-small profinite set as a (pre)sheaf of u+1-small sets

[Reid Barton]

I think the path of least resistance for now might be to define the embedding sSet.{0} -> sSet.{u} (which we will probably want to also apply to things that aren't representable) and use that in the definition of standard_simplex

[Reid Barton]

It should be possible to insulate oneself from the specific definition of yoneda by using yoneda.map/yoneda.preimage instead--basically, just using the fact that it is a fully faithful functor.

[Reid Barton]

Semi-relatedly, once you get the theory off the ground, I think you generally want to represent a simplex of a simplicial set as a map from a standard_simplex