Finding a bug in Dummit and Foote's Abstract Algebra

Ben Kallus discovered a bug in Dummit and Foote's "Abstract Algebra" textbook while formalizing a proof in Rocq: the first proof exercise claims that a function is injective if and only if it has a left inverse, but this is false when the domain is empty and the codomain is non-empty. The counterexample shows that an empty function from an empty set to a non-empty set is injective but has no left inverse, since no function can exist from the non-empty codomain back to the empty domain.