En mathématiques, c’est une pratique très courante que d’identifier deux objets à isomorphisme près. Par exemple, les matrices sont des tableaux de n × m cases (i.e. des fonctions dont l’ensemble de départ est {1, …, n}×{1, …, m} et l’ensemble d’arrivée est un corps K) mais on les identifie à des applications1 linéaires de l’espace vectoriel Kn vers Km. La principale justification en est que le produit de matrices correspond à la composition d’applications linéaires. Et c’est très pratique en effet, mais comment justifie-t-on la chose rigoureusement ?

Qu’est-ce qu’un isomorphisme ?

La (courte) page Wikipédia traitant du sujet nous rappelle la définition usuelle :

Un isomorphisme entre deux ensembles structurés est une application bijective qui préserve la structure et dont la réciproque préserve aussi la structure.

En pratique, cette notion nous était généralement présentée en cours de mathématiques sur des exemples. Un isomorphisme de groupe par exemple est un morphisme bijectif (où dans ce cas précis morphisme signifie une application envoyant l’élément neutre sur l’élément neutre et le “produit” de deux éléments sur le “produit” de leurs images).

La notion admet une définition générale grâce à la notion sous-jacente de structure mathématique, c’est-à-dire un ensemble muni d’un certain nombre de relations et d’axiomes décrivant les propriétés de ces relations (cette notion s’apparente à celle de théorie). On dispose alors d’une structure concrète (ou modèle) lorsque l’on connait l’ensemble sous-jacent, l’on est capable de définir les relations et de démontrer les axiomes.

On peut voir le rapport avec le besoin d’abstraction en programmation. La notion de signature en OCaml (ou d’interface en Java) correspond à celle de structure et son implémentation en termes de modules (respectivement en classes) correspond à la concrétisation.

À quoi sert ce genre d’abstraction ?

L’un de l’intérêt de l’abstraction est de simplifier et généraliser les raisonnements. On voit aussi qu’il peut exister plusieurs modèles pour une même structure. On pourra ainsi démontrer un théorème portant sur les groupes, en toute généralité, i.e. en ne se servant que des axiomes. Quel est alors l’intérêt de transférer des théorèmes d’une structure concrète à l’autre (ce qui est une technique différente) ?

Parfois, on peut préférer une structure concrète à une autre car ses propriétés spécifiques rendent les raisonnements plus faciles. Pour reprendre l’exemple des matrices, il est drôlement plus facile de faire un produit de matrices plutôt que de composer “à la main” les applications linéaires correspondant. Les démonstrations de certains théorèmes se font donc non pas sur la base des axiomes uniquement mais sur la base des connaissances supplémentaires dont on dispose.

Deux ensembles ayant la même structure ne sont pas nécessairement isomorphes. Il existe par exemple toutes sortes de groupes : certains finis, d’autres infinis ; pour certains l’opération commute (groupe Abéliens), pour d’autres non. Montrer alors un théorème pour un de ces ensembles ne permet pas nécessairement de le transférer à tous les autres. On pourra le faire si on peut identifier les deux structures à l’aide d’un isomorphisme.

Le (la) mathématicien-ne va donc s’employer à chercher un isomorphisme. Lorsqu’il (elle) l’a trouvé et l’a démontré, il (elle) prend alors un air solennel et déclare “nous pouvons identifier les deux structures donc les théorèmes que nous avions démontré pour l’une sont valables pour l’autre”.

Qu’est-ce que ça veut dire ?

C’est la justification de cette déclaration qui m’intéresse ici car mon but est de pouvoir la donner à un ordinateur. Les ordinateurs n’apprécient guère les déclarations solennelles.

Wikipédia ne m’aidera pas dans ma quête. En effet, voici ce qu’on y lit :

Savoir que deux objets sont isomorphes présente un grand intérêt car cela permet de transposer des résultats et propriétés démontrés de l'un à l'autre.

Selon certains points de vue, deux objets isomorphes peuvent être considérés comme identiques, ou du moins indiscernables. En effet, bien souvent, les propriétés intéressantes d'un objet seront partagées par tous les objets isomorphes de la catégorie. Ainsi on parle souvent d'unicité ou d'identité « à isomorphisme près ».

Ce dont j’ai besoin c’est d’une sorte de théorème méta-mathématique, autrement dit logique qui exprime cela. Je pense qu’une expression approximative en serait : Si une formule logique dont les atomes ne font intervenir que les éléments - de manière abstraite - et les relations de la structure est vraie alors elle est aussi vraie pour toute structure isomorphe.

Je ne vous fournirai pas de démonstration de ce théorème car je l’ai exprimé de manière intuitive. Mais je serais curieux d’en lire une formulation et une démonstration rigoureuse (il y a sûrement des gens qui l’ont faite). Dans la suite, je vous montrerai une démonstration d’un cas particulier.

Les questions subséquentes sont alors de s’interroger sur la minimalité des hypothèses de ce théorème. A-t-on vraiment besoin d’un isomorphisme ? A-t-on besoin de la notion de “structure” ?

Nous n’avons pas toujours besoin d’isomorphisme.

Prenons deux ensembles E (respectivement E’) munis d’une relation R (respectivement R’).

Soit F(E, R, x1, …, xn) une formule du premier ordre positive2 dont les variables libres3 sont x1, …, xn ∈ E et les atomes sont de la forme R(y1, …, yk).

