Relations d'équivalence et quotients

Dans ce chapitre, nous abordons l'étude du processus de passage au quotient. Il s'agit d'un procédé mathématique très puissant pour trier l'information, dans le but d'éliminer de l'information redondante ou pour mettre en valeur l'information pertinente dans une situation donnée. Bien que ce sujet soit moins fondamental que l'étude des connecteurs logiques et quantificateurs, il reste très proche des fondements, et prend de plus en plus d'importance au fur et à mesure des études de mathématiques. Ce cours est donc une initiation à un sujet plus avancé, qu'il est naturel de trouver plus difficile que les cours précédents.

L'exemple qui donne son nom au procédé, et qui servira de fil rouge, est celui de la construction des nombres rationnels. Un nombre rationnel est déterminé par une fraction : une paire d'entiers relatifs, le second étant strictement positif. Mais chaque nombre rationnel est représenté par une infinité de fractions, il y a donc une redondance à éliminer pour passer des fractions aux nombres rationnels.

On commence par rappeler la notions de relation d'équivalence.

Définition

Une relation sur un ensemble $X$ est un prédicat $R$ portant sur deux éléments de $X$. On note le plus souvent $xRx'$ l'énoncé $R(x, x')$. On dit que $R$ est une relation d'équivalence si elle vérifie les conditions suivantes :

  • (réflexivité) : $∀ x, xRx$
  • (symétrie) : $∀ x\, y, xRy ⇔ yRx$
  • (transitivité) : $∀ x\, y\, z, xRy \text{ et } yRz ⇒ xRz$.

Lorsque la relation est facile à déduire du contexte, on dit simplement que $x$ et $y$ sont équivalents si $xRy$. La notation $R$ n'est généralement utilisée que pour discuter des définitions. En pratique on utilise soit une notation spécialisée, telle que $x ≡ y \; [n]$ pour la relation de congruence modulo $n$, ou bien les notations plus génériques $x ∼ y$ ou $x ≈ y$. Cette dernière notation est aussi utilisée par les physiciens pour signifier « $x$ est à peu près égal à $y$ » ou, plus précisément, « pour toutes choses utiles, on pourra considérer $x$ comme étant égal à $y$ ». Cette dernière formulation est très proche du but poursuivi dans ce chapitre. Nous allons voir comment, étant donné une relation d'équivalence sur un ensemble $X$, on peut former un nouvel ensemble où les éléments équivalents de $X$ ne sont plus discernables.

Avant cela, vérifions que la relation assurant que deux fractions définissent le même nombre rationnel est une relation d'équivalence. Ici $X = ℤ × ℕ^*$, l'ensemble des fractions, qui sont simplement des paires $(p, q)$ où $p$ est un entier relatif et $q$ un entier strictement positif. La relation d'équivalence pertinente doit mettre en relation les paires définissant le même nombre rationnel. Bien sûr cette relation ne peut pas être définie en termes de nombres rationnels, et encore moins en termes de nombres réels, sinon la construction tourne en rond. On ne peut donc pas définir cette relation par $(p, q) ∼ (p', q')$ si $p/q = p'/q'$, qui présuppose construit l'ensemble des nombres rationnels. On définit plutôt $(p, q) ∼ (p', q')$ par la condition $pq' = p'q$. On vérifie immédiatement que cette relation est réflexive et symétrique. La transitivité demande un petit peu de réflexion. Soit $(p, q)$, $(p', q')$ et $(p'', q'')$ trois fractions telles que $(p, q) ∼ (p', q')$ et $(p', q') ∼ (p'', q'')$. Montrons que $(p, q) ∼ (p'', q'')$. Par hypothèse $pq' = p'q$ et $p'q'' = p''q'$. En multipliant la première égalité par $q''$ et en réécrivant à l'aide de la deuxième, on obtient $pq'q'' = p''q'q$. Or $q'$ est non-nul donc on peut diviser cette égalité par $q'$ pour obtenir $pq'' = p''q$, c'est à dire $(p, q) ∼ (p'', q'')$.

Il est important que tout nombre rationnel s'écrive comme fraction et que deux fractions définissent le même nombre rationnel si et seulement si elles sont équivalentes. Le théorème suivant affirme qu'une telle construction est possible en partant de n'importe quel ensemble et n'importe quelle relation d'équivalence. En première lecture il peut être utile de remplacer $X$ par l'ensemble $ℤ × ℕ^*$ des fractions, $X/{∼}$ par l'ensemble $ℚ$ des nombres rationnels et $π$ par $(p, q) ↦ \frac{p}q$.

Théorème

Soit $X$ un ensemble muni d'une relation d'équivalence $∼$. Il existe un ensemble, appelé quotient de $X$ par $∼$ et noté $X/{∼}$ et une fonction $π : X → X/{∼}$ appelée projection de $X$ sur $X/{∼}$ tels que :

  • tout $X/{∼}$ provient de $X$, c'est à dire que $π$ est surjective : $∀ q ∈ X/{∼}, ∃ x ∈ X, π(x) = q$
  • la projection identifie exactement les points équivalents de $X$ : $∀ x\, x' ∈ X, π(x) = π(x') ⇔ x ∼ x'$.

