Zulip Chat Archive
Stream: general
Topic: quotient.lift
Kenny Lau (Dec 18 2020 at 11:05):
Why is quotient.lift not called quotient.descend?
Alex J. Best (Dec 18 2020 at 11:10):
Kenny Lau (Dec 18 2020 at 14:36):
I'm asking because of this comment about the names of:
(K →+* L) ≃ (perfect_closure K p →+* L)(R →+* S) ≃ (R →+* ring.perfection S p)
How would you name them in terms of this lift / descend / extend / etc. terminiology?
Johan Commelin (Dec 18 2020 at 17:38):
I think the first one is an extend and the second one is a lift.
Kenny Lau (Dec 18 2020 at 17:40):
Well since the first one is called lift in mathlib we can just do a Greenland/Iceland switch
Kenny Lau (Dec 18 2020 at 17:41):
if the mods approve
Bryan Gin-ge Chen (Dec 18 2020 at 17:54):
I'd prefer if we stuck to conventional terminology everywhere that we can. quotient.lift going the wrong way is unfortunate, and flipping more names would only make things worse.
Is there anything we can do about quotient.lift (in Lean 4)? Could we agree to use some alias like quotient.descend everywhere in mathlib instead?
Kenny Lau (Dec 18 2020 at 17:55):
Sebastian Ullrich said:
Kevin Buzzard It is still there as
Quot.lift. Interesting point of view; from a CS standpoint one would say that the quotient type is "structurally bigger", i.e. has one more type constructor, I'd guess. Like lifting monadic values into bigger monads (where no-one wants to think about cardinality).
Adam Topaz (Dec 18 2020 at 18:04):
Sorry, that was probably wrong :)
Kevin Buzzard (Dec 18 2020 at 18:07):
I think we should just blame Grothendieck for not properly understanding that a quotient is bigger than the thing you started with, or perhaps for not putting big stuff on the bottom. "Let S be a base scheme, which we'll put at the top of everything"
Chris Hughes (Dec 18 2020 at 18:07):
I think it's correct if the morphism in the category of types with an equivalence relation are functions that preserve the relation
Adam Topaz (Dec 18 2020 at 18:08):
Kevin Buzzard said:
I think we should just blame Grothendieck for not properly understanding that a quotient is bigger than the thing you started with, or perhaps for not putting big stuff on the bottom. "Let S be a base scheme, which we'll put at the top of everything"
Grothendieck understood this, IMO. Look at things like the stack for example :)
Chris Hughes (Dec 18 2020 at 18:09):
In the category theory library iirc, lift is for colimits and desc is for limits. A quotient is more like a colimits than a limit.
Johan Commelin (Dec 18 2020 at 18:10):
nope, it's the other way round... lift is for limits
Adam Topaz (Dec 18 2020 at 18:10):
Now I'm confused.
Johan Commelin (Dec 18 2020 at 18:10):
the stack [*//G] is so small it can have negative dimension...
Johan Commelin (Dec 18 2020 at 18:11):
@Adam Topaz things "descend to the quotient", right?
Adam Topaz (Dec 18 2020 at 18:11):
Sure, when I write in latex :)
Johan Commelin (Dec 18 2020 at 18:11):
right... I would mind having the same terminology here
Johan Commelin (Dec 18 2020 at 18:12):
but in lean everything is a lift (except in category theory)
Adam Topaz (Dec 18 2020 at 18:13):
I guess I think of lean quotients as more stacky-ish than set-ish, so lift actually makes sense to me
Bryan Gin-ge Chen (Dec 18 2020 at 19:52):
We should add a section in our naming conventions page about this.
Kenny Lau (Dec 20 2020 at 15:08):
So do I have permission to name (R →+* S) ≃ (R →+* ring.perfection S p) as extend as per #5386?
Last updated: Dec 20 2023 at 11:08 UTC