challenge: eight sorries away from product-preserving

Stream: Infinity-Cosmos

[Emily Riehl]

A long standing goal is to show that the functor hoFunctor : SSet ⥤ Cat preserves binary products. We are now eight sorries away from this result, and the corresponding result for the restriction hoFunctor : QCat ⥤ Cat. This will be used to construct the 2-category of quasi-categories, modulo a major theorem from @Jack McKoen.

[Notification Bot]

This topic was moved here from #Infinity-Cosmos > eight sorries away from a product-preserving functor by Emily Riehl.

[Emily Riehl]

The eight sorries together with documentation can be found in the draft PR #25010. I'm hoping to challenge some folks here, both past contributors to the infinity cosmos project and other lurkers to help finish them.

[Emily Riehl]

The first is a component of a natural isomorphism that someone could also try to construct:

/-- The Yoneda embedding from the `SimplexCategory` into simplicial sets is naturally
isomorphic to `SimplexCategory.toCat ⋙ nerveFunctor` with component isomorphisms
`Δ[n] ≅ nerve (Fin (n + 1))`. -/
def simplexIsNerve (n : ℕ) : Δ[n] ≅ nerve (Fin (n + 1)) := sorry

[Emily Riehl]

The second observes that the triple composite defined by nerveAdjunction preserves binary products because it is naturally isomorphic to the right adjoint of that adjunction.

/-- Via the whiskered counit (or unit) of `nerveAdjunction`, the triple composite
`nerveFunctor ⋙ hoFunctor ⋙ nerveFunctor` is naturally isomorphic to `nerveFunctor`.
As `nerveFunctor` is a right adjoint, this functor preserves binary products.
Note Mathlib does not seem to recognize that `Cat.{v, u}` has binary products. -/
instance nerveHoNerve.binaryProductIsIso (C D : Type v) [Category.{v} C] [Category.{v} D] :
    IsIso (prodComparison (nerveFunctor ⋙ hoFunctor ⋙ nerveFunctor)
      (Cat.of C) (Cat.of D)) := by
  sorry

Note this might be easier to prove in the form

PreservesLimitsOfShape (Discrete Limits.WalkingPair) (nerveFunctor ⋙ hoFunctor ⋙ nerveFunctor)

in which case the instance CategoryTheory.Limits.instIsIsoProdComparison should be able to infer this result.

[Emily Riehl]

The third sorry follows from the first two results as well as the following proof, which needs golfing:

/-- This proof can surely be golfed. -/
instance hoFunctor.binaryProductNerveIsIso (C D : Type v) [Category.{v} C] [Category.{v} D] :
    IsIso (prodComparison hoFunctor (nerve C) (nerve D)) := by
  have : IsIso (nerveFunctor.map (prodComparison hoFunctor (nerve C) (nerve D))) := by
    have : IsIso (prodComparison nerveFunctor
      (hoFunctor.obj (nerve C)) (hoFunctor.obj (nerve D))) := inferInstance
    have : IsIso (prodComparison (hoFunctor ⋙ nerveFunctor) (nerve C) (nerve D)) := by
      have eq := prodComparison_comp
        nerveFunctor (hoFunctor ⋙ nerveFunctor) (A := Cat.of C) (B := Cat.of D)
      simp only [nerveFunctor_obj] at eq
      have : IsIso
        ((hoFunctor ⋙ nerveFunctor).map
          (prodComparison nerveFunctor (Cat.of C) (Cat.of D))) := inferInstance
      exact IsIso.of_isIso_fac_left eq.symm
    exact IsIso.of_isIso_fac_right (prodComparison_comp hoFunctor nerveFunctor).symm
  apply isIso_of_fully_faithful nerveFunctor

/-- By `simplexIsNerve` this is isomorphic to a map of the form
`hoFunctor.binaryProductNerveIsIso`. -/
instance hoFunctor.binarySimplexProductIsIso (n m : ℕ) :
    IsIso (prodComparison hoFunctor Δ[n] Δ[m]) := sorry

[Emily Riehl]

The fourth and fifth sorries are two instances of the same proof, up to symmetry.

