Théorème de relèvement
Le théorème de relèvement suivant est un cas particulier du théorème général de relèvement des chemins, appliqué au revêtement du cercle par une droite, vu comme le paramétrage privilégié du cercle unité du plan complexe,
En appelant chemin toute application continue sur l'intervalle réel [0, 1] : Modèle:Énoncé On dit alors que Modèle:Math est un chemin d'origine tModèle:Ind relevant Modèle:Math .
Compléments
- Deux relèvements de Modèle:Math diffèrent d'un multiple entier de Modèle:Math.
- Le résultat s'étend à une application sur un segment réel quelconque (par changement de variable) puis sur un intervalle réel quelconque (par réunion croissante de segments).
- Si Modèle:Math est une application continue d'un intervalle Modèle:Math dans ℂ*, on peut la mettre sous forme polaire en appliquant le théorème à Modèle:Math. On obtient ainsi une application continue θ de Modèle:Math dans ℝ telle queModèle:Retraitet si Modèle:Math est de [[classe de régularité|classe CModèle:Exp]] alors θ aussi.
Démonstration
Cas général
Remarquons d'abord que :
- pour tout point x de [0, 1] et tout réel t tel que Modèle:Math(x) = p(t), il existe un « relèvement local de Modèle:Math » (défini et continu sur un voisinage de x dans [0, 1]) prenant en x la valeur t : il suffit de choisir un voisinage sur lequel Modèle:Math n'atteint pas la valeur –Modèle:Math(x) et d'utiliser que p est un homéomorphisme de ]t – Modèle:Math, t + Modèle:Math[ dans le cercle privé du point –Modèle:Math(x) ;
- si deux relèvements locaux de Modèle:Math, définis respectivement sur deux sous-intervalles JModèle:Ind et JModèle:Ind de [0, 1], coïncident en un point commun, alors leur différence est nulle sur tout l'intervalle JModèle:Ind∩JModèle:Ind d'après le théorème des valeurs intermédiaires, puisqu'elle est nulle en ce point et ne peut prendre pour valeurs que des multiples entiers de Modèle:Math.
L'ensemble J des réels x de [0, 1] pour lesquels Modèle:Math possède sur [0, x] un relèvement d'origine tModèle:Ind est donc un sous-intervalle de [0, 1] de la forme [0, c[ ou [0, c], et Modèle:Math possède sur J un unique relèvement Modèle:Math d'origine tModèle:Ind.
Il reste à montrer que J = [0, 1]. Soit Modèle:Math un relèvement local de Modèle:Math sur un intervalle JModèle:' voisinage de c dans [0, 1]. En un point arbitraire de J∩JModèle:', ce relèvement Modèle:Math, quitte à lui ajouter un multiple adéquat de Modèle:Math, coïncide avec Modèle:Math ; il coïncide alors sur J∩JModèle:', ce qui permet d'étendre Modèle:Math en un relèvement sur J∪JModèle:'. Par maximalité, J contient donc JModèle:'. Par conséquent, J est un voisinage dans [0, 1] de son extrémité c, ce qui prouve que c est égal à 1 et appartient à J.
Si l'application est de classe Ck
On suppose avec . Alors par analyse-synthèse, si , on a nécessairement :, ce qui implique que . On vérifie alors que définit bien un relèvement de et qu'elle est de classe sur .