Fonction de choix, nécessaire ici ?

Homo Topi · June 2022

Dans un fil en algèbre, j'ai écrit ceci.

La situation est la suivante. J'ai un corps $K$ et une extension $L$ de $K$. $L$ est un $K$-espace vectoriel, soit $(e_j)_{j \in J}$ une $K$-base de $L$. Il y a trois situations possibles ici : $J$ peut être fini, infini dénombrable, ou infini indénombrable. J'ai ensuite pris $x \in L$ non nul : "il existe" une combinaison linéaire finie des $e_j$ telle que $x=\displaystyle \sum_{\text{finie}}\alpha_j e_j$ avec les $\alpha_j$ tous non nuls. Maintenant, je veux construire une application $\varphi : L \longrightarrow L$ qui soit $K$-linéaire et telle que $\varphi(x)\neq 0$. Pour ça, je prends un $e_{j_0}$ qui apparait dans la somme finie ci-dessus et je pose $\varphi(e_{j_0})=1$, $\varphi(e_j)=0$ sinon.

Ma question est la suivante : techniquement, j'ai dit "il existe une CL finie" mais l'énoncé précis est qu'il existe une application $f : J \longrightarrow K$, $j \longmapsto \alpha_j$, telle qu'il existe un sous-ensemble $I \subseteq J$ fini tel que $f(j)\neq 0$ pour tout $j \in I$. Il y a beaucoup de "il existe" dans ce bazar. Du coup, je me posais la question, de quel "niveau" d'axiome du choix (choix dénombrable, choix "normal" de ZFC classique, autre ?) ai-je besoin ici pour choisir $j_0$ ? $j_0$ est dans $I$, qui est fini, mais faut-il auparavant utiliser une fonction de choix pour choisir $I$ ? Auquel cas le "niveau" d'axiome du choix nécessaire dépendrait de la cardinalité de $J$ que je mentionnais ci-dessus.

Poirot · June 2022

Aucun choix où que ce soit à partir du moment où tu sais qu'il existe une $K$-base de $L$ (ce que l'on ne sait pas en toute généralité sans l'axiome du choix), et en acceptant que "fini" veut dire "en bijection avec un entier $n = \{0, 1, \dots, n-1\}$".

Par définition d'une telle base, l'application $$(\alpha_j)_{j \in J} \mapsto \sum_{j \in J} \alpha_j e_j,$$ définie sur l'ensemble $K^{(J)}$ des applications de $J$ dans $K$ à support fini et à valeurs dans $L$, est une bijection (linéaire).

Par surjectivité, si $x \in L \setminus \{0\}$, il existe un ensemble fini non vide $I \subset J$ sur lequel $x$ est supporté. $I$ étant fini, une fonction de choix existe dessus car il est tout simplement bien ordonné.

PS. Ta définition de combinaison linéaire finie n'est pas satisfaisante, c'est surtout $f(j) = 0$ pour $j \in J \setminus I$ qu'il faut préciser.

Foys · June 2022

L'axiome du choix est utilisé une fois, dans l'existence d'une base de $L$ comme $K$-espace vectoriel.

Après il ne l'est plus. L'utilisation de théorèmes affirmant l'existence d'un objet particulier se fait de la manière suivante: soit $\Gamma$ une théorie (un ensemble d'énoncés), $P$ un énoncé qu'on souhaite prouver (en supposant tous les énoncés de $\Gamma$). Mais on dispose d'une propriété $F(.)$ telle que $\Gamma$ démontre $\exists x F(x)$. Ce qu'on fait c'est qu'on prend un nouveau nom $\alpha$ (c'est une lettre ne figurant ni dans $\Gamma$ ni dans $P$ ni dans $F$) et qu'on rajoute $F(\alpha)$ dans l'ensemble des axiomes, afin de s'en servir pour démontrer $P$. Autrement dit on établit que $P$ est conséquence de $\Gamma \cup \{F(\alpha)\}$, cela montre que $P$ est conséquence de $\Gamma$ seul.

Le nouveau nom n'a pas d'autre rôle que de désigner l'objet dont on avait dit qu'il existe et satisfait $F(.)$ (et donc doit être distinct des noms déjà en présence pour éviter d'attribuer aux objets qu'ils désignent des propriétés qu'ils n'ont peut-être pas).

Il ne s'agit pas d'axiome du choix mais d'un résultat général de logique (règle "d'élimination du quantificateur existentiel").

Dans ton cas cette règle a été appliquée plusieurs fois:

1°) "soit $e$ une base de $L$ sur $K$". $e$ est une nouvelle lettre (les axiomes de base des maths -dont AC- sous-jacents ici, ne contiennent aucune lettre non liée). Considérons l'énoncé $F_1(x)$ suivant "$x$ est une base de $L$ comme $K$ espace vectoriel". AC entraîne $\exists x F_1(x)$. C'est ici qu'il est utilisé.

2°) Ca c'est complètement implicite mais $e$ est une fonction, donc il existe un ensemble de définition pour elle i.e. $\exists x Dom(e,x)$ avec $Dom(e,x):= \forall t \left [ t \in x \leftrightarrow \exists y (t,y) \in e\right ]$. On prend un nouveau nom $I$ et on ajoute $Dom(e,I)$ à l'ensemble des hypothèses.

Les étapes 1°) et 2°) sont compactées dans la phrase introductive "soit $(e_i)_{ \in I}$ une base de $L$ comme $K-ev$"

3°) "soit $\alpha$ une fonction de $I$ dans $K$ nulle sauf pour un nombre finie de valeurs" ... Par définition comme $e$ est une base, les hypothèses ambiantes (incluant $F_1(e)$) entraînent $\exists y F_2(y)$ où $F_2(y):= y$ est une fonction de $I$ dans $K$ nulle sauf en un nom fini de valeurs et $x:= \sum_{i\in I} y(i) e(i)$. On ajoute un nouveau nom $\alpha$, tel que $F_2(\alpha)$.

4°) On travaille avec l'hypothèse $x \neq 0$. Les hypothèses ambiantes entraînent $\exists z F_3(z)$ avec $F_3(z):= \alpha (z) \neq 0$". On introduit un nouveau nom $j_0$ et on ajoute $F_3(j_0)$ (i.e. $\alpha(j_0)$) aux hypothèses.

NB : "$a_b$" n'est jamais qu'une écriture plus compacte de $a(b)$ quand $a$ est une famille, et une famille est la même chose qu'une fonction.

Homo Topi · June 2022

Poirot a dit :
PS. Ta définition de combinaison linéaire finie n'est pas satisfaisante, c'est surtout $f(j) = 0$ pour $j \in J \setminus I$ qu'il faut préciser.

En effet.

Donc c'est bien la cardinalité de $J$ qui importe ici. Si $J$ est fini, pas d'AC nécessaire, si $J$ est infini dénombrable, AC dénombrable, et si $J$ est indénombrable, AC standard.

@Foys merci, je suppose que ce genre de chose est assez indigeste pour la plupart des gens, mais moi ça m'aide quand c'est présenté comme ça.

Poirot · June 2022

J'ai l'impression que tu ne m'as pas lu, où ai-je parlé de la cardinalité de $J$ ? C'est l'existence de $J$ qui vient de l'axiome du choix en toute généralité, mais une fois celui-ci introduit, il n'y a plus besoin du moindre choix.

Homo Topi · June 2022

Non mais. Justement. Si $L$ est une extension "à base dénombrable", ACD suffirait. Si $L=K[X]$ par exemple. Si $L$ est une extension finie, pas besoin d'axiome. C'est ça que j'ai voulu dire.