Ao formalizar a Álgebra Abstrata de Dummit e Foote em Rocq durante minha segunda semana no Recurse Center, descobri que o objetivo do primeiro exercício de prova era falso. A proposição afirma que uma função é injetora se e somente se tem inversa à esquerda. Mas existe um contra-exemplo: seja A vazio e B = {1}.

A função vazia f: A -> B é injetora vacuamente, porém nenhuma função g: B -> A existe porque B é não vazio e A é vazio. Esse caso extremo é fácil de passar despercebido no papel, mas Rocq me forçou a enfrentá-lo. Depois de lutar, consultei a errata do livro e a encontrei listada.

Foi frustrante, mas emocionante descobrir independentemente.