Il est courant d'utiliser une notation plus ramassée pour $π(x)$, souvent $\bar x$ ou $[x]$, ou bien une notation plus spécialisée comme $\frac{p}q$ pour un nombre rationnel. Bien sûr il peut y avoir plusieurs relations d'équivalence sur le même ensemble dans un contexte donné. Il est alors nécessaire d'utiliser une notation faisant apparaître explicitement la relation.

Comme annoncé, ce théorème est très proche des fondements des mathématiques, donc son statut et sa démonstration dépendent du système de fondements choisi. Pour cette raison, et pour garder l'attention sur l'énoncé, la discussion de cette question ne fait pas partie du cours. Les lecteurs frustrés pourront lire les paragraphes de complément à la fin de ce chapitre.

Dans Lean, la paire formée par une relation sur $X$ et une démonstration du fait qu'il s'agit d'une relation d'équivalence est un objet s de type setoid X. Le quotient $X/{∼}$ est alors noté quotient s. La relation d'équivalence est notée ≈ et la projection de x dans le quotient est notée ⟦x⟧. Les différentes informations contenues dans le théorème sont réparties dans les trois lemmes suivants.

lemma quotient.exists_repr : ∀ q : quotient s, ∃ x : X, q = ⟦x⟧

lemma quotient.sound : ∀ x x' : X, x ≈ x' →  ⟦x⟧ = ⟦x'⟧

lemma quotient.exact : ∀ x x' : X, ⟦x⟧ = ⟦x'⟧ →  x ≈ x'

En pratique le dernier lemme ci-dessus n'est pas très utile une fois démontré le théorème suivant, qui explique comment construire une fonction définie sur $X/{∼}$.

Théorème