/-- Modulo composing with a symmetry on both ends, the natural transformation
`prodComparisonNatTrans hofunctor Δ[m]` is a natural transformation between cocontinuous
functors whose component at `X : SSet` is `prodComparison hoFunctor X Δ[m]`. This makes use
of cartesian closure of both `SSet.{u}` and `Cat.{u,u}` to establish cocontinuity of the
product functors on both categories.

Using the colimit `Presheaf.colimitOfRepresentable (C := SimplexCategory) X` this reduces to
the result proven in `hoFunctor.binarySimplexProductIsIso`.
-/
instance hoFunctor.binaryProductWithSimplexIsIso (X : SSet) (m : ℕ) :
    IsIso (prodComparison hoFunctor X Δ[m]) := by
  have Xcolim := Presheaf.colimitOfRepresentable (C := ULiftHom SimplexCategory)
    (ULiftHom.down.op ⋙ X)
  sorry

/-- The natural transformation `prodComparisonNatTrans hofunctor X` is a natural
transformation between cocontinuous functors whose component at `Y : SSet` is
`prodComparison hoFunctor X Y`. This makes use of cartesian closure of both `SSet.{u}`
and `Cat.{u,u}` to establish cocontinuity of the product functors on both categories.

/-- The natural transformation `prodComparisonNatTrans hofunctor X` is a natural
transformation between cocontinuous functors whose component at `Y : SSet` is
`prodComparison hoFunctor X Y`. This makes use of cartesian closure of both `SSet.{u}`
and `Cat.{u,u}` to establish cocontinuity of the product functors on both categories.

Using the colimit `Presheaf.colimitOfRepresentable (C := SimplexCategory) Y` this reduces to
the result proven in `hoFunctor.binaryProductWithSimplexIsIso`.
-/
instance hoFunctor.binaryProductIsIso (X Y : SSet):
    IsIso (prodComparison hoFunctor X Y) := by
  unfold SSet SimplicialObject at X Y
  have Ycolim := Presheaf.colimitOfRepresentable (C := ULiftHom SimplexCategory)
    (ULiftHom.down.op ⋙ Y)
  have := prodComparisonNatTrans hoFunctor X
  sorry

UPDATE: The sixth sorry was related to a universe issue in the above that has now been fixed.

[Emily Riehl]

The seventh and eighth sorries are independent of the above, and aim to show that the inclusion of the full subcategory of quasi-categories preserves binary products. (In this case, it preserves all products, though that is not true of the nerve functor.) These should be direct verifications. Perhaps someone like @Jack McKoen or @Joël Riou have proven this already?

/--
QCat is the category of quasi-categories defined as the full subcategory of the category of `SSet`.
-/
def QCat := ObjectProperty.FullSubcategory Quasicategory
instance : Category QCat := ObjectProperty.FullSubcategory.category Quasicategory

/-- As objects characterized by a right lifting property, it is straightforward to directly
verify that. -/
instance QCat.hasBinaryProducts : HasBinaryProducts QCat := sorry

/-- The construction above should form the product in the category `SSet` and verify that this
object is a quasi-category. -/
instance QCat.inclusionPreservesBinaryProducts :
    PreservesLimitsOfShape (Discrete Limits.WalkingPair) (ObjectProperty.ι Quasicategory) := sorry

[Joël Riou]

Emily Riehl said:

/-- As objects characterized by a right lifting property, it is straightforward to directly
verify that. -/
instance QCat.hasBinaryProducts : HasBinaryProducts QCat := sorry

The relevant API to show this is ClosedUnderLimitsOfShape in Limits.FullSubcategory.

[Emily Riehl]

Update: @Andrew Yang solved the universe error, so now only seven sorries remain. I've updated the code above to reflect the current state of the pull request.

[Thomas Murrills]

@Emily Riehl Just checking, is it alright to push directly to #25010? I have some straightforward golfing, and hopefully a proof of the first sorry soon. :)

[Emily Riehl]

Excellent. Absolutely. Please do!

[Emily Riehl]

@Thomas Murrills this is really great, congrats! Do you want to keep your code as part of this PR or break it out into something separate? Either works for me. If it's easiest to keep it here, we can start cleaning things up and trying to put them in their correct place.

In particular, I think it would be good to ask the question on Zulip about the best way to build isomorphisms in Type (or Type-valued functors) from equivalences of types. I'm sure this has come up before and it would be good to ask around about what others have seen. Do you want to ask a question of this nature on the mathlib4 thread (or some general thread if you have another idea) and point to some of your code as an example? If you don't mind, @ me so I'll see it.

