I don't want your opinion, I want just the mathematical truth

The function
[math] f: \{ 0,1,2,3 \} \to \{6,7\} [/math]
defined by
[math] f(0):=6 [/math]
[math] f(1):=6 [/math]
[math] f(2):=7 [/math]
[math] f(3):=6 [/math]
is surjective: Its range (the set of values, 6 and 7) indeed equals its codomain ([math] \{6,7\} [/math]).

The function has a right inverse
[math] r: \{6,7\} \to \{ 0,1,2,3 \} [/math]
For example,
[math] r(6):=3 [/math]
[math] r(7):=2 [/math]
makes it so that [math]f \circ r[/math] is the identity function on [math] \{6,7\} [/math]:
[math]f(r(6))=f(3)=6[/math]
[math]f(r(7))=f(2)=7[/math]
It's easy to write down some right inverse if the sets involved are finite.

But does every surjective function have a right inverse?

Other urls found in this thread:

proofwiki.org/wiki/Surjection_iff_Right_Inverse
en.wikipedia.org/wiki/Axiom_of_choice
en.wikipedia.org/wiki/Brouwer–Hilbert_controversy#Origins_of_disagreement
twitter.com/SFWRedditImages

>does every surjective function have a right inverse
Yes, this is the definition of surjectivity.

proofwiki.org/wiki/Surjection_iff_Right_Inverse

That proof uses the axiom of choice.
So I take it you say the axiom of choice is true?

You shouldn't need AC if you're not working with infinite functions, no?

Consider suicide

Wow, you bothered to write all of that down before you bothered to think? Try better next time.

is this bait
how does it have an inverse
if r(6)=3 and r(7)=2 what about [eqn]f^{-1}(0)[/eqn]

Infinite functions? The axiom of choice is only needed in this case when it is not clear how to pick an element of the preimages to form the inverse.

I read Camus.

Think to reach which conclusion?

Right inverse:
For the surjection
[math]f: D \to C [/math]
this is a function
[math]r: C \to D [/math]
so that [math]f \circ r[/math] equals the identify on the [math] C [/math].
Here [math] C [/math] may be smaller than [math] D [/math], as in the example.

Nope.

From wikipedia:
>Informally put, the axiom of choice says that given any collection of bins, each containing at least one object, it is possible to make a selection of exactly one object from each bin. In many cases such a selection can be made without invoking the axiom of choice; this is in particular the case if the number of bins is finite.


en.wikipedia.org/wiki/Axiom_of_choice

you're not working with infinite functions (I assume you mean infinite domain or codomain by this), but to prove things about all functions, as OP is trying to do, you are essentially talking about an infinite number of functions, including ones with domains you can't easily choose elements from to form a right inverse. Thus, you need AC to prove that every surjective function has a right inverse.

By the way, this comes up all the time in category theory when you try to factorize an arrow through an equalizer. In the category of sets, this coincides with OP's statement.

If we axiomize that every surjective function has a right inverse, can we prove the axiom of choice?
(If we axiomize that every surjective function has a right inverse, can we prove Banach Tarski?)

If you take that as an axiom, it is equivalent to AC, as are a lot of statements of this type.
So yeah, you could prove Banach-Tarski.

The berger says there are not an infinite number of functions.

>finitism

>accept constructivism
>strong intuitionistic reading of existential quantifer yields a right inverse from the statement of surjectivity
why on earth would someone EVER accept classical logic but then reject AC? It's like getting the worst of both worlds, and there's no good philosophical justification
>"b-but I want to be able to construct my mathematical objects...some of the time"

>>strong intuitionistic reading of existential quantifer yields a right inverse from the statement of surjectivity
Could you elaborate?

So are you on the side of "choose the framework you feel like" or do you have constructionist convictions (in the intuistionstic logic sense)?

Why does the cat look so sad?

According to the BHK interpretation, a proof of

[math]\forall x\in A \varphi(x)[/math]

is a "function" that takes as input an element [math]a \in A[/math]
and outputs a proof of [math]\varphi(a)[/math]; and a proof of

[math]\exists x\in A \varphi(x)[/math]

is a pair consisting of an element [math]a \in A [/math] and a proof of [math]\varphi(a)[/math].

Thus, a proof or statement of [math]\forall y\in B\exists x \in A f(x) = y[/math] is read in this interpretation as a function accepting inputs [math]b \in B[/math] and outputs pairs [math]\langle a,P\rangle[/math] where [math]P[/math] is a proof of [math]f(a)=b[/math].
If we throw out the second component this gives us a function [math]g : B \rightarrow A[/math]. Furthur, we can use those [math]P[/math]'s to prove that [math]g[/math] is a right inverse.

I believe that in this manner, the statement that every surjection has a right inverse is provable in most type theories. Things get a bit hairier in constructive set theories, but I don't know much about that.

Both I guess. I like constructive mathematics because you can immediately see applications to the real world and the ontology is a bit more coherent. However, I think convincing mathematicians to give up classical logic is a bit of a fool's errand. And anyway, most mathematician's proofs end up being constructive anyway, or can be easily modified to yield constructive content

Yeah, I know that 'an' axiom of choice is provable in Per Martin Löf's type theory
(that theories notion of "set" is of course not as permissive as the ones written down in first-order logic)

"easy", depending on how explicit you want it.
I don't know but it might be that the algorithmic part of even new modern proves is not particular special. It often might come down to ideas found to be effective at the right place.

People who cry about AC are retarded psuedophilosophers who aren't bright enough to actually produce something definitive and modern so they have make problems out of previously insignificant things. They then create a proof without AC and expect to receive praise for solving a problem they themselves created and nobody gave a fuck about to begin with.

It's like blowing up a building in the middle of fucking nowhere then rebuilding it again and then expecting to receive an award for beautiful architecture the second time around.

the non-constructive aspects of the logical formalization of math were criticized right away. The whol shebang is no 150 years old.

en.wikipedia.org/wiki/Brouwer–Hilbert_controversy#Origins_of_disagreement

>If it's in one thing it's also in da other thing

Wow it's fucking nothing. Can we stop trying to reinvent the definition of functions and get on with it?

bump

bump for what, bre?

...

In a locally-small category, arrows which are epic are not necessarily a surjection, while monics may not be an injection.

this proves that m is monic, yet not injective.

funfact on the side?

It's not like epics are a very setty notion (they shouldn't be primarily thought of as functions to begin with)