9
$\begingroup$

In topology, the notion of "lifting" has a quite a long history, starting with the theory of covering spaces, where the classic example is that if you take an outdoor spiral staircase, $S$ and look at its shadow at noontime, you see a circle, $C$. "Casting a shadow" gives a map $p : S\to C$ with lots of nice properties, and we say that $S$ is a covering of $C$. $C$ is the base space, $S$ is the covering space, and $p$ is the projection.

A typical problem we consider is this: suppose we have a point $c \in C$ and a point $s \in S$ with $p(s) = c$. If we have a path in $C$ starting at $c$ (i.e., a function $u: [0, 1] \to C$ with $u(0) = c$), is there a path $\hat{u}$ in $S$ that "covers" $u$, i.e., a function $$ \hat{u}:[0, 1] \to S,\\ \hat{u}(0) = s \\ p(\hat{u}(t)) = u(t) \text{ for $0 \le t \le 1$ }. $$

In humbler terms, if Ann takes a walk on the circle starting at $c$, can Robin take a walk on the staircase starting at $s$ in such a way that Robin's shadow falls on Ann at all times?

The answer (at least in this example) is evidently "yes", and that's called the "path lifting theorem" --- the path $\hat{u}$ is a "lift" of the path $u$. That gets generalized to the homotopy lifting theorem, etc.

It's pretty clear that on $S$, there's an equivalence relation defined by $p$: points $s_1$ and $s_2$ are declared equivalent when $p(s_1) = p(s_2)$. Under this equivalence relation, the set $C$ is the quotient of $S$ by this relation.

So we have a set $S$, a relation $\sim$ on $S$, and a quotient $C = S/\sim$. A function $u$ to the set $C$ is said to "lift" to a function $\hat{u}$ to $S$.

This is exactly the opposite of the use of "lift" in both Lean and Isabelle, as far as I can tell. In those, we start with a function to $S$ and "lift" it to a function to $C$ (if certain conditions hold). A topologist would describe this second one by saying "we have a function going to $S$; is it the lift of a function to $C$?

There's a kind of "dual" notion: perhaps we have a function $f$ from $S$ to some space $X$. If $f(x) = f(y)$ whenever $p(x) = p(y)$, then topologists would say that $f$ "passes to (or even "projects to") a function on the quotient", while proof-assistant folks seem to say that $f$ lifts to a function on $C$.

Can anyone explain how this exactly-opposite notion of "lift" arose for proof-assistants? I know that lots of words in mathematics get used differently in different context, but I can't think of many instances where the meanings are exact opposites (except for some confusion over co-variant and contra-variant).

$\endgroup$

1 Answer 1

7
$\begingroup$

I totally agree that Lean's quotient.lift is disastrously-named as far as mathematicians are concerned. After discussion with the Lean devs it seems that it came about because to a computer scientist, quotienting out something by an equivalence relation is "making it more complex" (because as a type the quotient involves more stuff than the original type), whereas for mathematicians it's "making it smaller and hence simpler".

$\endgroup$
9
  • 3
    $\begingroup$ Today I learned that in mathematics the circle is simpler than the straight line. $\endgroup$ Feb 12, 2022 at 16:50
  • 2
    $\begingroup$ The circle is compact, the line is not. $\endgroup$ Feb 12, 2022 at 19:22
  • $\begingroup$ Thanks, Kevin. That makes some (unfortunate) sense. It's probably too late to go back and fix it, alas. $\endgroup$
    – John
    Feb 12, 2022 at 22:07
  • 1
    $\begingroup$ It's worth noting that in mathematics the term "lift" is part of 3 compatible conventions: "lift", "descent" (for more-or-less what Lean calls "lift"), and writing morphisms as a vertical arrow point downwards. $\endgroup$
    – Will Sawin
    Feb 13, 2022 at 13:27
  • 2
    $\begingroup$ @AndrejBauer Except in homotopy theory, the circle and the straight line are about equally complex - for example, they are each the unique isomorphism class of objects with their basic properties. A more clear-cut example might be hyperbolic manifolds, which really are much simpler than their universal covers. Almost every principle has exceptions! $\endgroup$
    – Will Sawin
    Feb 13, 2022 at 13:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.