Zulip Chat Archive
Stream: maths
Topic: Universe restriction for sheaves
Adam Topaz (Jan 21 2022 at 17:43):
@Andrew Yang why does one need C and D to be small categories in this line?
https://github.com/leanprover-community/mathlib/blob/9c39019f05579b5d0792661515c1d91636a180e4/src/category_theory/sites/dense_subsite.lean#L458
Adam Topaz (Jan 21 2022 at 17:45):
Is it because you use Kan extensions somewhere?
Andrew Yang (Jan 21 2022 at 17:49):
I think so. The construction of the glued sheaf is by definition the right kan extension of the original sheaf along the inclusion functor.
Adam Topaz (Jan 21 2022 at 17:49):
Right, that's what I figured.
Adam Topaz (Jan 21 2022 at 17:50):
It's causing me some issues unfortunately. Can we geeneralize the universes for Kan extensions using the max trick?
Andrew Yang (Jan 21 2022 at 17:55):
How general do you need it to be? I think the smallness condition is quite essential here.
Adam Topaz (Jan 21 2022 at 17:57):
Well, if A : Type w and category.{max u v} A, then we could presumably take C : Type u with category.{v} C and similarly for D.
Adam Topaz (Jan 21 2022 at 17:57):
Or maybe C : Type (max u v).
Adam Topaz (Jan 21 2022 at 17:57):
I wish we had a way of using inequality on universe parameters...
Riccardo Brasca (Jan 21 2022 at 17:58):
Adam Topaz said:
I wish we had a way of using inequality on universe parameters...
We all wish...
Kevin Buzzard (Jan 21 2022 at 17:58):
Feature request for Lean 5
Adam Topaz (Jan 21 2022 at 17:58):
Or lean 37?
Kevin Buzzard (Jan 21 2022 at 17:58):
I never wish it, I just go back to using Type and remember how in the old days I used to believe in ZFC
Kevin Buzzard (Jan 21 2022 at 18:00):
I had an interesting conversation with Jeremy about that approach yesterday; I said "obviously universes are dangerous because all mathematicians are happy with ZFC but the moment you start using universes you're assuming the consistency of a strictly stronger theory, which is an unnecessary risk". His reply, which caught me completely off guard, was "yes -- you're assuming ZFC is consistent -- and if you didn't believe that then what the heck are you doing working in ZFC in the first place!"
Adam Topaz (Jan 21 2022 at 18:00):
I mean there is no reason why something can't hold for non-small sites, because you can always promote a category to a small category over max v u. You just need the morphisms of the target category to be at the same level, and things should work. I could try to trek my way through with ulifts and such, but it would be nicer if we could just arrange the universes to work.
Andrew Yang (Jan 21 2022 at 18:10):
Adam Topaz (Jan 21 2022 at 18:11):
Awesome! Thank you!
Adam Topaz (Jan 21 2022 at 18:14):
I must say I'm very happy that generalizing the universes for Kan extensions was so easy once you have the right instances :)
Last updated: Dec 20 2023 at 11:08 UTC