From 13a8682830699d47aa9ece468822f30af7075bcd Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Fri, 12 Feb 2016 23:35:40 +0100
Subject: Linear disjointness, subextensions of finite type.

---
 notes-accq205.tex | 299 ++++++++++++++++++++++++++++++++++++++++++++++++------
 1 file changed, 266 insertions(+), 33 deletions(-)

(limited to 'notes-accq205.tex')

diff --git a/notes-accq205.tex b/notes-accq205.tex
index aa4d2e3..546d703 100644
--- a/notes-accq205.tex
+++ b/notes-accq205.tex
@@ -66,6 +66,8 @@ Git: \input{vcline.tex}
 \immediate\write18{echo ' (stale)' >> vcline.tex}
 \par}
 
+\pretolerance=8000
+\tolerance=50000
 
 
 %
@@ -287,6 +289,14 @@ famille donnée.  (Autrement dit, $y \in A$ appartient à $k[x_i]_{i\in
   I}$ si et selement si il existe $J\subseteq I$ fini tel que $y$
 appartienne à $k[x_i]_{i\in J}$.)
 
+\danger Attention : une sous-algèbre d'une algèbre de type fini n'est
+pas, en général, de type fini.  Un contre-exemple est fourni par
+l'anneau des polynômes $f \in k[x,y]$ à deux indéterminées sur un
+corps $k$ qui prennent une valeur constante sur l'axe des ordonnées :
+cette $k$-algèbre est engendrée par $1, x, xy, xy^2, xy^3,\ldots$ et
+on peut montrer qu'aucun nombre fini de ses éléments ne suffit à
+l'engendrer.
+
 \thingy Une \textbf{extension de corps} est un morphisme d'anneaux $k
 \to K$ entre corps (c'est-à-dire que $K$ est une $k$-algèbre qui est
 un corps).  Un tel morphisme est automatiquement injectif (car son
@@ -341,13 +351,21 @@ fini) de la famille donnée.  (Autrement dit, $y \in K$ appartient à
 $k(x_i)_{i\in I}$ si et selement si il existe $J\subseteq I$ fini tel
 que $y$ appartienne à $k(x_i)_{i\in J}$.)
 
+Contrairement au cas des algèbres
+(cf. \ref{subalgebra-generated-is-polynomials}), il \emph{est} bien
+vrai qu'une sous-extension d'une extension de corps de type fini est
+de type fini.  Mais ce n'est pas évident !  (Cela sera démontré en
+\ref{subextension-of-finite-type-is-of-finite-type} ci-dessous.)
+
+
 \subsection{Extensions algébriques et degré}
 
 \thingy\label{monogeneous-extensions-dichotomy} Si $k \subseteq K$ est
 une extension de corps et $x\in K$, on a noté
 (cf. \ref{subfield-generated}) $k(x)$ l'extension de $k$ engendrée
 par $x$.  On dira aussi que $k \subseteq k(x)$ est une extension
-\textbf{monogène}.
+\textbf{monogène} (certains auteurs utilisent « simple », notamment en
+anglais).
 
 On se pose la question de mieux comprendre cette extension.  Pour
 cela, on introduit l'unique morphisme $\varphi\colon k[t] \to K$, où
@@ -417,8 +435,9 @@ irréductibles dans $k[t]$ sont les $t-a$.
 considérer $K$ comme un $k$-espace vectoriel, et sa dimension (finie
 ou infinie) est notée $[K:k]$ et appelée \textbf{degré} de
 l'extension.  Une extension de degré fini est aussi dite
-\textbf{finie}.  Il va de soi qu'une sous-extension d'une extension
-finie est encore finie.
+\textbf{finie} (ainsi, on pourra dire simplement que $K$ est « fini
+sur $k$ » pour dire que son degré est fini).  Il va de soi qu'une
+sous-extension d'une extension finie est encore finie.
 
 Il résulte de l'identification de $k(x)$ à $k[t]/(\mu_x)$ que, si $x$
 est un élément algébrique sur $k$, alors $[k(x):k]$ est fini et égal
