title: Lemme de contraction de Mostowski
text: # Lemme de contraction de Mostowski
  
  En théorie des ensembles le lemme de contraction de Mostowski, dû à Andrzej Mostowski, associe à un ensemble muni d'une relation bien fondée un unique ensemble transitif, de façon que, si celui-ci est muni de l'appartenance, cette application est un morphisme. Si de plus la relation bien fondée sur l'ensemble de départ est extensionnelle, l'application est un isomorphisme. L'ensemble image est appelé contracté, ou collapse de Mostowski de l'ensemble muni de la relation bien fondée.
  
  Le lemme se généralise aux classes, moyennant que les antécédents d'un élément de la classe par la relation bien fondée considérée — cette relation étant elle-même une classe — forment un ensemble.
  
  Il intervient pour la construction de modèles de la théorie des ensembles, par exemple dans le cas du forcing.
  
  ## Cas ensembliste
  
  Soit A un ensemble et R une relation bien fondée sur cet ensemble. Alors il existe une et une seule fonction φ vérifiant
  
      φ( x ) = { φ( y ) | y ∈ A et y R x }.
  
  Cette relation permet en effet de définir φ par récurrence sur la relation bien fondée R.
  
  La fonction φ est la fonction contractante ((en)collapsing function) de l'ensemble (A, R). Son ensemble image T est le contracté ou collapse de Mostowski de (A, R). La fonction φ est un morphisme de (A, R) sur (T, ∈) : la relation qui permet de la définir par récurrence dit bien exactement que pour x ∈ A et y ∈ A
  
      φ( y ) ∈ φ( x ) si et seulement si y R x.
  
  Cet ensemble est transitif par construction.
  
  La fonction φ est surjective sur T mais peut ne pas être injective : deux éléments de A qui ont les mêmes antécédents par R sont identifiés par φ (c'est un collapse extensionnel).
  
  Un cas particulier intéressant est celui ou la relation R est extensionnelle sur A c'est-à-dire que (A, R) satisfait l'axiome d'extensionnalité, ce qui s'écrit
  
      ∀ x ∈ A ∀ y ∈ A [ ∀ z ∈ A (z R x ⇔ z R y) ⇒ x = y ].
  
  Par exemple la relation d'ordre strict d'un ensemble totalement ordonné est extensionnelle.
  
  Si la relation R est extensionnelle la fonction φ est un isomorphisme de (A, R) sur (I, ∈).
  
  En effet φ est déjà un morphisme surjectif sur T, et on montre par induction sur la relation bien fondée R, que pour tout x ∈ A
  
      ∀ y ∈ A ( φ(x) = φ(y) ⇒ x = y ).
  
  La propriété est supposée vraie pour tous les R-antécédents de x. Si φ(x) = φ(y), c'est que x et y ont même R-antécédents (définitions de φ(x) et φ(y)), et donc qu'ils sont égaux par extensionnalité. Le morphisme φ est donc injectif, donc bijectif.
  
  En résumé.
  
  Lemme de Mostowski (cas ensembliste).— Si (A, R) est un ensemble muni d'une relation bien fondée R, alors il existe un unique ensemble transitif T et une unique fonction φ tels que φ soit un morphisme surjectif de (A, R) sur (T, ∈). Si de plus R est extensionnelle sur A, φ est un isomorphisme.
  
  Par exemple pour {a, b}, avec l'ordre strict défini par a < b, φ(a) = ∅, φ(b) = {φ(a)} = {∅}, le collapse de Mostowski de ({a, b}, <) est { ∅, {∅} }, soit l'ordinal 2.
  
  Plus généralement si (A, <) est un bon ordre strict, l'ordre associé est total, le collapse de Mostowski est l'unique ordinal isomorphe à ce bon ordre.
  
  Le lemme de contraction de Mostowski se démontre dans la théorie des ensembles de Zermelo-Fraenkel ZF sans axiome de fondation. L'axiome de l'ensemble des parties n'est pas non plus nécessaire.
  
  ## Appartenance et axiome de fondation
  
  En présence de l'axiome de fondation, le lemme de Mostowski s'applique à un ensemble A muni de l'appartenance. Si la relation d'appartenance est extensionnelle sur A, soit (A, ∈) satisfait l'axiome d'extensionnalité, on dit que A est extensionnel.
  
      L'ensemble A est extensionnel quand ∀ x ∈ A ∀ y ∈ A [(x ∩ A = y ∩ A) ⇒ x = y ].
  
  Dans ce cas particulier le lemme de Mostowski devient alors
  
      Un ensemble extensionnel est isomorphe à un unique ensemble transitif, par un unique isomorphisme.
  
  ## Cas des classes
  
  Le lemme se généralise aux classes, mais il faut alors supposer que la « relation » R, qui alors est également une classe, a pour propriété que, pour tout x élément de A, la classe des R-antécédents de x est un ensemble. La « fonction » φ est alors une classe fonctionnelle. Cette condition est utile pour démontrer le théorème de définition par récurrence sur la classe relationnelle R, en l'occurrence pour démontrer l'existence de la classe fonctionnelle φ.
  
  