quotient.out

Stream: general

[Johan Commelin]

In #12438, Adam uses projectivization.rep as name for a representative of an element in a quotient. I think that's a very sensible name. Should quotient.out (and similar occurences) be renamed to quotient.rep? I think it's a more descriptive name, in line with mathematical terminology.

[Kevin Buzzard]

And how about renaming quotient.lift to quotient.descent while we're at it?

[Johan Commelin]

I would be happy with desc instead of descent (-; But yes!

[Eric Wieser]

One nice thing about the name out is that it's less obvious than rep, which increases the chance of the user being steered towards lift instead which is usually the better choice

[Johan Commelin]

That's another argument for renaming lift to desc.

[Johan Commelin]

src/data/quot.lean doesn't mention anything like "descends to the quotient" in the entire file.

[Eric Wieser]

What's the heuristic for which other lifts should be called desc?

[Eric Wieser]

Presumably docs#quot.lift would be renamed too (do we need buy in from Leo?)

[Johan Commelin]

Compare

• https://duckduckgo.com/?t=ffab&q=descend+to+the+quotient&ia=web
• https://duckduckgo.com/?t=ffab&q=lift+to+the+quotient&ia=web

[Johan Commelin]

Quotients are colimits, and the universal property of a colimit describes how a map descends to the colimit. (That's why we have docs#category_theory.limits.colimit.desc) It's the dual of limits, where the universal property describes how a map lifts to the limit.

[David Wärn]

So this 'descent' changes the domain of a map whereas 'lift' changes the codomain, right?

[Eric Wieser]

If so that would mean that docs#tensor_algebra.lift gets renamed too

[Johan Commelin]

Sure, a tonne of things in mathlib are called lift, because they all copy quot.lift.

[Eric Wieser]

Which doesn't fit the heuristic I had internalized of "T(V) is bigger than V, so it's lift"

[Eric Wieser]

Presumably that's just the wrong mental model, but it's the same one I've seen used in the past to argue for renaming quotient.lift to desc, and seems not to lead to the same conclusions

[Kevin Buzzard]

Certain colimits (perhaps not all?) are typically drawn on the blackboard with the colimit on the bottom

[Kevin Buzzard]

Quotients are an example

[Riccardo Brasca]

The difference with T(V) is that it is bigger than V, so "lift" makes sense here. But it is also a quotient by definition (of something even bigger), so also "desc" makes sense

[Kevin Buzzard]

Right. So colimits in e.g. the category of types (and in many other categories) can be made with a two step process; first a disjoint union (or more general coproduct) and then a quotient. For quotients mathematicians write X at the top and Q underneath, and descend maps X->Y satifying appropriate conditions to maps Q -> Y. However for a disjoint union of two types A and B, what does a mathematician to do maps A->Y and B->Y to get a map A+B -> Y? We "glue" them. So I think we want coproduct.glue and quotient.desc and then colimit.gluedesc or something.

[David Wärn]

I think there's a good sense in which a quotient $A / \sim$ is bigger than $A$: it contains all the elements of $A$ as well as some extra equalities. If you think about it in this way, you might say you extend a map along the quotient map. Either way I think the 'are we changing domain or codomain' distinction is more meaningful than the 'bigger / smaller' one

[Johan Commelin]

"extend" is certainly used a lot in similar settings. I guess the opposite of "extend" is "restrict"? But certainly you can't restrict a map to a limit... that sounds odd :smiley:
In fact, "restrict" should also be an operation that changes the domain. So in that sense it is no the dual of "extend".

[Kevin Buzzard]

I'm saying that I think it might be odd to "descend" maps f : A -> Y and g : B \to Y to f + g : A + B \to Y

[Kevin Buzzard]

I'm saying that I think it might be odd to "descend" maps f : A -> Y and g : B \to Y to f + g : A + B \to Y

[Kevin Buzzard]

Limits are the same: they are built as subsets of products. You can kind of "restrict" a map Y -> A to Y -> B if B is a subset of A and a condition is satisfied, but I guess I "product" two maps Y->A and Y->B to get a map Y -> A x B

[Johan Commelin]

A map "factors" through the kernel, I guess? Maybe it "restricts" or even "lifts"?

[Johan Commelin]

But a map can also factor through a quotient.

[Riccardo Brasca]

"restricts" seems a little odd, unless you want to produce a map from the kernel, but that's easy. I would say "factors", but probably we just use some random terminology without a precise rule

[Patrick Massot]

I don't know any situation where a mathematician would hesitate between "lift" and "descend", so the only reasonable path is to simply follow mathematics conventions. And indeed for tensor algebra the obvious answer is neither descends nor lifts, it's extends. Note that docs#uniform_space.completion uses "extend" for instance (and "map" when both the domain and codomain change).

[Kevin Buzzard]

So "extends" when there's an injection involved and "descends" when there's a surjection?

[Adam Topaz]

I should probably mention that the name projectivization.rep was as much of a practical choice as it was a name choice. The point is that projectivization K V is defined as quotient S where S is a setoid on {v // v \ne 0 }. So quotient.out' gives back an element of the subtype { v // v \ne 0 }, but I wanted to choose representatives in V directly. Defining projectivization.out or projectivization.out' was an issue because lean sometimes got confused with out to use (projectivization vs. quotient), and I wasn't prepared to make projectivization irreducible because I didn't completely copy over the quotient api (we probably don't want projectivization to be irreducible anyway).