Zulip Chat Archive

Stream: new members

Topic: What does it mean to "use Choice"?


view this post on Zulip Ken Lee (Jun 18 2020 at 16:48):

In maths, we are often given a surjection π:αβ\pi : \alpha \to \beta and f:αγf : \alpha \to \gamma which preserves preimages of elements in β\beta and want to lift ff to a map g:βγg : \beta \to \gamma. I've written what I believe is a faithful representation of the "mathematical argument" in Lean :

universes u v w
theorem quotient_exists_lift {α : Sort u} {β : Sort v} {γ : Sort w}
{π : α  β} {f : α  γ} ( : function.surjective π)
(hf :  x y : α, π x = π y  f x = f y) :
 g : β  γ, g  π = f := 
  λ b : β, f $ classical.some ( b),
  funext $ λ a : α,
  hf (classical.some ( (π a))) a $ classical.some_spec ( (π a))

My questions are :

  1. I have used classical.some in the proof, so does this count as having "used choice" as we say it in maths?
  2. The second part of the constructor corresponds in the "mathematical argument" to checking the function is well-defined and "independent of choice of representative". Does this mean I have "not used choice" or is this just a coincidence in the language?
  3. I understand that using classical.choice or any of its corollaries means I have to mark my theorems noncomputable. Is the reverse true and how is this related to when we have "used choice" in maths? In particular, since Lean did not complain that the above theorem is noncomputable, does it mean I have "not used choice"?

view this post on Zulip Johan Commelin (Jun 18 2020 at 16:50):

definition and theorem are treated differently here, I think.

view this post on Zulip Bhavik Mehta (Jun 18 2020 at 16:50):

  1. Yes. You can do #print axioms quotient_exists_lift to see

view this post on Zulip Johan Commelin (Jun 18 2020 at 16:50):

If you #print axioms quotient_exists_lift -- nvm Bryan Bhavik's faster

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

So fast that I got @Bhavik Mehta to post in my stead!

view this post on Zulip Bhavik Mehta (Jun 18 2020 at 16:52):

  1. The second part of the constructor corresponds to showing that you've got an actual lift of f, rather than just any function beta -> gamma

view this post on Zulip Johan Commelin (Jun 18 2020 at 16:53):

Oops, sorry Bhavik...

view this post on Zulip Bhavik Mehta (Jun 18 2020 at 16:54):

No worries!

view this post on Zulip Ken Lee (Jun 18 2020 at 16:57):

Bhavik Mehta said:

  1. Yes. You can do #print axioms quotient_exists_lift to see

I know that I have used classical.choice. What I meant to ask was whether this is exactly what we mean by "using choice" in maths. Sorry I should've worded this better.

view this post on Zulip Reid Barton (Jun 18 2020 at 16:58):

It depends on your exact foundational setup and interpretation of Prop, quantifiers etc.

view this post on Zulip Reid Barton (Jun 18 2020 at 17:06):

If you replace the existential quantifier in and the conclusion by trunc, then you can prove this without axioms. But in classical foundations you can't distinguish between existential quantification and trunc.

view this post on Zulip Reid Barton (Jun 18 2020 at 17:07):

("without axioms" = maybe still using stuff like funext)


Last updated: May 15 2021 at 02:11 UTC