En formalisant l'algèbre abstraite de Dummit et Foote dans Rocq durant ma deuxième semaine au Recurse Center, j'ai découvert que l'objectif du premier exercice de preuve était faux. La proposition affirme qu'une fonction est injective si et seulement si elle a un inverse à gauche. Mais un contre-exemple existe : soit A vide et B = {1}.

La fonction vide f: A -> B est injective de manière vacante, pourtant aucune fonction g: B -> A n'existe car B est non vide et A est vide. Ce cas limite est facile à manquer sur papier, mais Rocq m'a forcé à y faire face. Après avoir lutté, j'ai consulté l'errata du livre et je l'ai trouvé listé.

C'était frustrant mais excitant de le découvrir indépendamment.