Left inverse to injection

Stream: maths

[Roselyn Baxter]

Hello, I'd like some tips for how to implement something. So given an injection f : α → β with α nonempty, classically one would not need the axiom of choice to prove that it has a retraction, i.e. a left inverse. This is because for any y : β that is in the image of f, we can map it onto its unique inverse image, and if y is not in the image we can just map it onto a witness of α being nonempty. This clearly relies on excluded middle, because it is not in general decidable wether y will be in the image of f, but to my mind it should not rely on the axiom of choice. How would I go about implementing this in Lean? I cannot produce data from the assertion that ∃ x, f x = y, but can I produce data from unique existence?

[Anne Baanen]

I'm pretty sure you need some classical axiom to produce data from docs#exists_unique.

[Anne Baanen]

If you want to find a retrect for an injective function, you can combine docs#function.injective.has_left_inverse and docs#Exists.some, so something like (untested):

noncomputable def retract (f : α → β) [nonempty α] (hf : function.injective f) : β → α :=
hf.has_left_inverse.some

[Anne Baanen]

Note that in dependent type theory, there are many formulations of choice principles, and some of the original set-theoretical formulations choice principles such as docs#classical.axiom_of_choice or docs#set.pi_nonempty_iff follow from double negation elimination (more specifically, from docs#classical.choice), while others are trivially true: if we translate "for all x, there is a y such that P(x, y)" to h : Π x, Σ y, P x y, then this obviously has a choice function, namely λ x, sigma.fst (h x).

[Eric Wieser]

There is docs#fintype.choose for constructively extracting data from exists_unique via enumeration

[Anne Baanen]

I suppose it would work for all enumerable types α and decidable predicates α → Prop, right?

[Anne Baanen]

Indeed: docs#encodable.choose

[Eric Rodriguez]

yeah, I was going to point out docs#nat.find, docs#enat.find, (docs#int.find ?) but that seems like the better general version

[Reid Barton]

There are three other "axioms" that are derived from choice in Lean:

• docs#classical.em
• unique choice
• docs#classical.axiom_of_choice

If you want to minimize axioms then you should pose them all as axioms separately.

[Reid Barton]

For the original question, you would need to use the first two.

[Roselyn Baxter]

Ah, I hadn't realised classical.em was proved from classical.choice, I see. I won't be able to use much of anything in mathlib then, oh well.

[Reid Barton]

Since em and axiom_of_choice are propositions, I would guess you could get pretty far by modifying the Lean core library to replace them by axioms.

[Reid Barton]

But indeed, mathlib is very much not designed for this kind of thing.