lift (terminology)

Stream: mathlib4

[Yoh Tanimoto]

In SeparationQuotient.lift, for (f : X → α) (hf : ∀ (x y : X), Inseparable x y → f x = f y) p.liftQ f h is defined as a map such that lift f hf(mk x) = f x, but is this the standard terminology? It feels rather that the RHS is the lift of the LHS.
cf. https://en.wikipedia.org/wiki/Lift_(mathematics)

[Christian Merten]

This naming comes from the naming of docs#Quotient.lift. Arguably it should be called Quotient.desc and this is how it is called in the category theory limits API, see e.g. docs#CategoryTheory.Limits.colimit.desc

[Patrick Massot]

We discuss this periodically, and have been discussing it at least since 2017. The current terminology is definitely backward compared to mathematics but it is very much entrenched, including in Lean core.

[Yoh Tanimoto]

in other words, it is difficult change, I see.

[Notification Bot]

Yoh Tanimoto has marked this topic as resolved.

[Kim Morrison]

I don't think it is impossible for Mathlib to change unilaterally however.

[Patrick Massot]

Kim Morrison said:

I don't think it is impossible for Mathlib to change unilaterally however.

Isn’t this terminology introduced in core?

[Kim Morrison]

Yes, but Mathlib could choose to not name further things lift.

[Kim Morrison]

(My take here is that lift is just wrong, and mathematicians have the right words here that unfortunately got scrambled.)

[Kim Morrison]

That said, I don't want to make a case for renaming it in Lean; I'm just proposing moving where the seam occurs.

[Notification Bot]

Yoh Tanimoto has marked this topic as unresolved.

[Yoh Tanimoto]

(deleted)

[Yoh Tanimoto]

I coud start by renaming lift by Inseparable setoid, indeed I have some related PR #18178. What is the mathematically right terminology? desc, or maybe factor?

[Notification Bot]

Yoh Tanimoto has marked this topic as unresolved.