But f's codomain is B, and g isn't a function on B, so you can't compose them in the first place. And saying "well yeah but you could compose f's restriction" is exactly making f surjective.

The basic result here is every function factors as a surjection (collapsing to the quotient) followed by an isomorphism (with the image) followed by an injection (enlarging the codomain). The surjection and injection are "trivial" and the isomorphism is the part that "does something" (permuting your thing somehow).

▲

troethe 5 hours ago | parent [-]

Of course I can compose `f: A -> B` and `g: f(A) -> A`. The composition maps a `x` from `A` to `g(f(x))` which is well defined. Therefore the composition is a function.

`g` and `f` aren't functions in a programming language and `A` and `B` are not types. There is nothing like a type checker forbidding you from composing `f: A -> B` and `g: f(A) -> A`.

▲

ndriscoll 5 hours ago | parent [-]

I suppose, but then your definition of composition requires checking compatibility of codomain/domain instead of it being automatic (and your definition of composition does not fit the shape to form a category), which seems way worse than stipulating f non-empty for some theorem that isn't even true for other categories either.

And for e.g. for vector spaces or modules over semisimple rings they're actually the same so there's a real statement being made to say they're not always.

	▲	troethe 4 hours ago \| parent [-]
		I think we can sit here and speculate which properties of left inverses are actually important for quite a while. But we will only ever get a real answer to this question, when the original poster finishes formalizing the whole book and can tell us which weakenings break further proofs in the books and which won't.