[Merged by Bors] - chore: make SimplexCategory.skeletalFunctor a functor to NonemptyFinLinOrdCat.{0}
#7272
Conversation
joelriou
added
t-category-theory
leanprover-community-mathlib4-bot
added
the
merge-conflict
leanprover-community-mathlib4-bot
removed
the
merge-conflict
|
Can you move the PR description above the |
| def skeletalFunctor : SimplexCategory ⥤ NonemptyFinLinOrd where | ||
| obj a := NonemptyFinLinOrd.of (Fin (a.len + 1)) |
There was a problem hiding this comment.
Is the argument here that if you want NonemptyFinLinOrd.{v}, you cam compose with something like NonemptyFinLinOrd.ulift.{v} : NonemptyFinLinOrd.{u} ⥤ .NonemptyFinLinOrd {max u v}?
| { hom := ⟨f, hf.monotone⟩ | ||
| inv := ⟨f.symm, _⟩ | ||
| hom_inv_id := by ext1; apply f.symm_apply_apply | ||
| inv_hom_id := by ext1; apply f.apply_symm_apply } | ||
| intro i j h | ||
| show f.symm i ≤ f.symm j | ||
| rw [← hf.le_iff_le] | ||
| show f (f.symm i) ≤ f (f.symm j) | ||
| simpa only [OrderIso.apply_symm_apply]⟩⟩ |
There was a problem hiding this comment.
I suspect there's a golf hiding here, but it's probably out of scope
|
✌️ joelriou can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-mathlib4-bot
added
delegated
and removed
awaiting-review
|
Thanks! bors merge |
…nLinOrdCat.{0} (#7272)
`SimplexCategory` used to have a universe parameter, but for already some time, it is no longer the case. However, the functor `SimplexCategory.skeletalFunctor` was still a functor from the simplex category to `NonemptyFinLinOrdCat.{v}`. This PR changes this to `NonemptyFinLinOrdCat.{0}`. The main consequence of this is that if `C` is a category, the `n`-simplices of the simplicial set `nerve C` (see `AlgebraicTopology.Nerve`) are now definitionally equal to `Fin (n+1) ⥤ C`.
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
SimplexCategory.skeletalFunctor a functor to NonemptyFinLinOrdCat.{0}SimplexCategory.skeletalFunctor a functor to NonemptyFinLinOrdCat.{0}
SimplexCategoryused to have a universe parameter, but for already some time, it is no longer the case. However, the functorSimplexCategory.skeletalFunctorwas still a functor from the simplex category toNonemptyFinLinOrdCat.{v}. This PR changes this toNonemptyFinLinOrdCat.{0}. The main consequence of this is that ifCis a category, then-simplices of the simplicial setnerve C(seeAlgebraicTopology.Nerve) are now definitionally equal toFin (n+1) ⥤ C.(Previously, there was an annoying
ULift.{0,0}when we unfolded the definition of the nerve.)