What does it mean to "use Choice"?

Stream: new members

[Ken Lee]

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]

definition and theorem are treated differently here, I think.

[Bhavik Mehta]

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

[Johan Commelin]

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

[Bryan Gin-ge Chen]

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

[Bhavik Mehta]

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

Oops, sorry Bhavik...

[Bhavik Mehta]

No worries!

[Ken Lee]

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]

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

[Reid Barton]

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]

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