@@ -498,6 +517,144 @@ algébriques sur $k$, donc certainement aussi sur $k(t_1,\ldots,t_n)$,
 et on applique \ref{basic-facts-algebraic-extensions}(3).)
 
 
+\subsection{Extensions linéairement disjointes}
+
+\begin{defn}\label{definition-linear-disjointness}
+Si $k \subseteq K$ et $k \subseteq L$ sont deux extensions contenues
+dans une même troisième $M$, on dit qu'elles sont \textbf{linéairement
+  disjointes} lorsque toute famille d'éléments de $K$ linéairement
+indépendante sur $k$ est encore linéairement indépendante sur $L$
+quand on la voit comme une famille d'éléments de $M$.  (Il suffit,
+bien sûr, de le tester pour des familles \emph{finies}.)
+\end{defn}
+
+La définition de cette relation n'est pas symétrique.  Elle l'est
+cependant :
+\begin{prop}
+La propriété pour deux extensions contenues dans une même troisième
+d'être linéairement disjointes est symétrique.
+\end{prop}
+\begin{proof}
+Supposons $k \subseteq K$ et $k \subseteq L$ linéairement disjointes
+comme on vient de le définir : on veut inverser le rôle de $L$ et $K$.
+Soient $y_1,\ldots,y_n$ des éléments de $L$ linéairement indépendants
+sur $k$.  Supposons que pour certains $x_1,\ldots,x_n$ de $K$ non tous
+nuls, on ait $x_1 y_1 + \cdots + x_n y_n = 0$ dans $M$.  Quitte à
+réordonner les $x_i$, on peut supposer que $x_1,\ldots,x_r$ sont
+linéairement indépendants sur $k$ (avec $r\geq 1$) et que
+$x_{r+1},\ldots,x_n$ en sont des combinaisons $k$-linéaires, disons
+$x_i = \sum_{j=1}^r c_{i,j} x_j$ pour $i>r$ avec $c_{i,j} \in k$.  La
+relation $\sum_{i=1}^n x_i y_i = 0$ devient donc $\sum_{i=1}^r x_i y_i
++ \sum_{i=r+1}^n \sum_{j=1}^r c_{i,j} x_j y_i = 0$, soit, en
+regroupant : $\sum_{j=1}^r \big(y_j + \sum_{i=r+1}^n c_{i,j} y_i\big)
+x_j = 0$.  Par indépendance linéaire des $x_i$ sur $k$ donc sur $L$,
+on a $y_j + \sum_{i=r+1}^n c_{i,j} y_i = 0$ pour chaque $j\leq r$, ce
+qui contredit l'indépendance linéaire des $y_i$ sur $L$.
+\end{proof}
+
+\thingy Lorsque $k \subseteq K$ et $k \subseteq L$ sont deux
+extensions contenues dans une même troisième $M$, on appelle
+\textbf{composé} des corps $K$ et $L$ le sous-corps de $M$ engendré
+par $K$ et $L$, autrement dit $k(K \cup L) = K(L) = L(K)$, et on le
+note $K.L$.
+
+\danger Il faut prendre garde au fait que l'extension composée n'a de
+sens que si les deux extensions sont contenues dans une même troisième
+(en changeant les plongements de $K$ et $L$ dans $M$ on peut changer
+$K.L$ en un corps non isomorphe).
+
+\begin{prop}\label{compositum-generated-by-products}
+Si $k \subseteq K$ est une extension algébrique et $k \subseteq L$ une
+extension quelconque, toutes les deux contenues dans une même
+extension $M$, alors l'extension composée $K.L$ est le sous-$k$-espace
+vectoriel de $M$ engendré par les produits $xy$ avec $x\in K$ et $y\in
+L$.
+\end{prop}
+\begin{proof}
+Soit $V$ le sous-$k$-espace vectoriel de $M$ engendré par les produits
+$xy$ avec $x\in K$ et $y\in L$, autrement dit l'ensemble des $\sum_i
+x_i y_i$ (sommes finies) avec $x_i \in K$ et $y_i \in L$ (les
+coefficients dans $k$ peuvent s'absorber dans les $x_i$ ou les $y_i$).
+Il est trivial que $V \subseteq K.L$, et pour prouver l'inclusion
+contraire il suffit de montrer que $V$ est bien un corps.  En
+développant les produits $(\sum_i x_i y_i)(\sum x'_j y'_j) =
+\sum_{i,j} (x_i x'_j)(y_i y'_j)$ on voit que $V$ est stable par
+produit : c'est donc une algèbre sur $k$ ou $K$ ou $L$ comme on
+préfère.  Comme $V$ est un sous-anneau de $M$, qui est un corps, il
+s'agit d'un anneau intègre.
+
+Dans le cas où $[K:k] < \infty$, on a $[V:L] < \infty$ car une famille
+génératrice $(v_j)$ de $K$ comme $k$-espace vectoriel est encore
+génératrice de $V$ comme $L$-espace vectoriel (en effet, si tout
+élément de $K$ peut s'écrire $\sum_j c_j v_j$ pour certains $c_i \in
+k$, alors tout élément de $V$ peut s'écrire $\sum_i (\sum_j c_{i,j}
+v_j) y_i = \sum_j (\sum_i c_{i,j} y_i) v_j$), et
+d'après \ref{finite-integral-algebra-is-a-field} on en déduit que $V$
+est un corps.  On a donc obtenu le résultat annoncé pour le cas
+où $[K:k] < \infty$.
+
+En général, si $z \in V$ n'est pas nul, on peut écrire $z = \sum_i x_i
+y_i$ pour certains $x_i \in K$ et $y_i \in L$.  Soit $K_0$ l'extension
+de $k$ engendrée par les $x_i$ : l'hypothèse selon laquelle $K$ est
+algébrique entraîne que $[K_0:k] < \infty$
+(cf. \ref{basic-facts-algebraic-extensions}(1)), et on a $z \in
+K_0.L$.  D'après le cas précédemment traité, tout élément de $K_0.L$,
+et en particulier $z^{-1}$, appartient au sous-$k$-espace vectoriel
+$V_0$ de $M$ engendré par les produits $xy$ avec $x\in K_0$ et $y\in
+L$, et on a bien sûr $V_0 \subseteq V$.  Donc $z^{-1} \in V$ et $V$
+est bien un corps.
+\end{proof}
+
+\begin{prop}\label{base-of-compositum}
+Si $k \subseteq K$ et $k \subseteq L$ sont deux extensions
+linéairement disjointes contenues dans une même troisième, et si l'une
+des deux est algébrique, alors toute base de $K$ sur $k$ est encore
+une base de $K.L$ sur $L$.
+\end{prop}
+\begin{proof}
+Soit $(v_j)$ une base de $K$ comme $k$-espace vectoriel.  D'après la
+définition de la relation d'être linéairement disjointes, les $(v_j)$
+vus dans $K.L$ sont linéairement indépendants sur $L$.  Mais d'après
+la proposition \ref{compositum-generated-by-products}, tout élément de
+$K.L$ peut s'écrire sous la forme d'une somme finie $\sum_i x_i y_i$
+pour des $x_i \in K$ et $y_i \in L$, et on peut réécrire $x_i = \sum
+c_{i,j} v_j$ donc $\sum_i x_i y_i = \sum_i (\sum_j c_{i,j} v_j) y_i =
+\sum_j (\sum_i c_{i,j} y_i) v_j$ appartient au $L$-espace vectoriel
+engendré dans $K.L$ par les $(v_j)$, c'est-à-dire que ceux-ci sont
+générateurs, et finalement sont une base de $K.L$.
+\end{proof}
+
+\begin{prop}\label{linear-disjointness-of-algebraic-and-transcendental}
+Soit $k \subseteq K$ une extension de corps, et $t_1,\ldots,t_n$ des
+indéterminées.  Alors les extension $k\subseteq K$ et $k\subseteq
+k(t_1,\ldots,t_n)$ sont linéairement disjointes dans
+$K(t_1,\ldots,t_n)$, i.e., toute famille $k$-linéairement
+indépendante de $K$ est encore linéairement indépendante sur
+$k(t_1,\ldots,t_n)$ (dans $K(t_1,\ldots,t_n)$).  Si de plus $K$ est
+algébrique sur $k$, alors toute base de $K$ comme $k$-espace
+vecotriel est une base de $K(t_1,\ldots,t_n)$ comme
+$k(t_1,\ldots,t_n)$-espace vectoriel.
+\end{prop}
+\begin{proof}
+Soit $(u_j)_{j\in J}$ une famille $k$-linéairement indépendante de
+$K$ : montrons qu'ils sont linéairement indépendants sur
+$k(t_1,\ldots,t_n)$.  Si on a une relation de dépendance linéaire non
+triviale $\sum_{j\in J} c_j u_j = 0$ dans $K(t_1,\ldots,t_n)$ avec
+les $c_j$ dans $k(t_1,\ldots,t_n)$ tous nuls sauf un nombre fini, les
+$c_j$ sont des fractions rationnelles ; cette même relation est
+valable si on multiplie les $c_j$ par un dénominateur commun, si bien
+qu'on peut supposer que les $c_j$ sont des polynômes en
+$t_1,\ldots,t_n$ ; quitte à diviser autant de fois que nécessaire par
+chaque $t_i$ qui divise tous les $c_j$, on peut supposer que le $c_j$
+ne s'annulent pas tous à l'origine (i.e., quand on remplace tous les
+$t_i$ par $0$) : mais alors, en les évaluant à l'origine (i.e., en
+remplaçant tous les $t_i$ par $0$), on obtient une relation de
+dépendance linéaire non-triviale sur $k$, qui est censée ne pas
+exister.  Ceci montre la première affirmation.  La seconde découle
+de \ref{base-of-compositum}.
+\end{proof}
+
+
 \subsection{Bases et degré de transcendance}
 
 \begin{defn}