Soit $X$ un ensemble muni d'une relation d'équivalence $∼$. Soit $f$ une fonction de $X$ dans un ensemble $Y$. Les conditions suivantes sont équivalentes :

  1. il existe $\bar f : X/{∼} → Y$ telle que $\bar f ∘ π = f$
  2. $∀ x, x' ∈ X,\; x ∼ x' ⇒ f(x) = f(x')$.

Lorsque les conditions du théorème sont vérifiées, on dit que « $f$ descend au quotient ». La fonction $\bar f$ est alors unique, elle est appelée « fonction induite par $f$ sur $X/{∼}$ ».

Ce théorème est une conséquence assez directe du théorème précédent. Supposons d'abord la première condition. Soit $x$ et $x'$ des éléments de $X$ qui sont équivalents : $x ∼ x'$. La première condition garantit $f(x) = \bar f(π(x))$ et $f(x') = \bar f(π(x'))$. Or le théorème précédent assure que $π(x) = π(x')$ donc ces deux expressions sont égales. L'autre implication est un peu plus délicate. Supposons la condition 2. L'idée est que la contrainte $\bar f ∘ π = f$ spécifie entièrement $\bar f$ car $π$ est surjective (au passage cela montre l'unicité). A priori cette spécification est sur-déterminée car chaque point du quotient peut avoir de nombreuses préimages dans $X$ mais la condition 2 assure que ce n'est pas un problème : tous les choix de préimage donne la même valeur dans $Y$. Plus précisément, la surjectivité $∀ q ∈ X/{∼}, ∃ x ∈ X, π(x) = q$ et l'axiome du choix fournissent une fonction $σ : X/{∼} → X$ telle que $π ∘ σ = Id$. Montrons que $\bar f = f ∘ σ$ convient. Pour tout $x$ dans $X$, $σ(π(x)) ∼ x$ car tous deux se projettent sur $π(x)$. Donc la condition 2 assure que $\bar f(π(x))$, qui vaut $f(σ(π(x)))$ par construction, vaut aussi $f(x)$.

À titre d'exemple de manipulation de quotient dans Lean, et dans l'espoir de mieux comprendre la délicate démonstration ci-dessus, voyons comment convaincre Lean de ce théorème. Comme $\bar f$ n'a pas de jolie écriture en unicode, on le note φ. On rappelle que, par défaut, Lean note les relations d'équivalence ≈ plutôt que $∼$ et la projection $π(x)$ comme ⟦x⟧.

Théorème

Soit $X$ un ensemble muni d'une relation d'équivalence $∼$. Soit $f$ une fonction de $X$ dans un ensemble $Y$. \[ \big(∃ φ : X/{∼} → Y, ∀ x ∈ X, φ(π(x)) = f(x) \big) ⇔ \big(∀ x, x' ∈ X,\; x ∼ x' ⇒ f(x) = f(x')\big). \]

theorem passage_au_quotient (X Y : Type) (s : setoid X) (f : X → Y) :
(∃ φ : quotient s → Y, ∀ x : X, φ(⟦x⟧) = f x) ↔ (∀ x x', x ≈ x' → f x = f x') :=
Démonstration
Montrons les deux implications. 
  split,

X Y : Type,
s : setoid X,
f : X → Y
⊢ (∃ (φ : quotient s → Y), ∀ (x : X), φ ⟦x⟧ = f x) ↔ ∀ (x x' : X), x ≈ x' → f x = f x'

2 goals
X Y : Type,
s : setoid X,
f : X → Y
⊢ (∃ (φ : quotient s → Y), ∀ (x : X), φ ⟦x⟧ = f x) → ∀ (x x' : X), x ≈ x' → f x = f x'

X Y : Type,
s : setoid X,
f : X → Y
⊢ (∀ (x x' : X), x ≈ x' → f x = f x') → (∃ (φ : quotient s → Y), ∀ (x : X), φ ⟦x⟧ = f x)
On commence par supposer la condition de gauche. 
    intro hyp,

X Y : Type,
s : setoid X,
f : X → Y
⊢ (∃ (φ : quotient s → Y), ∀ (x : X), φ ⟦x⟧ = f x) → ∀ (x x' : X), x ≈ x' → f x = f x'

X Y : Type,
s : setoid X,
f : X → Y,
hyp : ∃ (φ : quotient s → Y), ∀ (x : X), φ ⟦x⟧ = f x
⊢ ∀ (x x' : X), x ≈ x' → f x = f x'
Fixons un $φ$ vérifiant cette propriété. 
    cases hyp with φ Hφ,

X Y : Type,
s : setoid X,
f : X → Y,
hyp : ∃ (φ : quotient s → Y), ∀ (x : X), φ ⟦x⟧ = f x
⊢ ∀ (x x' : X), x ≈ x' → f x = f x'

X Y : Type,
s : setoid X,
f : X → Y,
φ : quotient s → Y,
Hφ : ∀ (x : X), φ ⟦x⟧ = f x
⊢ ∀ (x x' : X), x ≈ x' → f x = f x'
Soit $x$ et $x'$ des éléments équivalents de $X$. 
    intros x x' Hxx',

X Y : Type,
s : setoid X,
f : X → Y,
φ : quotient s → Y,
Hφ : ∀ (x : X), φ ⟦x⟧ = f x
⊢ ∀ (x x' : X), x ≈ x' → f x = f x'

X Y : Type,
s : setoid X,
f : X → Y,
φ : quotient s → Y,
Hφ : ∀ (x : X), φ ⟦x⟧ = f x,
x x' : X,
Hxx' : x ≈ x'
⊢ f x = f x'
On veut montrer que $f(x) = f(x')$. Vu la propriété supposée pour $φ$, on peut réécrire le membre de gauche comme $φ(π(x))$ et celui de droite comme $φ(π(x))$. 
    rw ← Hφ  x,

X Y : Type,
s : setoid X,
f : X → Y,
φ : quotient s → Y,
Hφ : ∀ (x : X), φ ⟦x⟧ = f x,
x x' : X,
Hxx' : x ≈ x'
⊢ f x = f x'

X Y : Type,
s : setoid X,
f : X → Y,
φ : quotient s → Y,
Hφ : ∀ (x : X), φ ⟦x⟧ = f x,
x x' : X,
Hxx' : x ≈ x'
⊢ φ ⟦x⟧ = f x'

    rw ← Hφ x',

X Y : Type,
s : setoid X,
f : X → Y,
φ : quotient s → Y,
Hφ : ∀ (x : X), φ ⟦x⟧ = f x,
x x' : X,
Hxx' : x ≈ x'
⊢ φ ⟦x⟧ = f x'

X Y : Type,
s : setoid X,
f : X → Y,
φ : quotient s → Y,
Hφ : ∀ (x : X), φ ⟦x⟧ = f x,
x x' : X,
Hxx' : x ≈ x'
⊢ φ ⟦x⟧ = φ ⟦x'⟧
Le point clef est que, puisque $x ∼ x'$, le théorème fondamentalde la théorie des quotients assure $π(x) = π(x')$ 
    have clef : ⟦x⟧ = ⟦x'⟧,

X Y : Type,
s : setoid X,
f : X → Y,
φ : quotient s → Y,
Hφ : ∀ (x : X), φ ⟦x⟧ = f x,
x x' : X,
Hxx' : x ≈ x'
⊢ φ ⟦x⟧ = φ ⟦x'⟧

2 goals
X Y : Type,
s : setoid X,
f : X → Y,
φ : quotient s → Y,
Hφ : ∀ (x : X), φ ⟦x⟧ = f x,
x x' : X,
Hxx' : x ≈ x'
⊢ ⟦x⟧ = ⟦x'⟧

X Y : Type,
s : setoid X,
f : X → Y,
φ : quotient s → Y,
Hφ : ∀ (x : X), φ ⟦x⟧ = f x,
x x' : X,
Hxx' : x ≈ x',
clef : ⟦x⟧ = ⟦x'⟧
⊢ φ ⟦x⟧ = φ ⟦x'⟧

    { exact quotient.sound Hxx' },

2 goals
X Y : Type,
s : setoid X,
f : X → Y,
φ : quotient s → Y,
Hφ : ∀ (x : X), φ ⟦x⟧ = f x,
x x' : X,
Hxx' : x ≈ x'
⊢ ⟦x⟧ = ⟦x'⟧

X Y : Type,
s : setoid X,
f : X → Y,
φ : quotient s → Y,
Hφ : ∀ (x : X), φ ⟦x⟧ = f x,
x x' : X,
Hxx' : x ≈ x',
clef : ⟦x⟧ = ⟦x'⟧
⊢ φ ⟦x⟧ = φ ⟦x'⟧

X Y : Type,
s : setoid X,
f : X → Y,
φ : quotient s → Y,
Hφ : ∀ (x : X), φ ⟦x⟧ = f x,
x x' : X,
Hxx' : x ≈ x',
clef : ⟦x⟧ = ⟦x'⟧
⊢ φ ⟦x⟧ = φ ⟦x'⟧
On conclue en reportant cette égalité dans notre objectif, qui devient une tautologie. 
    rw clef },

X Y : Type,
s : setoid X,
f : X → Y,
φ : quotient s → Y,
Hφ : ∀ (x : X), φ ⟦x⟧ = f x,
x x' : X,
Hxx' : x ≈ x',
clef : ⟦x⟧ = ⟦x'⟧
⊢ φ ⟦x⟧ = φ ⟦x'⟧

X Y : Type,
s : setoid X,
f : X → Y
⊢ (∀ (x x' : X), x ≈ x' → f x = f x') → (∃ (φ : quotient s → Y), ∀ (x : X), φ ⟦x⟧ = f x)
Réciproquement, supposons la condition de droite et construisons une fonction $φ$ convenable. 
    intro hyp,

X Y : Type,
s : setoid X,
f : X → Y
⊢ (∀ (x x' : X), x ≈ x' → f x = f x') → (∃ (φ : quotient s → Y), ∀ (x : X), φ ⟦x⟧ = f x)

X Y : Type,
s : setoid X,
f : X → Y,
hyp : ∀ (x x' : X), x ≈ x' → f x = f x'
⊢ ∃ (φ : quotient s → Y), ∀ (x : X), φ ⟦x⟧ = f x
Le théorème fondamental assure que $π$ est surjectif. 
    have surj : ∀ q, ∃ x : X, ⟦x⟧ = q,

X Y : Type,
s : setoid X,
f : X → Y,
hyp : ∀ (x x' : X), x ≈ x' → f x = f x'
⊢ ∃ (φ : quotient s → Y), ∀ (x : X), φ ⟦x⟧ = f x

2 goals
X Y : Type,
s : setoid X,
f : X → Y,
hyp : ∀ (x x' : X), x ≈ x' → f x = f x'
⊢ ∀ (q : quotient s), ∃ (x : X), ⟦x⟧ = q

X Y : Type,
s : setoid X,
f : X → Y,
hyp : ∀ (x x' : X), x ≈ x' → f x = f x',
surj : ∀ (q : quotient s), ∃ (x : X), ⟦x⟧ = q
⊢ ∃ (φ : quotient s → Y), ∀ (x : X), φ ⟦x⟧ = f x

    { apply quotient.exists_rep },

2 goals
X Y : Type,
s : setoid X,
f : X → Y,
hyp : ∀ (x x' : X), x ≈ x' → f x = f x'
⊢ ∀ (q : quotient s), ∃ (x : X), ⟦x⟧ = q

X Y : Type,
s : setoid X,
f : X → Y,
hyp : ∀ (x x' : X), x ≈ x' → f x = f x',
surj : ∀ (q : quotient s), ∃ (x : X), ⟦x⟧ = q
⊢ ∃ (φ : quotient s → Y), ∀ (x : X), φ ⟦x⟧ = f x

X Y : Type,
s : setoid X,
f : X → Y,
hyp : ∀ (x x' : X), x ≈ x' → f x = f x',
surj : ∀ (q : quotient s), ∃ (x : X), ⟦x⟧ = q
⊢ ∃ (φ : quotient s → Y), ∀ (x : X), φ ⟦x⟧ = f x
L'axiome du choix donne alors une fonction $σ : X/{∼} → X$ qui est un inverse à droite de $π$. 
    choose σ Hσ using surj,

X Y : Type,
s : setoid X,
f : X → Y,
hyp : ∀ (x x' : X), x ≈ x' → f x = f x',
surj : ∀ (q : quotient s), ∃ (x : X), ⟦x⟧ = q
⊢ ∃ (φ : quotient s → Y), ∀ (x : X), φ ⟦x⟧ = f x

X Y : Type,
s : setoid X,
f : X → Y,
hyp : ∀ (x x' : X), x ≈ x' → f x = f x',
σ : quotient s → X,
Hσ : ∀ (q : quotient s), ⟦σ q⟧ = q
⊢ ∃ (φ : quotient s → Y), ∀ (x : X), φ ⟦x⟧ = f x
Montrons que la fonction qui envoie $q$ sur $f(σ(q))$ convient, 
    use λ q, f (σ q),

X Y : Type,
s : setoid X,
f : X → Y,
hyp : ∀ (x x' : X), x ≈ x' → f x = f x',
σ : quotient s → X,
Hσ : ∀ (q : quotient s), ⟦σ q⟧ = q
⊢ ∃ (φ : quotient s → Y), ∀ (x : X), φ ⟦x⟧ = f x

X Y : Type,
s : setoid X,
f : X → Y,
hyp : ∀ (x x' : X), x ≈ x' → f x = f x',
σ : quotient s → X,
Hσ : ∀ (q : quotient s), ⟦σ q⟧ = q
⊢ ∀ (x : X), f (σ ⟦x⟧) = f x
Dire qu'elle convient signifie que, pour tout $x$ dans $X$, $f(σ(π(x))) = f(x)$. Soit $x$ dans $X$. 
    intro x,

X Y : Type,
s : setoid X,
f : X → Y,
hyp : ∀ (x x' : X), x ≈ x' → f x = f x',
σ : quotient s → X,
Hσ : ∀ (q : quotient s), ⟦σ q⟧ = q
⊢ ∀ (x : X), f (σ ⟦x⟧) = f x

X Y : Type,
s : setoid X,
f : X → Y,
hyp : ∀ (x x' : X), x ≈ x' → f x = f x',
σ : quotient s → X,
Hσ : ∀ (q : quotient s), ⟦σ q⟧ = q,
x : X
⊢ f (σ ⟦x⟧) = f x
Le point clef est que le théorème fondamental et la propriété de $σ$ assurent que $σ(π(x))$ et $x$ sont équivalents. 
    have clef : σ ⟦x⟧ ≈ x,

X Y : Type,
s : setoid X,
f : X → Y,
hyp : ∀ (x x' : X), x ≈ x' → f x = f x',
σ : quotient s → X,
Hσ : ∀ (q : quotient s), ⟦σ q⟧ = q,
x : X
⊢ f (σ ⟦x⟧) = f x

2 goals
X Y : Type,
s : setoid X,
f : X → Y,
hyp : ∀ (x x' : X), x ≈ x' → f x = f x',
σ : quotient s → X,
Hσ : ∀ (q : quotient s), ⟦σ q⟧ = q,
x : X
⊢ σ ⟦x⟧ ≈ x

X Y : Type,
s : setoid X,
f : X → Y,
hyp : ∀ (x x' : X), x ≈ x' → f x = f x',
σ : quotient s → X,
Hσ : ∀ (q : quotient s), ⟦σ q⟧ = q,
x : X,
clef : σ ⟦x⟧ ≈ x
⊢ f (σ ⟦x⟧) = f x

    { apply quotient.exact,

2 goals
X Y : Type,
s : setoid X,
f : X → Y,
hyp : ∀ (x x' : X), x ≈ x' → f x = f x',
σ : quotient s → X,
Hσ : ∀ (q : quotient s), ⟦σ q⟧ = q,
x : X
⊢ σ ⟦x⟧ ≈ x

X Y : Type,
s : setoid X,
f : X → Y,
hyp : ∀ (x x' : X), x ≈ x' → f x = f x',
σ : quotient s → X,
Hσ : ∀ (q : quotient s), ⟦σ q⟧ = q,
x : X,
clef : σ ⟦x⟧ ≈ x
⊢ f (σ ⟦x⟧) = f x

X Y : Type,
s : setoid X,
f : X → Y,
hyp : ∀ (x x' : X), x ≈ x' → f x = f x',
σ : quotient s → X,
Hσ : ∀ (q : quotient s), ⟦σ q⟧ = q,
x : X
⊢ ⟦σ ⟦x⟧⟧ = ⟦x⟧

      exact Hσ ⟦x⟧ },

X Y : Type,
s : setoid X,
f : X → Y,
hyp : ∀ (x x' : X), x ≈ x' → f x = f x',
σ : quotient s → X,
Hσ : ∀ (q : quotient s), ⟦σ q⟧ = q,
x : X
⊢ ⟦σ ⟦x⟧⟧ = ⟦x⟧

X Y : Type,
s : setoid X,
f : X → Y,
hyp : ∀ (x x' : X), x ≈ x' → f x = f x',
σ : quotient s → X,
Hσ : ∀ (q : quotient s), ⟦σ q⟧ = q,
x : X,
clef : σ ⟦x⟧ ≈ x
⊢ f (σ ⟦x⟧) = f x
Par hypothèse sur $f$, cette équivalence est suffisante pour assurer $f (σ(π(x))) = f x$. 
    exact hyp (σ ⟦x⟧) x clef },

X Y : Type,
s : setoid X,
f : X → Y,
hyp : ∀ (x x' : X), x ≈ x' → f x = f x',
σ : quotient s → X,
Hσ : ∀ (q : quotient s), ⟦σ q⟧ = q,
x : X,
clef : σ ⟦x⟧ ≈ x
⊢ f (σ ⟦x⟧) = f x

no goals
QED.

Dans Lean, la fonction $φ$ promise par l'énoncé précédent est notée quotient.lift f h avec h : ∀ x x', x ≈ x' → f x = f x'.

Dans la pratique, il est courant de vouloir définir des fonctions dont l'ensemble de départ et l'ensemble d'arrivée sont des ensembles quotients, ainsi que des fonctions sur des produits d'ensembles quotient. Le théorème précédent donne par exemple le corollaire suivant, qui permet de définir des opérations algébriques telles que l'addition et la multiplication de nombres rationnels.

Corollaire

Soit $X$ un ensemble muni d'une relation d'équivalence $∼$. Soit $f$ une fonction de $X × X$ dans $X$. Si \[ ∀ x\, x'\, y\, y' ∈ X, x ∼ x' \text{ et } y ∼ y' ⇒ f(x, y) ∼ f(x', y') \] alors il existe une unique fonction $\bar f : X/{∼} × X/{∼} → X/{∼}$ telle que $∀ x\, y ∈ X, \bar f(π(x), π(y)) = π(f(x, y))$.

Ce corollaire s'obtient en appliquant deux fois le théorème après avoir composé $f$ avec la projection $π$, de sorte que l'hypothèse devienne $∀ x\, x'\, y\, y' ∈ X, x ∼ x' \text{ et } y ∼ y' ⇒ π(f(x, y)) = π(f(x', y'))$.

Par exemple, en appliquant ce théorème à la fonction qui envoie $((p₁, q₁), (p₂, q₂))$ sur $(p₁q₂ + p₂q₁, q₁q₂)$ on obtient l'addition $ℚ × ℚ → ℚ$.

Dans Lean, la fonction $φ$ promise par l'énoncé précédent est notée quotient.lift₂ f h avec h : ∀ x x' y y', x ≈ x' → y ≈ y' → f x = f x'.

Complément

Comme expliqué plus haut, la démonstration éventuelle du théorème fondamental de la théorie des quotients n'est pas un objectif de ce cours. Les paragraphes suivants sont destinés aux lecteurs curieux que cette exclusion risque de frustrer.

Comme annoncé, ce théorème est très proche des fondements des mathématiques, donc son statut et sa démonstration dépendent du système de fondements choisi. En fondant tout sur la théorie des ensembles (au sens fort évoqué dans le chapitre sur les ensembles, en se méfiant des paradoxes comme celui qui proviendrait d'un ensemble des ensembles qui ne se contiennent pas) on peut démontrer le théorème en passant par la partition de $X$ associée à $∼$, au sens du cours de Graphes, et en définissant $X/{∼}$ comme ensemble des classes d'équivalences de cette partition. Chaque élément de $X/{∼}$ est donc un ensemble inclus dans $X$. Mais cette construction n'est qu'un détail de la démonstration, qui obscurcit l'énoncé en faisant apparaître une structure interne des éléments de $X/{∼}$ qui, par rapport au but recherché, n'est qu'un bruit parasite. Par exemple on veut penser à un nombre rationnel comme à un nombre, pas une classe infinie de paires de nombres entiers.

Dans les fondations utilisées par Lean, ce théorème est essentiellement un axiome, ce qui évite les distractions évoquées au paragraphe précédent. Cette absence de démonstration pourrait être vue comme une faiblesse, mais elle provient aussi du cadre d'application plus vaste de la notion de relation d'équivalence dans Lean. Ainsi on peut démontrer sans problème que l'équivalence logique (le connecteur $⇔$) est une relation d'équivalence sur le type d'objet mathématique des énoncés, le type Prop. Une telle affirmation n'a aucun sens dans le contexte des mathématiques fondées sur la théorie des ensembles car ces fondations séparent entièrement la logique des objets mathématiques manipulés.

La feuille de td 7 contient des exercices sur ce cours. En étant patient, car un navigateur web n'est pas prévu pour faire tourner un assistant de démonstration, on peut travailler sur cette feuilles en ligne là.