Soit $E$ un fibré vectoriel sur un espace analytique $X$. Considérons un modèle formel $(\mathfrak{X},\mathfrak{E})$ de $(X,E)$ : cela signifie que $\mathfrak{X}$ est $k^{\circ}$-schéma formel, plat et localement topologiquement de type fini muni d’un isomorphisme $\mathfrak{X}_{\eta}\simeq X$ et que $\mathfrak{E}$ est un fibré vectoriel sur $\mathfrak{X}$ muni d’un isomorphisme $\mathfrak{E}_{\eta}\simeq E$. On lui associe une métrique PL sur $E$ de la façon suivante.

Soit $(\mathfrak{U}_{i})$ un recouvrement formel de $\mathfrak{X}$ qui trivialise $\mathfrak{E}$ et soit, pour tout $i$, une trivialisation $(e_{1},\dots,e_{n})$ de $\mathfrak{E}|_{\mathfrak{U}_{i}}$. Pour tout $i$, $\mathfrak{U}_{i,\eta}$ est un domaine analytique de $X$.

Pour toute section $s$ de $E$ sur le domaine analytique fermé $\mathfrak{U}_{i,\eta}$ de $X$, il existe une unique famille $(f_{1},\dots,f_{n})$ de fonctions holomorphes sur $\mathfrak{U}_{i,\eta}$ telles que $s=\sum f_{i}e_{i}$, et l’on pose $\mathopen{\|}{s}\mathclose{\|}=\max(\mathopen{|}{f_{1}}\mathclose{|},\dots,\mathopen{|}{f_{n}}\mathclose{|})$ ; c’est une fonction continue.

Si $(e^{\prime}_{1},\dots,e^{\prime}_{n})$ est une autre trivialisation de $\mathfrak{E}|_{\mathfrak{U}_{i}}$, il existe une matrice inversible $A\in\operatorname{GL}_{n}(\mathfrak{U}_{i})$ telles que $(e_{1},\dots,e_{n})=(e^{\prime}_{1},\dots,e^{\prime}_{n})\cdot A$. Si $s=\sum f_{i}e_{i}=\sum f^{\prime}_{i}e^{\prime}_{i}$, cela entraîne la relation $(f^{\prime}_{1},\dots,f^{\prime}_{n})^{\mathrm{t}}=A(f_{1},\dots,f_{n})^{\mathrm{t}}$. Pour tout point $x\in\mathfrak{U}_{i,\eta}$, $\mathopen{\|}{A(x)}\mathclose{\|}=\mathopen{\|}{A^{-1}(x)}\mathclose{\|}=1$, si bien que l’on a $\max(\mathopen{|}{f_{i}}\mathclose{|})=\max(\mathopen{|}{f^{\prime}_{i}}\mathclose{|})$. Il en résulte que la définition donnée de $\mathopen{\|}{s}\mathclose{\|}$ ne dépend pas du choix de la trivialisation $(e_{1},\dots,e_{n})$.

Cela entraîne aussi que ces différentes prescriptions coïncident sur les domaines analytiques $\mathfrak{U}_{i,\eta}\cap\mathfrak{U}_{j,\eta}$, d’où un morphisme de faisceau de $E$ dans l’espace des fonctions à valeurs réelles sur $X$.

Comme les domaines $\mathfrak{U}_{i,\eta}$ forment un G-recouvrement de $X$, tout point de $X$ possède un voisinage qui est réunion finie de certains de ces $\mathfrak{U}_{i,\eta}$. Par suite, l’image de ce morphisme est contenu dans le faisceau $\mathscr{C}^{0}_{X_{G}}$.

C’est une métrique PL sur $E$. De telles métriques seront appelées formelles.