@@ -515,16 +672,17 @@ chacun des $x_i$ est transcendant sur $k$ ; et un unique élément $x$
 de $K$ est algébriquement indépendant sur $k$ si et seulement si il
 est transcendant sur $k$.
 
-On dit d'une famille infinie $(x_i)$ d'éléments de $K$ qu'elle est
-algébriquement indépendante sur $k$ lorsque toute sous-famille finie
-d'entre eux l'est (i.e., il n'existe pas de relation de dépendance
-algébrique entre les $x_i$, c'est-à-dire entre un nombre fini d'entre
-eux).
-
-Une famille $(x_i)$ d'éléments de $K$ est appelée \textbf{base de
-  transcendance} de $K$ sur $k$ lorsqu'elle est algébriquement
-indépendante sur $k$ et que $K$ est algébrique au-dessus de
-l'extension $k(x_i)$ de $k$ engendrée par les $x_i$.
+On dit d'une famille infinie $(x_i)_{i\in I}$ d'éléments de $K$
+qu'elle est algébriquement indépendante sur $k$ lorsque toute
+sous-famille finie d'entre eux l'est (i.e., il n'existe pas de
+relation de dépendance algébrique entre les $x_i$, c'est-à-dire entre
+un nombre fini d'entre eux).
+
+Une famille $(x_i)_{i\in I}$ d'éléments de $K$ est appelée
+\textbf{base de transcendance} de $K$ sur $k$ lorsqu'elle est
+algébriquement indépendante sur $k$ et que $K$ est algébrique
+au-dessus de l'extension $k(x_i)_{i\in I}$ de $k$ engendrée par
+les $x_i$.
 \end{defn}
 
 \thingy\label{remark-indeterminates-versus-transcendentals} Il est trivialement le cas que $t_1,\ldots,t_n$ sont
@@ -544,11 +702,11 @@ infini d'indéterminées, comme « réunion », techniquement la limite
 inductive, des corps de fractions rationnelles sur une sous-famille
 finie quelconque d'entre elles.)
 
-\thingy Lorsque les $(x_i)$ sont algébriquement indépendants, on dit
-aussi que l'extension $k \subseteq k(x_i)$ est \textbf{transcendante
-  pure} : autrement dit, une extension transcendante pure est un corps
-de fractions rationnelles en un nombre quelconque (peut-être infini,
-cf. ci-dessus) de variables.
+\thingy Lorsque les $(x_i)_{i\in I}$ sont algébriquement indépendants,
+on dit aussi que l'extension $k \subseteq k(x_i)_{i\in I}$ est
+\textbf{transcendante pure} : autrement dit, une extension
+transcendante pure est un corps de fractions rationnelles en un nombre
+quelconque (peut-être infini, cf. ci-dessus) de variables.
 
 La question de déterminer si une extension de corps est transcendante
 pure peut être extrêmement difficile ; à titre d'exemple, le corps
