Zulip Chat Archive

Stream: general

Topic: quotient.lift


view this post on Zulip Kenny Lau (Dec 18 2020 at 11:05):

Why is quotient.lift not called quotient.descend?

view this post on Zulip Alex J. Best (Dec 18 2020 at 11:10):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Proving.20that.20a.20variable.20is.20of.20a.20given.20type/near/215583327

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Dec 18 2020 at 17:38):

I think the first one is an extend and the second one is a lift.

view this post on Zulip 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

view this post on Zulip Kenny Lau (Dec 18 2020 at 17:41):

if the mods approve

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip Adam Topaz (Dec 18 2020 at 18:04):

Sorry, that was probably wrong :)

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip 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 [/G][\star/G] for example :)

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Dec 18 2020 at 18:10):

nope, it's the other way round... lift is for limits

view this post on Zulip Adam Topaz (Dec 18 2020 at 18:10):

Now I'm confused.

view this post on Zulip Johan Commelin (Dec 18 2020 at 18:10):

the stack [*//G] is so small it can have negative dimension...

view this post on Zulip Johan Commelin (Dec 18 2020 at 18:11):

@Adam Topaz things "descend to the quotient", right?

view this post on Zulip Adam Topaz (Dec 18 2020 at 18:11):

Sure, when I write in latex :)

view this post on Zulip Johan Commelin (Dec 18 2020 at 18:11):

right... I would mind having the same terminology here

view this post on Zulip Johan Commelin (Dec 18 2020 at 18:12):

but in lean everything is a lift (except in category theory)

view this post on Zulip 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

view this post on Zulip Bryan Gin-ge Chen (Dec 18 2020 at 19:52):

We should add a section in our naming conventions page about this.

view this post on Zulip 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: May 14 2021 at 22:15 UTC