De auteur beschrijft een ervaring tijdens het formaliseren van het leerboek Abstract Algebra van Dummit and Foote in de proof assistant Rocq. Hierbij stuit de auteur op een onjuiste stelling in de eerste bewijsoefening: de bewering dat een functie injectief is dan en slechts dan als deze een links-inverse heeft.
Door de strikte eisen van Rocq wordt een specifiek randgeval zichtbaar: wanneer de domeinverzameling $A$ leeg is en de codomeinverzameling $B$ niet. In dit scenario is de functie weliswaar vacuüm injectief, maar kan er geen links-inverse bestaan omdat er simpelweg geen functies mogelijk zijn van $B$ naar $A$. De auteur merkt op dat deze fout waarschijnlijk over het hoofd zou zijn gezien bij een handmatige uitwerking, en dat de fout inmiddels is opgenomen in de officiële errata van het boek.
Een fout ontdekt in 'Abstract Algebra' van Dummit and Foote
Ik had veel moeite met de eerste bewijsoefening in het boek, omdat het gestelde doel van het bewijs niet waar is. Dit was zowel frustrerend als spannend om uit te zoeken :)
Definities
Functie Een functie $f$ van een verzameling $A$ naar een verzameling $B$ (geschreven als $f: A \to B$) is een verzameling paren zodan dat:
- Het eerste item in elk paar afkomstig is uit $A$.
- Het tweede item in elk paar afkomstig is uit $B$.
- Voor elk element van $A$ geldt dat dit het eerste item is in precies één van de paren.
In andere woorden, voor de programmeurs onder jullie: een functie wordt gedefinieerd door de verzameling van al zijn input-output paren en moet deterministisch zijn.
Injectiviteit Een functie is injectief als geen twee verschillende inputs naar dezelfde output mappen.
- Voorbeeld: $f: \text{int} \to \text{int}$ door $f(x) = x^2$ is niet injectief, omdat $f(1) = f(-1)$.
Links-inverse Een functie $f: A \to B$ heeft een links-inverse als er een functie $g: B \to A$ bestaat zodan dat voor alle $a$ in $A$ geldt dat $g(f(a)) = a$. In andere woorden: de links-inverse van $f$ "maakt $f$ ongedaan".
Propositie 1 (1)
De eerste bewijsoefening in het boek is om aan te tonen dat een functie injectief is dan en slechts dan als deze een links-inverse heeft.
Deze stelling is onjuist. Stel dat $A = \emptyset$ en $B = \{1\}$. Laat $f: A \to B = \emptyset$.
- De functie $f$ is inderdaad een functie, omdat deze voldoet aan de drie criteria uit de bovenstaande definitie.
- De functie $f$ is injectief, omdat het (vacuüm) waar is dat geen twee verschillende inputs naar dezelfde output mappen.
- Echter heeft $f$ geen links-inverse, omdat er geen functies bestaan van $B$ naar $A$.
Ik had waarschijnlijk niet aan dit randgeval gedacht als ik deze oefening op papier had gemaakt. Omdat ik Rocq gebruikte, liep ik constant tegen muren op bij het proberen te bewijzen van de propositie zoals deze gesteld was. Alle manieren waarop ik me kon voorstellen de stelling te bewijzen, vereisten ofwel dat $A$ bevolkt (inhabited) was, of dat $B$ onbewoond (uninhabited) was.
Na veel te lange tijd begon ik me af te vragen of de propositie überhaupt wel waar was, en hier zijn we dan :)
Tijdens het schrijven van dit bericht heb ik de errata van het boek gecontroleerd, en dit staat er al in. Tja :)
Een fout ontdekt in 'Abstract Algebra' van Dummit and Foote
Ik had veel moeite met de eerste bewijsoefening in het boek, omdat het gestelde doel van het bewijs niet waar is. Dit was zowel frustrerend als spannend om uit te zoeken :)
Definities
Functie Een functie $f$ van een verzameling $A$ naar een verzameling $B$ (geschreven als $f: A \to B$) is een verzameling paren zodan dat:
- Het eerste item in elk paar afkomstig is uit $A$.
- Het tweede item in elk paar afkomstig is uit $B$.
- Voor elk element van $A$ geldt dat dit het eerste item is in precies één van de paren.
In andere woorden, voor de programmeurs onder jullie: een functie wordt gedefinieerd door de verzameling van al zijn input-output paren en moet deterministisch zijn.
Injectiviteit Een functie is injectief als geen twee verschillende inputs naar dezelfde output mappen.
- Voorbeeld: $f: \text{int} \to \text{int}$ door $f(x) = x^2$ is niet injectief, omdat $f(1) = f(-1)$.
Links-inverse Een functie $f: A \to B$ heeft een links-inverse als er een functie $g: B \to A$ bestaat zodan dat voor alle $a$ in $A$ geldt dat $g(f(a)) = a$. In andere woorden: de links-inverse van $f$ "maakt $f$ ongedaan".
Propositie 1 (1)
De eerste bewijsoefening in het boek is om aan te tonen dat een functie injectief is dan en slechts dan als deze een links-inverse heeft.
Deze stelling is onjuist. Stel dat $A = \emptyset$ en $B = \{1\}$. Laat $f: A \to B = \emptyset$.
- De functie $f$ is inderdaad een functie, omdat deze voldoet aan de drie criteria uit de bovenstaande definitie.
- De functie $f$ is injectief, omdat het (vacuüm) waar is dat geen twee verschillende inputs naar dezelfde output mappen.
- Echter heeft $f$ geen links-inverse, omdat er geen functies bestaan van $B$ naar $A$.
Ik had waarschijnlijk niet aan dit randgeval gedacht als ik deze oefening op papier had gemaakt. Omdat ik Rocq gebruikte, liep ik constant tegen muren op bij het proberen te bewijzen van de propositie zoals deze gesteld was. Alle manieren waarop ik me kon voorstellen de stelling te bewijzen, vereisten ofwel dat $A$ bevolkt (inhabited) was, of dat $B$ onbewoond (uninhabited) was.
Na veel te lange tijd begon ik me af te vragen of de propositie überhaupt wel waar was, en hier zijn we dan :)
Tijdens het schrijven van dit bericht heb ik de errata van het boek gecontroleerd, en dit staat er al in. Tja :)
Groetjes,