## Stream: new members

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

#### Ken Lee (Jun 18 2020 at 16:48):

In maths, we are often given a surjection $\pi : \alpha \to \beta$ and $f : \alpha \to \gamma$ which preserves preimages of elements in $\beta$ and want to lift $f$ to a map $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 : α → γ} (hπ : function.surjective π)
(hf : ∀ x y : α, π x = π y → f x = f y) :
∃ g : β → γ, g ∘ π = f := ⟨
λ b : β, f $classical.some (hπ b), funext$ λ a : α,
hf (classical.some (hπ (π a))) a \$ classical.some_spec (hπ (π 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"?

#### Johan Commelin (Jun 18 2020 at 16:50):

definition and theorem are treated differently here, I think.

#### Bhavik Mehta (Jun 18 2020 at 16:50):

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

#### Johan Commelin (Jun 18 2020 at 16:50):

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

#### Bryan Gin-ge Chen (Jun 18 2020 at 16:52):

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

#### 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

#### Johan Commelin (Jun 18 2020 at 16:53):

Oops, sorry Bhavik...

No worries!

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

#### Reid Barton (Jun 18 2020 at 16:58):

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

#### Reid Barton (Jun 18 2020 at 17:06):

If you replace the existential quantifier in hπ 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.

#### 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