[Gröbner] Début de démonstration de correction de l'algorithme d'inversion.

1 files changed, 9 insertions, 0 deletions

diff --git a/chapitres/bases-groebner.tex b/chapitres/bases-groebner.tex
index e82f27f..19c93e3 100644
--- a/chapitres/bases-groebner.tex
+++ b/chapitres/bases-groebner.tex
@@ -1449,6 +1449,15 @@ où $I'=I$ et $C$ est vide, il ne se produit que lorsque
 $k[Z_1,\ldots,Z_d]/I$ est l'algèbre nulle, ce cas étant trivial).
 \end{proof}
 \begin{proof}
+On sait d'après \ref{base-de-groebner-elimination} que l'ensemble $B'
+= \tilde B \cap k[Z_1,\ldots,Z_d]$ des éléments de $\tilde B$ ne
+faisant intervenir que les variables $Z_1,\ldots,Z_d$ est la base de
+Gröbner réduite de $I' = \tilde I \cap k[Z_1,\ldots,Z_d]$ (soulignons
+que cet idéal contient $I$).  Si on note $A = k[Z_1,\ldots,Z_d]/I$,
+alors $k[Z_1,\ldots,Z_d,Y]/\tilde I = A[Y]/(xY-1)$.  L'élément $x$ de
+$A$ est inversible si et seulement si la flèche évidente $A \to
+A[Y]/(xY-1)$ est un isomorphisme.
+
 \XXX
 \end{proof}