@@ -565,10 +723,10 @@ algébriquement indépendants.  L'exemple ci-dessus montre que c'est
 abusif ; cependant, on verra que ce ne l'est plus si on sait que le
 degré de transcendance est bien $n$.
 
-Si $x_i$ est une base de transcendance de $K$ sur $k$, celle-ci
-« décompose » l'extension $k \subseteq K$ en deux : l'extension $k
-\subseteq k(x_i)$ est transcendante pure, et l'extension $k(x_i)
-\subseteq K$ est algébrique.
+Si $(x_i)_{i\in I}$ est une base de transcendance de $K$ sur $k$,
+celle-ci « décompose » l'extension $k \subseteq K$ en deux :
+l'extension $k \subseteq k(x_i)_{i\in I}$ est transcendante pure, et
+l'extension $k(x_i)_{i\in I} \subseteq K$ est algébrique.
 
 \begin{prop}\label{transcendence-basis-facts}
 Soit $k \subseteq K$ une extension de corps.
@@ -577,9 +735,9 @@ Soit $k \subseteq K$ une extension de corps.
 de $K$ se complète en une base de transcendance de $K$ sur $k$.  (Ceci
 s'applique notamment à la famille vide, donc il existe toujours une
 base de transcendance de $K$ sur $k$.)  (1b) De toute famille qui