[Emily Riehl]

And @Thomas Murrills (or anyone else), if you're looking for something else to do, here's a place where I could use some help.

In this file in the infinity-cosmos repository, we apply the results of PR #25010 and the construction of the strict bicategory of a Cat-enriched category to construct the 2-category of quasi-categories. But there is one more result we need: namely that the homotopy category functor preserves the terminal object. I tried to prove this, using the result that @Thomas Murrills just proved, but got stuck (update: at just one) at a few places:

def simplexIsNerve (n : ℕ) : Δ[n] ≅ nerve (Fin (n + 1)) := sorry

noncomputable def iso : hoFunctor.obj Δ[0] ≅ Cat.of (Fin 1) :=
  hoFunctor.mapIso (simplexIsNerve 0) ≪≫ nerveFunctorCompHoFunctorIso.app (Cat.of (Fin 1))

def finOneTerminalIso' : Cat.of (Fin 1) ≅ Cat.of (Discrete PUnit) where
  hom := toCatHom (star (Fin 1))
  inv := toCatHom (fromPUnit 0)
  hom_inv_id := ComposableArrows.ext₀ rfl
  inv_hom_id := rfl

instance DiscretePUnit.isTerminal : IsTerminal (Cat.of (Discrete PUnit)) :=
  IsTerminal.ofUniqueHom (fun C ↦ star C) (fun _ _ => punit_ext' _ _)

noncomputable def finOneTerminalIso : ⊤_ Cat.{u, u} ≅ Cat.of (Discrete PUnit.{u + 1}) :=
  terminalIsoIsTerminal DiscretePUnit.isTerminal

noncomputable def hoFunctor.terminalIso : (hoFunctor.obj (⊤_ SSet)) ≅ (⊤_ _) :=
  hoFunctor.mapIso (terminalIsoIsTerminal isTerminalDeltaZero) ≪≫ iso ≪≫
    finOneTerminalIso' ≪≫ finOneTerminalIso.symm

--- Why can't I just exact this?
instance hoFunctor.preservesTerminal : PreservesLimit (empty SSet) hoFunctor := by
  have := preservesTerminal_of_iso hoFunctor hoFunctor.terminalIso
  sorry

Update: I made some progress with the universe errors and now am a lot closer. Can anyone help?

[Emily Riehl]

If there is a more efficient way to do this that would also be appreciated. This code is pretty ugly!

[Thomas Murrills]

Emily Riehl said:

Thomas Murrills this is really great, congrats! Do you want to keep your code as part of this PR or break it out into something separate?

I'm fine with either too! On the one hand these definitely belong somewhere else, but on the other hand splitting PRs can be, well, kind of a pain—especially because the home is not clear for some of these, so discussion might be needed. OrderHom.isoFunctor needs the category instance on Type u, which leads #find_home! to list a bunch of mostly unrelated files where the imports happen to be available. Or, should it just be an equivalence of types, and we leave the isomorphism to be built on the fly? Etc.

If we can leave it here with a TODO (and I'll relocate them once this is discussed) that might be easiest! :)

In particular, I think it would be good to ask the question on Zulip about the best way to build isomorphisms in Type (or Type-valued functors) from equivalences of types.

Just to be clear, do you mean whether we should in fact be defining and composing isomorphisms in Type _ in the first place (as opposed to defining Equivs, then using Equiv.toIso only when necessary after composing those as Equivs), or the thing about whether to use RepresentableBy? (Or something else?) (There are a lot of questions I have at this stage, so I could ask a lot of things! :blush:)

(If there's some doubt about using isomorphisms in Type in the first place over equivs, I'll hold off on asking about locations for OrderHom.isoFunctor for a moment, in case it shouldn't exist!)

In this file in the infinity-cosmos repository [...]

Ooh, interesting. I'll take a look!

[Emily Riehl]

@Thomas Murrills I just pushed some code Dom and I wrote which you can find in the infinity-cosmos repository to  #25010.

We had to build a lot of infrastructure about terminal categories in arbitrary universes to get everything to work. In particular, this uses a higher universe version of your SimplexIsNerve that we left with a sorry.

It would be great to find out that all of this is unnecessary: i.e., if we can check that hoFunctor preserves the terminal object at universe level zero and then conclude that it does so at any universe level. If you can figure out how to do that let me know and I'll gladly cut much of what we just added!

[Emily Riehl]

In the meanwhile, if you want to get zulip's advice on any of your code, please go ahead. In particular, if you want to ask about some of the questions you had in comments, that would be great.

[Thomas Murrills]

(Just wanted to mention that I've been busy the past day or two and might continue to be busy for the next day or two, but am still thinking about this, and will post some thoughts when I get the chance :) )

[Emily Riehl]

Great! In the meanwhile, an update: a new approach to the preservation of terminal objects is now in #25459 (suggested by @Robin Carlier). Along the way we're finally PRing stuff about terminal objects in simplicial sets developed by @Adam Topaz and @Zeyi Zhao to mathlib.

I still think we might need some generalization of your simplexIsNerveto arbitrary universe levels so that issue (plus the remaining sorries here) is wide open.

[Emily Riehl]

Update: because of the new PR from fork infrastructure, the four PRs associated with this challenge now have new numbers: #25780, #25781, #25782, #25784.

(Aside, if you are confused about how to move exiting PRs to a newly created mathlib fork, I can tell you how I did this. Once I had a few questions answered, it wasn't so difficult.)

[Emily Riehl]

A disadvantage of the new set up is that it's a little more complicated to contribute collaboratively to PRs. Either

(i) I can add you as a collaborator on my mathlib fork, or
(ii) you can make a PR to one of these branches on my mathlib fork.

I don't really understand how (ii) works but either way I want to make it clear that I'd very much welcome further golfing, edits, or contributions of any sort. So let me know if you want to try to change something on them and we'll figure out how to make it work.

[Thomas Murrills]

Thomas Murrills said:

busy for the next day or two

Well...turns out I was busy for almost three weeks! :face_with_spiral_eyes: :sweat_smile: But, I'm a lot more (reliably) free now. :)

In the past couple weeks I've had some thoughts on managing universe issues in category theory and in this project specifically.

I'm going to put more extensive thoughts in new topics. But tl;dr:

• Some relationships like Functor and Equivalence do not demand the universe levels of the things they relate are the same, but some, e.g. Isos, do. We're missing a "u-flexible" analogue of Isos in Mathlib's 1-cat Cat, where Isos correspond to strict equivalences between categories, not Equivalences. This forces us to solve universe issues before composing instead of after, and the latter might be smoother. (#Infinity-Cosmos > Universe issues: relating across universes)
• Some relevant constructions like Δ[n] are universe polymorphic, but nonetheless get all their data from a single low universe level. We could maybe create automation to ulift definitions when possible and then apply this ulifting appropriately during composition. (#Infinity-Cosmos > Universe issues: ulifting from low-u data )

Disclaimer: I say some very basic things in those messages! :sweat_smile: This is because I'm still familiarizing myself with the situation, and am writing in a way that I myself can understand. So please assume that any very basic statement is directed only at myself! :grinning_face_with_smiling_eyes:

[Thomas Murrills]

Note: I've just opened #26415 which should split out the basic OrderHom definitions into a small PR. :)

[Emily Riehl]

I'm trying to get #25780 ready for review. So in particular, it would be helpful if @Thomas Murrills could fill me in on what code should stay here vs what has been/is being migrated elsewhere. In particular, I can't find your original simplexIsNerve nor do I remember the status of our attempts to generalize to an arbitrary universe level.

There's also something broken that @Andrew Yang wrote that I haven't figured out how to fix. There used to be an import of a file AlgebraicTopology.SimplicialSet.ColimitOfRepresentable that I cut because it doesn't seem to exist. But now there seems to be some difficulty in applying the general CategoryTheory.Presheaf.colimitOfRepresentable in the case of a simplicial set X because Lean fails to unify SSet with a type of presheaves.

[Thomas Murrills]

Okay—I will do these things tomorrow! :)

[Emily Riehl]

Thomas Murrills said:

Okay—I will do these things tomorrow! :)

Thanks! LMK how it goes...

[Thomas Murrills]

Alright, I've done some work on this!

• I've removed the OrderHom functionality being upstreamed in #26415 (and effectively based the PR on that one, which I hope will be merged soon)
• I've also restored simplexIsNerve (as far as I'm aware, it's the original—was there another?), and included the ULiftFin version for now.
• and I've golfed some things, as well as cleaned up the ULiftFin API a bit (but without major changes).

I've made a PR to your fork; would it be alright to gain write access and push directly to the branch in future? :) (Or, if you prefer to receive changes in PR form, that's of course fine with me too!)

[Thomas Murrills]

Re: the status of generalizing to arbitrary universe levels, there were three things that might be relevant (iirc):

• It could be nice to move from ULfitHom <| ULift C to ULiftCat C. I'd be happy to do the work to change the API here if desired; I'd like to ask what people think in #mathlib4.
• I've also been working on finding a good StrictEquivalence definition. This would give us a u-flexible means of composing things which are morally isomorphisms in Cat, but which can't be so due to the u-rigidity of Cat isos. Then we could compose a string of u-flexible StrictEquivalences whose start and end are in the same universe, and put that in Cat, maybe(??) letting us get rid of ULiftFin.
• I'm interested in figuring out how to move between universes in general! The error you mention above is actually (potentially) another example, as it happens. Presheaf.colimitOfRepresentable makes a choice that constrains a universe in its argument to be smaller than necessary. (If it were too big, that would be fine—just ulift.) Generalizing this universe parameter in the original file seems plausible, but then the whole file needs to be reworked (starting all the way up at functorToRepresentables), uliftFunctors need to be inserted everywhere, potential pitfalls await, etc.

I've found that ULifting in general suffers from a number of unfortunate properties, such as ULift.{u,u} not being the identity, ULift.{v} <| ULift.{w} A not being defeq to ULift.{max v w} A, the implications for manipulating terms of these types, etc. (since it's really just a one-field structure). So, one has to rely on the "algebraic" properties surrounding ULifts (if they can be called that): the properties of equivs, equivalences, functors, etc.

I'd love to figure out some sort of automation as hinted at in #Infinity-Cosmos > Universe issues: ulifting from low-u data, but I'm not sure how it would even work yet in principle.

I'll post about StrictEquivalence and ULiftCat in #mathlib4 tomorrow or Saturday. :)

[Thomas Murrills]

I'm also a little confused by lean's refusal to see X as something of type ?_ᵒᵖ ⥤ Type ?u after Presheaf.colimitOfRepresentable. If I try to recreate the issue with something like

def F {α} [Category α] (_ : αᵒᵖ ⥤ Type*) : True := trivial

variable (x : SSet.{u})

#check F x

it shows no signs of trouble.

If I add a coercion of the form

instance : Coe SSet.{u} (SimplexCategoryᵒᵖ ⥤ Type u) := ⟨id⟩

the application type mismatch for X disappears, and is replaced by a failure to synthesize a certain Category (which I believe, in this case, hints at the deeper universe issue I mentioned above).

I wonder if the application mismatch wouldn't have occurred if the typeclass synthesis would succeed, or something strange like that? (If so, I'd suspect that something to do with backtracking and/or metavariable synthesis order/postponement was to blame...)

[Emily Riehl]

Invite sent. Let me look at all of this now.

[Emily Riehl]

An update for @Thomas Murrills and anyone else who might be interested. After bumping mathlib (with the update from the now merged #26415) I copied across a few definitions and one sorried theorem from @Joël Riou's PR #27576 and then was finally able to fix the rest of our proof at a generic universe level! See the current version of #25780.

[Emily Riehl]

It would be more natural to just base #25780 on top of #27576 but I don't actually know how to do this...

Anyway we're nearly there. If folks want to help with the golfing that would be appreciated.

[Thomas Murrills]

Emily Riehl said:

It would be more natural to just base #25780 on top of #27576

I think it's fine to just merge the branch of #27576 and then indicate the dependence in the PR! :) I've pushed this change (but can't edit the PR description) along with some minor golfing and small modifications (but happy to revert if you'd rather not, after all).

[Emily Riehl]

Updated the description. Let me know if you'd like me to add/change anything.

[Emily Riehl]

@Thomas Murrills I attempted to fix an unused argument error by cutting the [Category.{v} C] from

/-- The type-level equivalence between `C` and `ULiftHom (ULift C)`. -/
def ULiftHomULiftCategory.objEquiv.{v', u', u} {C : Type u} :
    C ≃ ULiftHom.{v'} (ULift.{u'} C) :=
  Equiv.ulift.symm.trans ULiftHom.objEquiv

Since this is an equivalence between underlying type aliases, it makes sense that the category instance isn't needed. But does dropping the universe variable v mess something up?

[Thomas Murrills]

Oops, sorry, I indeed shouldn’t have left [Category.{v} C] in there in the first place! It should be fine, but if that does somehow cause any universe issues, they ought to be fixed without touching that def anyway.

[Thomas Murrills]

(Huh, there's a weird error involving the cache. I've merged master, but don't see anything particularly cache-y or dependency related in the new commits...I guess we'll see if it happens again!)

[Thomas Murrills]

By the way: if, in the PR description, below the ---, you format the dependence as

- [ ] depends on: #27576

(without code fencing) the dependent-issues bot will pick it up, and keep the PR labeled appropriately!

[Emily Riehl]

Thanks. I think it's finally ready for review (modulo the dependency)!

[Emily Riehl]

Whelp the dreaded PR #25780 is broken again with a universe error I can't fix. I've just pushed a commit that I hope clarifies exactly where the problem lies

[Emily Riehl]

This first thing that seems weird is in the SimplexCategory/Defs.lean file where we have:

/-- Homs in `SimplexCategory` are equivalent to functors between finite linear orders, with
codomain lifted to a higher universe. -/
def homEquivFunctorULiftRight {a b : SimplexCategory} :
    (a ⟶ b) ≃ (Fin (a.len + 1) ⥤ ULiftFin.{0, v} (b.len + 1)) :=
  SimplexCategory.homEquivOrderHom.trans OrderHom.equivFunctor
    |>.trans ULiftHomULiftCategory.equivCongrLeft

In particular I can't replace the universe level 0 by a generic universe level u even though I think ULiftHomULiftCategory.equivCongrLeft should let me do this.

[Emily Riehl]

I suspect this is the reason why the proof shown here only works when the first universe level of ULiftFin is 0:

/-- The n-simplex is isomorphic to the nerve of the ordinal category `ULiftFin (n + 1)`. -/
def simplexIsNerveULiftFin (n : ℕ) : Δ[n] ≅ nerve (ULiftFin.{0, u} (n + 1)) :=
  NatIso.ofComponents
    (fun i ↦ Equiv.toIso <| stdSimplex.objEquiv.trans SimplexCategory.homEquivFunctorULiftRight)

/-- The n-simplex is isomorphic to the nerve of the ordinal category `ULiftFin (n + 1)`. -/
def simplexIsNerveULiftFin' (n : ℕ) : Δ[n] ≅ nerve (ULiftFin.{u, u} (n + 1)) := sorry

The second sorried statement is the one we actually need in the NerveAdjunction file.

[Thomas Murrills]

Got pinged for this thread, and while unfortunately I have very little time in general this week, I was curious! The issue comes from the following chain of facts:

• the category instance for ULiftFin comes from ULiftHom.category applied to the category instance for ULift (Fin _)
• the category instance for ULift (Fin _) comes from the SmallCategory instance on it (docs#Preorder.smallCategory) (which in turn comes from the Preorder instance on ULifted Preorders, which is fine as-is and not an obstacle)
• The universe level for objects in small categories is by definition the same as the universe level for arrows; so by lifting the objects in Fin _ to u and then relying on its small category instance, we've inadvertently lifted the arrows in the category ULift.{u} (Fin _) to u as well!

In general, maybe we should not get category instances on Preorders from small categories—is there a good reason why the library is set up this way? Currently the Hom U V is ULift (PLift (U ≤ V)), but we don't need the outer ULift. (Is there a better instance elsewhere? I notice this one has lower priority.)

In the meantime, I wonder if supplying a different instance just for ULiftFin somehow would be acceptable; if we do so by writing e.g.

-- Don't lift arrows
attribute [local instance] uliftCategory

instance {n : ℕ} : Category (ULiftFin n) := ULiftHom.category

in Mathlib.CategoryTheory.ComposableArrows, it does get the job done! (Though I'm not sure this is exactly what we should do; there are many ways to "fix" this, and this is just a quick proof of concept.)

[Aaron Liu]

Can we make the category instance on preorders a Category.{v, u} (with universe parameters in both arguments) instead of SmallCategory.{u} (which is Category.{u, u})? Or is that a bad idea since it leads to multiple category instances (they're in different universes so it's probably fine?)

[Aaron Liu]

I think this also gets rid of the diamond with uLiftCategory (but I haven't checked)

[Thomas Murrills]

An alternative is making it a Category.{0, u}, and relying on ULiftHom when we want to lift the arrows (to avoid diamonds there)

[Fernando Chu]

Just wondering, do you know of a situation where you want to lift arrows? I was also thinking of making it Category.{0, u} for an entirely different problem (the ThinSkeleton of a category is defined as a poset, and therefore if a category HasLimits it does not follow that its ThinSkeleton has limits too).

[Emily Riehl]

As @Thomas Murrills pointed out the problem (from the point of view of our main theorem) might not be with universe levels but with category instances, so perhaps there is an easier fix? What I need in that the n-simplex as an object of type SSet.{u} (for arbitrary u) is isomorphic to the nerve of some category. If our ULiftFin has objects at universe level u and morphisms at universe level 0 then its nerve should be a simplicial set at universe level max {0,u} = u, which should be fine? But I couldn't get the code to work ...

[Aaron Liu]

Emily Riehl said:

But I couldn't get the code to work ...

what's wrong?

[Thomas Murrills]

Aaron Liu said:

Emily Riehl said:

But I couldn't get the code to work ...

what's wrong?

See the sorry above!

[Aaron Liu]

there's a lot above, where above?

[Aaron Liu]

oh is it

Emily Riehl said:

I suspect this is the reason why the proof shown here only works when the first universe level of ULiftFin is 0:

/-- The n-simplex is isomorphic to the nerve of the ordinal category `ULiftFin (n + 1)`. -/
def simplexIsNerveULiftFin (n : ℕ) : Δ[n] ≅ nerve (ULiftFin.{0, u} (n + 1)) :=
  NatIso.ofComponents
    (fun i ↦ Equiv.toIso <| stdSimplex.objEquiv.trans SimplexCategory.homEquivFunctorULiftRight)

/-- The n-simplex is isomorphic to the nerve of the ordinal category `ULiftFin (n + 1)`. -/
def simplexIsNerveULiftFin' (n : ℕ) : Δ[n] ≅ nerve (ULiftFin.{u, u} (n + 1)) := sorry

The second sorried statement is the one we actually need in the NerveAdjunction file.

[Aaron Liu]

I can't figure out which namespaces to open to get this compiling

[Thomas Murrills]

I’d say pull the PR, and play with them in their respective files instead of trying to get them to work in a standalone fashion

[Thomas Murrills]

(Though to be clear modifying the instance as I mentioned does get things working! :) )

[Thomas Murrills]

Unless, @Emily Riehl, are you saying that ideally we shouldn’t actually need ULiftFin.{u,u} there in the first place, and the NerveAdjunction file shouldn’t require ULiftFin.{u,u} (with arrows at u) but only ULiftFin.{u,0} (with arrows at 0)? (hang on, I think I got myself turned around here)

[Aaron Liu]

If you swap the ULifts around you can get ULiftFin.{u, v} to have arrows in v instead of max u v which might be simpler

[Thomas Murrills]

Okay, so just to recap (at least for myself!): the issue is that the current category instance for ULiftFin requires the arrows to be in a higher universe than the objects, and this is due to relying on Preorder.smallCategory (and can be fixed by relying on uliftCategory instead).

[Emily Riehl]

At this point @Thomas Murrills understands things better than I do. I suspect (but am not 100% certain) that we don't actually need ULiftFin.{u,u} and perhaps the currently non-sorried simplexIsNerveULiftFin would be fine once we resolve some the confusing about category instances.

[Emily Riehl]

If anyone has advice on the easiest way to fix this, that would be great. Even better if it's something that can be done in this PR, so we don't have to rebase it on something else. But if this uncovers a longer term issue that needs fixing than so be it.

[Emily Riehl]

Thanks to @Mario Carneiro #25780 is finally fixed and ready for review!