# Zulip Chat Archive

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

- I have used
`classical.some`

in the proof, so does this count as having "used choice" as we say it in maths? - 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?
- 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):

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

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

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

No worries!

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

Bhavik Mehta said:

- 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