-engendre $K$ en tant qu'extension de corps de $k$ (ou même : qui
+engendre $K$ en tant qu'extension de corps de $k$, ou même qui
 engendre un corps intermédiaire $E$ au-dessus duquel $K$ est
-algébrique) on peut extraire une base de transcendance.
+algébrique, on peut extraire une base de transcendance.
 
 (2) \textit{Lemme d'échange :} Si $z_1,\ldots,z_n$ est une base de
 transcendance finie de $K$ sur $k$ et $t$ un élément de $K$ tel que
@@ -605,13 +763,14 @@ cardinal.
   sur $k(x_i)_{i\in I}$.  Mais s'il l'est, on observe que la famille
   obtenue en rajoutant $t$ à la famille $(x_i)_{i \in I}$ est encore
   algébriquement indépendante : en effet, si on avait un polynôme
-  $P(t,(x_i))$ qui l'annulât, en considérant $P$ comme polynôme de la
-  seule variable $t$ (dont il dépend effectivement, sinon il donnerait
-  une relation de dépendance algébrique sur $k$ entre les $x_i$, chose
-  qui n'existe pas) on contredirait la transcendance de $t$ sur
-  $k(x_i)_{i\in I}$.  Par maximalité de $(x_i)_{i\in I}$, ceci ne peut
-  pas se produire : donc $K$ est bien algébrique sur $k(x_i)_{i\in I}$
-  et $(x_i)_{i\in I}$ est une base de transcendance.
+  $P(t,x_{i_1},\ldots,x_{i_n})$ qui l'annulât, en considérant $P$
+  comme polynôme de la seule variable $t$ (dont il dépend
+  effectivement, sinon il donnerait une relation de dépendance
+  algébrique sur $k$ entre les $x_i$, chose qui n'existe pas) on
+  contredirait la transcendance de $t$ sur $k(x_i)_{i\in I}$.  Par
+  maximalité de $(x_i)_{i\in I}$, ceci ne peut pas se produire : donc
+  $K$ est bien algébrique sur $k(x_i)_{i\in I}$ et $(x_i)_{i\in I}$
+  est une base de transcendance.
 
 (1b) Soit maintenant $(x_i)_{i\in J}$ une famille génératrice (i.e.,
   $K = k(x_i)_{i \in J}$) ou telle que $K$ soit algébrique sur $E =
@@ -684,7 +843,10 @@ dépend pas du choix de celle-ci) s'appelle \textbf{degré de
   transcendance} de $K$ sur $k$ et se note $\degtrans_k(K)$.
 \end{defn}
 
-\begin{prop}
+On remarquera que le degré de transcendance vaut $0$ si et seulement
+si l'extension est algébrique.
+
+\begin{prop}\label{additivity-transcendence-degree}
 Si $k \subseteq K \subseteq L$ est une tour d'extensions, alors
 $\degtrans_k(L) = \degtrans_k(K) + \degtrans_K(L)$.
 \end{prop}
@@ -700,12 +862,83 @@ une relation de dépendance algébrique sur $k$ entre les $x_i$, qui
 n'existe pas non plus, c'est-à-dire plus exactement qu'elle est nulle,
 et ceci montre que la réunion considérée est algébriquement
 indépendante ; d'autre part, $L$ est algébrique sur $K(y_j)$, qui est
-lui-même algébrique sur $k(x_i,y_j)$ car $K$ l'est sur $k(x_i)$
+lui-même algébrique sur $k(x_i)_{i\in I}(y_j)_{j\in J}$ car $K$ l'est
+sur $k(x_i)_{i\in I}$
 (cf. \ref{upgrade-algebraic-with-indeterminates}), donc $L$ est
 algébrique sur $k(x_i,y_j)$
 (cf. \ref{basic-facts-algebraic-extensions}(4)).
 \end{proof}
 
+\begin{prop}\label{push-of-transcendentals}
+Soit $k \subseteq k' \subseteq K$ est une tour d'extensions avec $k'$
+algébrique sur $k$ : alors si $(x_i)_{i\in I}$ est une famille
+d'éléments de $K$ algébriquement indépendants sur $k$, ils le sont
+encore sur $k'$.  De plus, dans ces conditions, toute base de $k'$
+comme $k$-espace vectoriel est encore une base de $k'(x_i)_{i\in I}$
+sur $k(x_i)_{i\in I}$, et notamment, $[k'(x_i)_{i\in I} : k(x_i)_{i\in
+    I}] = [k':k]$.
+\end{prop}
+\begin{proof}
+Montrons la première affirmation.  D'après la définition de
+l'indépendance algébrique d'une famille infinie, il suffit de la
+prouver pour un nombre fini $x_1,\ldots,x_n$ d'éléments.
+
+D'après \ref{transcendence-basis-facts}(1b), on peut extraire
+de $x_1,\ldots,x_n$ une base de transcendance de $k'(x_1,\ldots,x_n)$
+sur $k'$, disons $x_1,\ldots,x_r$.  Ainsi, $k'(x_1,\ldots,x_n)$ est
+algébrique sur $k'(x_1,\ldots,x_r)$ ; or $k'(x_1,\ldots,x_r)$ est
+algébrique sur $k(x_1,\ldots,x_r)$
+(cf. \ref{upgrade-algebraic-with-indeterminates}) ; donc
+$k'(x_1,\ldots,x_n)$, et en particulier $k(x_1,\ldots,x_n)$, est
+algébrique sur $k(x_1,\ldots,x_r)$, ce qui n'est possible que
+pour $n=r$ d'après \ref{transcendence-basis-facts}(3).  Donc
+$x_1,\ldots,x_n$ sont algébriquement indépendants sur $k'$.
+
+(Variante en utilisant \ref{additivity-transcendence-degree} : On a
+$\degtrans_k k'(x_1,\ldots,x_n) = \degtrans_k k(x_1,\ldots,x_n) +
+\degtrans_{k(x_1,\ldots,x_n)} k'(x_1,\ldots,x_n)$, où le premier terme
+vaut $n$ par hypothèse et le second vaut $0$ de nouveau parce que
+$k'(x_1,\ldots,x_n)$ est algébrique sur $k(x_1,\ldots,x_n)$
+(cf. \ref{upgrade-algebraic-with-indeterminates}) : ceci montre
+$\degtrans_k k'(x_1,\ldots,x_n) = n$.  Mais on a aussi $\degtrans_k
+k'(x_1,\ldots,x_n) = \degtrans_k k' + \degtrans_{k'}
+k'(x_1,\ldots,x_n)$, et de nouveau $\degtrans_k k' = 0$ : ceci montre
+$\degtrans_{k'} k'(x_1,\ldots,x_n) = n$.  C'est donc que
+$x_1,\ldots,x_n$ est une base de transcendance de $k'(x_1,\ldots,x_n)$
+(d'après \ref{transcendence-basis-facts} (1b) et (3)).  En
+particulier, $x_1,\ldots,x_n$ sont algébriquement indépendants
+sur $k'$.)
+
+Pour ce qui est de la dernière affirmation, elle découle
+de \ref{linear-disjointness-of-algebraic-and-transcendental} (au moins
+dans le cas d'un nombre fini de $x_i$ ; mais comme tout élément de
+$k(x_i)_{i\in I}$ ou $k(x_i)_{i\in I}$ ne fait intervenir qu'un nombre
+fini des $x_i$, le cas général se ramène au cas fini).
+\end{proof}
+
+\begin{prop}\label{subextension-of-finite-type-is-of-finite-type}
+Si $k \subseteq E \subseteq L$ et si $L$ est de type fini sur $k$
+(i.e., $L = k(x_1,\ldots,x_n)$ pour un nombre fini d'éléments
+$x_1,\ldots,x_n$ de $L$), alors $E$ l'est aussi.
+\end{prop}
+\begin{proof}
+On a vu $\degtrans_k(L) = \degtrans_k(E) + \degtrans_E(L)$ : cette
+quantité étant finie, les deux termes de droite sont finis.  Si
+$t_1,\ldots,t_r$ est une base de transcendance de $E$ sur $k$, quitte
+à remplacer $k$ par $k(t_1,\ldots,t_r)$, on peut supposer $E$
+algébrique sur $k$, et on veut montrer que $E$ est finie sur $k$.
+
+Supposons maintenant $L = k(x_1,\ldots,x_n)$ avec $x_1,\ldots,x_r$ une
+base de transcendance de $L$ sur $k$ (possible, quitte à renuméroter,
+d'après \ref{transcendence-basis-facts}(1b)).  On a $[L :
+  k(x_1,\ldots,x_r)] < \infty$ d'après
+\ref{basic-facts-algebraic-extensions}(1), et en particulier
+$[E(x_1,\ldots,x_r) : k(x_1,\ldots,x_r)] < \infty$.  Or
+d'après \ref{push-of-transcendentals}, $[E(x_1,\ldots,x_r) :
+  k(x_1,\ldots,x_r)] = [E:k]$ : on a bien $[E:k] < \infty$ comme
+annoncé.
+\end{proof}
+
 
 \subsection{Corps de rupture, corps de décomposition, clôture algébrique}
 
-- 
cgit v1.2.3