Supposons qu’on dispose d’une fonction f : E → E’

  • surjective : ∀ y ∈ E’, ∃ x ∈ E, f(x) = y
  • avec une propriété de transfert de R : ∀ x1, …, xk ∈ E, R(x1, …, xk) → R’(f(x1), …, f(xk))

Alors si F(E, R, x1, …, xn) est vraie, F(E’, R’, f(x1), …, f(xn)) aussi.

Le cas particulier où il n’y a pas de variable libre nous montre que tout théorème positif du premier ordre ne portant que sur R se transfère de E à E’.

Effectuons la démonstration par récurrence structurelle sur F :

Cas F = ∀ x ∈ E, F’(E, R, x1, …, xn, x)

Soit x ∈ E’, d’après la surjectivité de f, on peut trouver x’ ∈ E tel que x = f(x’). Alors on applique F à x’ pour obtenir F(E, R, x1, …, xn, x’).

Du coup, par hypothèse de récurrence, F(E’, R’, f(x1), …, f(xn), f(x’)) est vraie, i.e. F(E’, R’, f(x1), …, f(xn), x) est vraie.

Ainsi on conclut que ∀ x ∈ E’, F’(E’, R’, f(x1), …, f(xn), x).

Cas F = ∃ x ∈ E, F’(E, R, x1, …, xn, x)

Soit un témoin x rendant la formule F’(E, R, x1, …, xn, x) vraie. Alors par hypothèse de récurrence, F’(E, R, f(x1), …, f(xn), f(x)). D’où f(x) est un témoin rendant la formule ∃ x ∈ E’, F’(E’, R’, f(x1), …, f(xn), x) vraie.

Cas F = F’(E, R, x1, …, xn) ∨ F’‘(E, R, x1, …, xn)

L’une au moins de ces deux sous-formules F’ et F’’ est vraie. Supposons par exemple que ce soit F’. Alors par hypothèse de récurrence, F’(E’, R’, f(x1), …, f(xn)) est vraie ce qui suffit à conclure que F’(E’, R’, f(x1), …, f(xn)) ∨ F’‘(E’, R’, f(x1), …, f(xn)) est vraie aussi.

Le cas avec ∧ est similaire.

Cas de base F = R(y1, …, yk)

C’est là qu’on utilise la seconde propriété de f et c’est alors immédiat.

QED

On peut généraliser facilement à des formules comportant aussi des négations ¬ et des implications → à condition :

  1. Qu’aucun quantificateur n’apparaisse sous ces deux connecteurs logiques ;
  2. Qu’on renforçe un petit peu la seconde hypothèse sur f : ∀ x1, …, xk ∈ E, R(x1, …, xk) ↔ R’(f(x1), …, f(xk)).

Pour le voir il faudra renforcer l’hypothèse de récurrence sur toutes les sous-formules sans quantificateurs, dans l’esprit avec lequel on a renforcé l’hypothèse sur f.

En revanche, nous avons besoin d’un isomorphisme pour considérer les théorèmes quelconques du premier ordre mixant allègrement les quantificateurs et les négations.

Nous avons besoin d’un isomorphisme si nous rajoutons l’égalité

Plus précisément, dès lors que nous autorisons les formules atomiques à être des égalités x = y et pas seulement des relations R(y1,…,yk), alors on peut exprimer la taille de l’ensemble pour tout ensemble fini. Une bijection est alors nécessaire pour qu’une telle propriété se transmette (une surjection entre deux ensembles finis de même taille est une bijection).

Nous n’avons pas besoin des axiomes de la structure

Il est bien connu qu’un morphisme de monoïde transfère les propriétés de groupe et de groupe Abélien. La raison est la même que pour tous les autres théorèmes que nous pouvons vouloir transférer. Par conséquent, tous ces axiomes structurels sont superflus : si on peut transférer les relations, on peut transférer les axiomes.

Que se passe-t-il lorsque nous avons des éléments distingués et des opérations ?

Des opérations (i.e. des applications à plusieurs arguments, à valeurs de départ et d’arrivée dans la structure) peuvent être représentées par des relations bien particulières.

De même, des éléments distingués (comme l’élément neutre d’un groupe) peuvent n’être distingués que par une relation spéciale à un seul argument, toujours fausse, sauf pour l’élément concerné.

Cependant, il pourra être utile, en encodant cela, de traiter les opérations et les éléments distingués de manière spécifique, notamment pour des raisons d’efficacité et d’utilisabilité.

Conclusion

J’ai essayé de faire une présentation assez pédagogique, au moins pour le début. En revanche, elle est aussi assez naïve, comme je ne suis pas spécialiste du sujet, alors que les questions soulevées m’intéressent vraiment pour mon travail. Je serais donc ravi d’avoir des retours de mes amis mathématiciens ou catégoriciens (ce mot n’existe pas, j’en ai conscience).

Si vous voulez en savoir plus, lisez l’article que j’ai écrit sur le sujet depuis [en anglais].

  1. Dans tout cet article, on emploiera le terme d’application qui est synonyme de fonction (totale). ↩

  2. Dans une formule du premier ordre positive, on peut avoir des connecteurs logiques comme la conjonction ∧ et la disjonction ∨, des quantificateurs ∀ et ∃ mais toutes les variables quantifiées le sont dans E et on ne peut pas avoir de connecteurs comme la négation ¬ et l’implication →. ↩

  3. Les variables libres sont celles sur lesquelles il n’y a pas de quantification dans la formule. ↩