# Zulip Chat Archive

## Stream: general

### Topic: quotient.out

#### Johan Commelin (Mar 07 2022 at 08:59):

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 (Mar 07 2022 at 09:03):

And how about renaming `quotient.lift`

to `quotient.descent`

while we're at it?

#### Johan Commelin (Mar 07 2022 at 09:08):

I would be happy with `desc`

instead of `descent`

(-; But yes!

#### Eric Wieser (Mar 07 2022 at 09:25):

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 (Mar 07 2022 at 09:32):

That's another argument for renaming `lift`

to `desc`

.

#### Johan Commelin (Mar 07 2022 at 09:33):

`src/data/quot.lean`

doesn't mention anything like "descends to the quotient" in the entire file.

#### Eric Wieser (Mar 07 2022 at 09:36):

What's the heuristic for which other `lift`

s should be called `desc`

?

#### Eric Wieser (Mar 07 2022 at 09:37):

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

#### Johan Commelin (Mar 07 2022 at 09:40):

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 (Mar 07 2022 at 09:41):

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 (Mar 07 2022 at 09:45):

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

#### Eric Wieser (Mar 07 2022 at 09:47):

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

#### Johan Commelin (Mar 07 2022 at 09:48):

Sure, a tonne of things in mathlib are called `lift`

, because they all copy `quot.lift`

.

#### Eric Wieser (Mar 07 2022 at 09:48):

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

"

#### Eric Wieser (Mar 07 2022 at 09:49):

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 (Mar 07 2022 at 10:19):

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

#### Kevin Buzzard (Mar 07 2022 at 10:19):

Quotients are an example

#### Riccardo Brasca (Mar 07 2022 at 10:22):

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 (Mar 07 2022 at 10:27):

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 (Mar 07 2022 at 10:29):

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 (Mar 07 2022 at 10:31):

"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 (Mar 07 2022 at 10:44):

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 (Mar 07 2022 at 10:44):

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 (Mar 07 2022 at 10:47):

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 (Mar 07 2022 at 10:48):

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

#### Johan Commelin (Mar 07 2022 at 10:48):

But a map can also factor through a quotient.

#### Riccardo Brasca (Mar 07 2022 at 11:03):

"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 (Mar 07 2022 at 12:32):

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 (Mar 07 2022 at 14:09):

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

#### Adam Topaz (Mar 07 2022 at 14:52):

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).

Last updated: Dec 20 2023 at 11:08 UTC