% !TEX encoding =  UTF-8 Unicode

% \documentclass[dvips,twoside] {article}
% \usepackage[a5paper,layoutwidth=148mm,layoutheight=7.77817in,outer=10mm,inner=35bp,tmargin=10mm,bmargin=10mm,footskip=15bp]{geometry}

\documentclass[12pt,twoside,a4paper]{article}
\usepackage[a4paper,layoutwidth=210mm,layoutheight=11in,margin=121pt]{geometry}
%----- ceci retrecit les marges format  A4---------
\marginparwidth 0pt
\oddsidemargin  0cm
\evensidemargin  0cm
\marginparsep 0pt
\topmargin -1.5cm
\textwidth 16cm
\textheight 25.5cm
\sloppy
%-----------------------------------

\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage[bookmarksopen=false,breaklinks=true,%
backref=page,pagebackref=true,plainpages=false,%
hyperindex=true,pdfstartview=FitH,colorlinks=true,%
pdfpagelabels=true,linkcolor=blue,%
citecolor=red,urlcolor=red,hypertexnames=false%
]%
{hyperref}

\usepackage{doi}
% \usepackage{mathrsfs}
\usepackage{mathtools}
% \usepackage{stmaryrd}
% \usepackage[all]{xy}
% \usepackage{makeidx}
\usepackage{natbib}
\bibpunct (),.{},
\usepackage[british]{babel}
%\usepackage{bm}
\usepackage{xspace}

\usepackage{etoolbox}
\makeatletter\def\th@plain{\slshape}
\patchcmd{\th@remark}{\itshape}{\slshape}{}{}\makeatother

\newcounter{bidon}
\newcommand{\rdb}{\refstepcounter{bidon}}

% \newcommand{\di}{\,\vert\,}
% \newcommand{\ndi}{\nmid}%{{\not\vert}\;}


% \newcommand \nzr {\neq 0}
% \newcommand{\Vr}{\mathrm{Vr}}
% \newcommand{\Rn}{\mathrm{Rn}}
% \newcommand{\Nvr}{\mathrm{Nvr}}
% \newcommand{\Nrn}{\mathrm{Nrn}}
% \newcommand{\U}{\mathrm{Un}}

% \newcommand{\Gati}{\Gat\cup\so\infty }

%: générateurs
% \newcommand \Rzero {R_{=0}}
% \newcommand \Rnz {R_{\nzr}}
% \newcommand \Rvr {R_{\Vr}}
% \newcommand \Ru {R_{\U}}
% \newcommand \Rrn {R_{\Rn}}
% \newcommand \Rnrn {R_{\Nrn}}
% \newcommand \Rnvr {R_{\Nvr}}

%: ensembles engendrés
% \newcommand \zg {{\ZZ[G]}}
% \newcommand \Izero {{\cI}_{=0}}
% \newcommand \Mnz {{\cM}_{\nzr}}
% \newcommand \Mpos {{\cM}_{\Pos}}
% \newcommand \Cnng {{\cC}_{\Nng}}
% \newcommand \Irn {{\cI}_{\Rn}}
% \newcommand \Vvr {{\cV}_{\Vr}}
% \newcommand \Mu {{\cM}_{\U}}
% \newcommand \abg {{\rm Ab}(G)}
% \newcommand \Hzero {{\cH}_{=0}}

%: \vdg et autres

% \usepackage{stixgras}
% \RequirePackage{amsbsy}

% \newcommand\Exists{\boldsymbol{\stixexists}}
% \newcommand\Forall{\boldsymbol{\stixforall}}
% \newcommand\VDash{\boldsymbol{\stixvdash}}
% \newcommand\Land{\boldsymbol{\stixwedge}}
% \newcommand\Lor{\boldsymbol{\stixvee}}
% \newcommand\Top{\boldsymbol{\stixtop}}
% \newcommand\Bot{\boldsymbol{\stixbot}}
% \newcommand\bigLand{\boldsymbol{\stixbigwedge}}
% \newcommand\bigLor{\boldsymbol{\stixbigvee}}

% \newcommand\dotminus{\stixdotminus}

% \newcommand \vdg{\VDash}
% \newcommand \Vd {\,\vdg}
% \newcommand \vd {\,\,\vdg}
% \newcommand \vii{\Land}
% \newcommand \vuu{\Lor}
% \newcommand \vdi[1] {\mathrel{\,\,\vdg_{#1}}}
% \newcommand \Vii{\bigLand}
% \newcommand \Vuu{\bigLor}

%!TEX encoding =  UTF-8 Unicode
%!TEX root = E-LHM.tex 

%-------- newtheorem ----------


\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem*{theoremcinqtrois}{Theorem 6.3}
% \newtheorem{thdef}[theorem]{Theorem and definition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{conj}[theorem]{Conjecture}
% \newtheorem{proposition}[theorem]{Proposition}
% \newtheorem{propdef}[theorem]{Proposition and definition}
% \newtheorem{plcc}[theorem]{Concrete local-global principle}
% \newtheorem{fact}[theorem]{Fact}
% \newtheorem{vastf}[theorem]{Formal \vst}
% \newtheorem{vast}[theorem]{\vst}
% \newtheorem{valsatz}[theorem]{\vst}
% \newtheorem{precision}[theorem]{Precision}
% \newtheorem{convention}[theorem]{Convention}


% \newtheorem{theoremc}[theorem]{Theorem\etoz}
% \newtheorem{lemmac}{Lemma\etoz}
% \newtheorem{corollaryc}{Corollairy\etoz}
% \newtheorem{propositionc}{Proposition\etoz}
% \newtheorem{factc}{Fait\etoz}
% \newtheorem{propdefc}[theorem]{Proposition and definition\etoz}

%\newtheorem{atheorem}{Theorem}
%\newtheorem{alemma}{Lemma}
%\newtheorem{acorollary}{Corollary}
%\newtheorem{aproposition}{Proposition}
%\newtheorem{apropdef}{Proposition and definition}
%\newtheorem{afact}{Fact}
% \newtheorem*{Principleofcoveringbyquotients}{Principle of covering by quotients}


\theoremstyle{definition}
% \newtheorem{note}[theorem]{Note}
% \newtheorem{context}[theorem]{Context}
\newtheorem{comment}[theorem]{Comment}
% \newtheorem{definition}[theorem]{Definition}
\newtheorem{remark}[theorem]{Remark}
\newtheorem{example}[theorem]{Example}
% \newtheorem{definitions}[theorem]{Definitions}
% \newtheorem{descri}[theorem]{Description}
% \newtheorem{notation}[theorem]{Notation}
% \newtheorem{definota}[theorem]{Definition and notation} 
% \newtheorem{problem}[theorem]{Problem}
% \newtheorem{question}[theorem]{Question}
% \newtheorem{ter}[theorem]{Terminology}

% \theoremstyle{remark}
% \newtheorem{notes}[theorem]{Notes}%[section]
% \newtheorem{remarks}[theorem]{Remarks}
% \newtheorem{comment}[theorem]{Comment}
% \newtheorem{comments}[theorem]{Comments}
% \newtheorem{examples}[theorem]{Examples}





% \usepackage[commandnameprefix=ifneeded,deletedmarkup=xout]{changes}







% \newcommand \Glio {\MA{\mathsf{Liog}}}

% \newcommand{\vou}{\MA{\tsbf{ or }}}
% \newcommand{\Vou}{\MA{\tsbf{OR}}}
% \newcommand \EXists[1] {\tsbf{Introduce }{#1}\tsbf{ such that }\,}
% \newcommand \vet {{\tsbf{,}}\,}
% \newcommand \Atcl {\mathrm{Clat}}
% \newcommand \Atclv {\mathrm{VClat}}
% \newcommand \tcl {\mathrm{Clt}}
% \newcommand \Tcl {\tcl}

% %:  Commentaires, remarques, exemples, problemes
% \newcommand\comm{\rdb
% \noi{\sl Comment. }}

% \newcommand\COM[1]{\rdb
% \noi{\sl Comment #1. }}

% \newcommand\comms{\rdb
% \noi{\sl Comments. }}

% \newcommand\Pb{\rdb
% \noi{\bf Problem. }}

% \newcommand \rem{\rdb
% \noi{\sl Remark. }}

% \newcommand \REM[1]{\rdb
% \noi{\sl Remark #1. }}

% \newcommand \rems{\rdb
% \noi{\sl Remarks. }}

% \newcommand \exl{\rdb
% \noi{\bf Example. }}

% \newcommand \EXL[1]{\rdb
% \noi{\bf Example #1. }}

% \newcommand \exls{\rdb
% \noi{\bf Examples. }}

% \newcommand\Subsubsection[1]{
% \rdb\addcontentsline{toc}{subsubsection}{#1} \subsubsection*{#1}}

% \newcommand\Subsection[1]{
% \rdb\addcontentsline{toc}{subsection}{#1} \subsection*{#1}}

% \newcommand\Section[1]{
% \rdb\addcontentsline{toc}{section}{#1} \section*{#1}}

% \renewcommand\paragraph[1]{

% \medskip \noindent $\bullet$ \textbf{#1}}


% \newcommand\gui[1]{``{#1}''}

% \newcommand \thref[1] {Theorem~\ref{#1}}
% \newcommand \paref[1] {page~\pageref{#1}}
% \newcommand \pstfref[1] {Positivstellensatz formel~\ref{#1}}
% \newcommand \pstref[1] {Positivstellensatz~\ref{#1}}

% \newcommand \num {{n$^{\mathrm{ o}}$}}
% %\newcommand \num {{n\o}}


% \newcommand\subsubsec[1] {\subsubsection*{#1}}

% % ----  ssi  etc  
% \newcommand \recu {induction\xspace}
% \newcommand \hdr {induction hypothesis\xspace}
% \newcommand \ssi {if and only if\xspace}
% \newcommand \cnes {necessary and sufficient condition\xspace}
% \newcommand \spdg {without loss of generality\xspace}
% \newcommand \Propeq {T.f.a.e.\xspace}
% \newcommand \propeq {t.f.a.e.\xspace}
% \newcommand \disept {17$^{th}$ Hilbert's problem\xspace}


% \newcommand \cad {i.e.\ }
% \newcommand \Cad {I.e.\ }
% %\newcommand \wlog {w.l.o.g.\/}



% %------- abr\'eviations math\'ematiques courantes ---

% \newcommand \Amo {$\gA$-module\xspace}
% \newcommand \Amos {$\gA$-modules\xspace}

% \newcommand \Bmo {$\gB$-module\xspace}
% \newcommand \Bmos {$\gB$-modules\xspace}

% \newcommand \kmo {$\gk$-module\xspace}
% \newcommand \kmos {$\gk$-modules\xspace}

% \newcommand \Kmo {$\gK$-module\xspace}
% \newcommand \Kmos {$\gK$-modules\xspace}

% \newcommand \Lmo {$\gL$-module\xspace}
% \newcommand \Lmos {$\gL$-modules\xspace}

% \newcommand \Vmo {$\gV$-module\xspace}
% \newcommand \Vmos {$\gV$-modules\xspace}


% \newcommand \Zmo {$\gZ$-module\xspace}
% \newcommand \Zmos {$\gZ$-modules\xspace}

% \newcommand \ZZmo {$\ZZ$-module\xspace}
% \newcommand \ZZmos {$\ZZ$-modules\xspace}


% \newcommand \Ali {$\gA$-\ali}
% \newcommand \Alis {$\gA$-\alis}

% \newcommand \Bli {$\gB$-\ali}
% \newcommand \Blis {$\gB$-\alis}

% \newcommand \Cli {$\gC$-\ali}
% \newcommand \Clis {$\gC$-\alis}


% \newcommand \Alg {$\gA$-\alg}
% \newcommand \Algs {$\gA$-\algs}

% \newcommand \Blg {$\gB$-\alg}
% \newcommand \Blgs {$\gB$-\algs}

% \newcommand \Clg {$\gC$-\alg}
% \newcommand \Clgs {$\gC$-\algs}

% \newcommand \klg {$\gk$-\alg}
% \newcommand \klgs {$\gk$-\algs}


% \newcommand \Klg {$\gK$-\alg}
% \newcommand \Klgs {$\gK$-\algs}

% \newcommand \Llg {$\gL$-\alg}
% \newcommand \Llgs {$\gL$-\algs}

% \newcommand \Vlg {$\gV$-\alg}
% \newcommand \Vlgs {$\gV$-\algs}



% \newcommand \kev {$\gk$-vector space\xspace}
% \newcommand \kevs {$\gk$-vector spaces\xspace}

% \newcommand \Kev {$\gK$-vector space\xspace}
% \newcommand \Kevs {$\gK$-vector spaces\xspace}


% \newcommand \Kli {$\gK$-\ali}
% \newcommand \Klis {$\gK$-\alis}


% %: a
% \newcommand \ac {algebraically closed\xspace}
% \newcommand \alc {\agq closure\xspace}

% \newcommand \adv {valuation domain\xspace}
% \newcommand \advs {valuation domains\xspace}

% \newcommand \advl {domain with divisors\xspace} %anneaux à diviseurs
% \newcommand \advls {domains with divisors\xspace} 

% \newcommand \advd {discrete valuation ring\xspace}
% \newcommand \advds {discrete valuation rings\xspace}

% \newcommand \agq {algebraic\xspace}

% \newcommand \alg {algebra\xspace}
% \newcommand \algs {algebras\xspace}

% \newcommand \alge {étale \alg}
% \newcommand \alges {étale \algs}

% \newcommand \agB {Boolean \alg}

% \newcommand \algo{algorithm\xspace}
% \newcommand \algos{algorithms\xspace}

% \newcommand \algq{algorithmic\xspace}

% \newcommand \alo {local ring\xspace}
% \newcommand \alos {local rings\xspace}

% \newcommand \aloh {henselian \alo}
% \newcommand \alohs {henselian \alos}

% \newcommand \ali {\lin map\xspace}
% \newcommand \alis {\lin maps\xspace}

% \newcommand \alrd {\dcd \alo}
% \newcommand \alrds {\dcd \alos}


% \newcommand \anar {\ari \ri}
% \newcommand \anars {\ari \ris}
% \newcommand \Anars {\Ari \ris}

% \newcommand \ari{arithmetic\xspace}

% \newcommand \arv {valuation ring\xspace}
% \newcommand \arvs {valuation rings\xspace}

% \newcommand \auto {automorphism\xspace}
% \newcommand \autos {automorphisms\xspace}

% %: c

% \newcommand \cac {algebraically closed field\xspace}
% \newcommand \cacs {algebraically closed fields\xspace}

% \newcommand \cara{characteristic\xspace}  
% \newcommand \caras{characteristics\xspace}  

% \newcommand \carn{characterisation\xspace}  
% \newcommand \carns{characterisations\xspace}

% \newcommand \cdf{field of fractions\xspace}

% \newcommand \cdH{Hensel code\xspace}
% \newcommand \cdHs{Hensel codes\xspace}
  

% \newcommand \cdi{discrete field\xspace}  
% \newcommand \cdis{discrete fields\xspace}  

% \newcommand \cdr{field of roots\xspace}

% \newcommand \cdv{variables change\xspace}  
% \newcommand \cdvs{variables changes\xspace}  
% \newcommand \cdvu{homogeneous \cdv}  
% \newcommand \cdvus{homogeneous \cdvs}  

% \newcommand \cli{integral closure\xspace}  
% \newcommand \clis{integral closures\xspace}  

% \newcommand \codi {discrete ordered field\xspace}
% \newcommand \codis {discrete ordered fields\xspace}

% \newcommand \coe {coefficient\xspace}
% \newcommand \coes {coefficients\xspace}

% \newcommand \cof {\cov}

% \newcommand \coh {coherent\xspace}

% \newcommand \coli {linear combination\xspace}
% \newcommand \colis {linear combinations\xspace}

% \newcommand \colo {local \cou}
% \newcommand \colos {local \cous}

% \newcommand \com {comaximal\xspace}

% \newcommand \coo {coordinate\xspace}
% \newcommand \coos {coordinates\xspace}

% \newcommand \cop {complementary\xspace}

% \newcommand \cosv {conservative\xspace}

% \newcommand \cou {pair\xspace}
% \newcommand \couh {henselian \cou}
% \newcommand \cous {pairs\xspace}
% \newcommand \couhs {henselian \cous}

% \newcommand \crdl {residual field\xspace}

% \newcommand \crl {corollary\xspace}
% \newcommand \crls {corollaries\xspace}


% \newcommand \cval{valued field\xspace}
% \newcommand \cvals{valued fields\xspace}

% \newcommand \cvar{valuated field\xspace}
% \newcommand \cvars{valuated fields\xspace}

% \newcommand \cvard{valuated discrete field\xspace}
% \newcommand \cvards{valuated discrete fields\xspace}

% \newcommand \cvd {valued discrete field\xspace}
% \newcommand \cvds {valued discrete fields\xspace}

% \newcommand \cvdh {henselian \cvd}
% \newcommand \cvdhs {henselian \cvds}

% \newcommand \cvdsc {separably closed valued discrete field\xspace}
% \newcommand \cvdscs {separably closed valued discrete fields\xspace}

% \newcommand \cvdac {algebraicalle closed valued discrete field\xspace}
% \newcommand \cvdacs {algebraicalle closed valued discrete fields\xspace}

% \newcommand \cvdu{\ultm \cvard}
% \newcommand \cvdus{\ultm \cvards}

% \newcommand \cvu{\ultm \cvar}
% \newcommand \cvus{\ultm \cvars}


% %: d

% \newcommand \dcd {residually discrete\xspace}

% \newcommand \ddp {Pr\"ufer domain\xspace}
% \newcommand \ddps {Pr\"ufer domains\xspace}

% \newcommand \ddk {Krull dimension\xspace}

% \newcommand \demo {proof\xspace}
% \newcommand \dems {proofs\xspace}
% \newcommand \demos {\dems}

% \newcommand \deter {determinant\xspace}
% \newcommand \deters {determinants\xspace}


% \newcommand \dfn{definition\xspace}  
% \newcommand \Dfn{Definition\xspace}  
% \newcommand \Dfns{Definitions\xspace}  
% \newcommand \dfns{definitions\xspace}  

% \newcommand \dil{differential\xspace}  
% \newcommand \diles{differentials\xspace}  

% \newcommand \dij{disjunctive\xspace}

% \newcommand \dimm {immediate description\xspace}
% \newcommand \dimms {immediate descriptions\xspace}

% \newcommand \discri{discriminant\xspace}
% \newcommand \discris{discriminants\xspace}

% \newcommand \dok {Dedekind domain\xspace}
% \newcommand \doks {Dedekind domains\xspace}

% \newcommand \dve {divisibility\xspace}

% \newcommand \dvz {zerodivisor\xspace}
% \newcommand \dvzs {zerodivisors\xspace}

% %: e
% \newcommand \eco{\com \elts}  

% \newcommand \egmt{also\xspace} 

% \newcommand \egt{equality\xspace} 
% \newcommand \egts{equalities\xspace} 

% \newcommand \elr{elementary\xspace}  

% \newcommand \elt{element\xspace}  
% \newcommand \elts{elements\xspace}  

% \def \endo {endomorphism\xspace}
% \def \endos {endomorphisms\xspace}

% \newcommand \entrel {entailment relation\xspace}
% \newcommand \entrels {entailment relations\xspace}

% \newcommand \eqn  {equation\xspace}
% \newcommand \eqns  {equations\xspace}

% \newcommand \eqv  {equivalent\xspace}

% \newcommand \eqvc  {equivalence\xspace}
% \newcommand \eqvcs  {equivalences\xspace}

% \newcommand \eseq{essentially equivalent\xspace} 
% \newcommand \Eseq{Essentially equivalent\xspace} 

% \newcommand \esid{essentially identical\xspace} 
% \newcommand \Esid{Essentially identical\xspace} 

% \newcommand \evc{vector space\xspace} 
% \newcommand \evcs{vector spaces\xspace} 

% %: f

% \newcommand \fab {bounded \fcn}
% \newcommand \fabs {bounded \fcns}

% %\newcommand \fac {total \fcn}

% \newcommand \facile{\begin{proof}
% Left to the reader.
% \end{proof}}


% \newcommand \fap {partial \fcn}
% \newcommand \faps {partial \fcns}

% \newcommand \fat {total \fcn}

% \newcommand \fcn {factorisation\xspace}
% \newcommand \fcns {factorisations\xspace}

% \newcommand \fdi{strongly discrete\xspace} 

% \newcommand \fit {faithfully\xspace}
% \newcommand \fpt {\fit flat\xspace}

% \newcommand \fmt {formellement\xspace}

% \newcommand \flw {following\xspace}

% %: g

% \newcommand\gmq{geometric\xspace}

% \newcommand\gne{generalised\xspace}

% \newcommand\gnl{general\xspace}

% \newcommand\gnlt{generally\xspace}

% \newcommand\gnn{generalisation\xspace}
% \newcommand\gnns{generalisations\xspace}

% \newcommand\gnq{generic\xspace}

% \newcommand\gnr{generalise\xspace}  

% \newcommand\grl{$\ell$-group\xspace}
% \newcommand\grls{$\ell$-groups\xspace}

% \newcommand \gtr{generator\xspace}  
% \newcommand \gtrs{generators\xspace}  

% %: h i

% \newcommand \homo {homomorphism\xspace}
% \newcommand \homos {homomorphisms\xspace}

% \newcommand \icl {integrally closed\xspace}

% \newcommand \id {ideal\xspace}
% \newcommand \ids {ideals\xspace}

% \newcommand \idd {determinantal \id}
% \newcommand \idds {determinantal \ids}

% \newcommand \idema {maximal \id}
% \newcommand \idemas {maximal \ids}

% \newcommand \idep {prime \id}
% \newcommand \ideps {prime \ids}

% \newcommand \idemi {minimal prime\xspace}
% \newcommand \idemis {minimal primes\xspace}

% \newcommand \idf {Fitting \id}
% \newcommand \idfs {Fitting \ids}

% \newcommand \idm {idempotent\xspace}
% \newcommand \idms {idempotents\xspace}

% \newcommand \idp {principal \id}
% \newcommand \idps {principal \ids}

% \newcommand \idtr {indeterminate\xspace}
% \newcommand \idtrs {indeterminates\xspace}

% \newcommand \ifr {fractional \id}
% \newcommand \ifrs {fractional \ids}

% \newcommand \inteq {intuitively \eqv}

% \newcommand \ird {irreducible\xspace}

% \newcommand \itf {\tf \id}
% \newcommand \itfs {\tf \ids}

% \newcommand \iso {isomorphism\xspace}
% \newcommand \isos {isomorphisms\xspace}

% \newcommand \iv {invertible\xspace}

% %: l
% \newcommand \lec {reader\xspace}
% \newcommand \llec {the reader\xspace}

% \newcommand \lgb {local global\xspace}

% \newcommand \LHe {Hensel Lemma\xspace}
% \newcommand \lHe {Hensel lemma\xspace}
% %\newcommand \lHes {Hensel Lemmas\xspace}
% \newcommand \LHm {Multivariate \LHe}
% %\newcommand \lHM {multivariate \LHe}
% %\newcommand \lHm {multivariate \lHe}


% \newcommand \lin {linear\xspace}

% \newcommand \lint {linearly\xspace}

% \newcommand \lon {localisation\xspace}
% \newcommand \lons {localisations\xspace}

% \newcommand \lop {\lot principal\xspace}

% \newcommand \losd {\lsdz}
% \newcommand \lsdz {\lot \sdz\xspace}

% \def \lot {locally\xspace}

% %: m
% \newcommand \mlp {principal \lon matrix\xspace}
% \newcommand \mlps {principal \lon matrices\xspace}

% \newcommand \mnp {manipulation\xspace}
% \newcommand \mnps {manipulations\xspace}
% \newcommand \mnr {\elr \mnp}
% \newcommand \mnrs {\elr \mnps}

% \newcommand \mo {monoid\xspace}
% \newcommand \mos {monoids\xspace}
% \newcommand \moco {\com \mos}

% \newcommand \mpf {\pf module\xspace}
% \newcommand \mpfs {\pf modules\xspace}

% \newcommand \mpn {\pn matrix\xspace}
% \newcommand \mpns {\pn matrices\xspace}

% \newcommand \mpr {\pro module\xspace}
% \newcommand \mprs {\pro modules\xspace}

% \newcommand \mprn {\prn matrix\xspace}
% \newcommand \mprns {\prn matrices\xspace}

% \newcommand \mptf {\ptf module\xspace}
% \newcommand \mptfs {\ptf modules\xspace}

% \newcommand \mrc {projective module of constant rank\xspace}
% \newcommand \mrcs {projective modules of constant rank\xspace}

% %: n

% \newcommand \ncr{necessary\xspace}

% \newcommand \ncrt{necessarily\xspace}

% \newcommand \ndz {regular\xspace}

% \newcommand \noe {noetherian\xspace}
% \newcommand \noco {\noe\coh}

% \newcommand \nst {Nullstellensatz\xspace}
% \newcommand \nsts {Nullstellens\"atze\xspace}

% \newcommand \odz {Zariski open set\xspace}

% \newcommand \oqc {\qc open set\xspace}
% \newcommand \oqcs {\qc open sets\xspace}

% \newcommand \ort {orthogonal\xspace}

% %: p

% \newcommand \pa {saturated pair\xspace}
% \newcommand \pas {saturated pairs\xspace}

% \newcommand \pb{problem\xspace}  
% \newcommand \pbs{problems\xspace}

% \newcommand \peq {purely equational\xspace}
  

% \newcommand \pf {finitely presented\xspace}

% \newcommand \pgn {Newton polygon\xspace}
% \newcommand \pgns {Newton polygons\xspace}

% \newcommand \plg {\lgb principle\xspace}
% \newcommand \plgs {\lgb principles\xspace}

% \newcommand \pn {presentation\xspace}
% \newcommand \pns {presentations\xspace}

% \newcommand \pol {polynomial\xspace}
% \newcommand \pols {polynomials\xspace}

% \newcommand \polcar {characteristic \pol}
% \newcommand \polcars {characteristic \pols}

% \newcommand \polH {Hensel \pol}
% \newcommand \polHs {Hensel \pols}

% \newcommand \polmin {minimal \pol}
% \newcommand \polmins {minimal \pols}

% \newcommand \poll {polynomial\xspace}
% \newcommand \Poll {Polynomial\xspace}

% \newcommand \polu {monic \pol}
% \newcommand \polus {monic \pols}

% \newcommand \prc {rank constant \pro}

% \newcommand \prmt {precisely\xspace}
% \newcommand \Prmt {Precisely\xspace}

% \newcommand \prn {projection\xspace}
% \newcommand \prns {projections\xspace}

% \newcommand \pro {projective\xspace}

% \newcommand \proi {potential prime\xspace}
% \newcommand \prois {potential primes\xspace}

% \newcommand \proc {potential chain\xspace}
% \newcommand \procs {potential chains\xspace}

% \newcommand \proel {elementary \proc}
% \newcommand \proels {elementary \procs}
% \newcommand \proelo {\proel of length }
% \newcommand \proelos {\proels of length }

% \newcommand \prolo {\proc of length }
% \newcommand \prolos {\procs of length }

% \newcommand \prt {property\xspace}
% \newcommand \prts {properties\xspace}

% \newcommand \pst {Positivstellensatz\xspace}
% \newcommand \psts {Positivstellens\"atze\xspace}

% \newcommand \ptf {\tf \pro}

% %: q

% \newcommand \qc {quasi-compact\xspace}

% \newcommand \qi {quasi integral\xspace}
% \newcommand \qiri {pp-ring\xspace}
% \newcommand \qiris {pp-rings\xspace}

% \newcommand \ralg {Horn rule\xspace}
% \newcommand \ralgs {Horn rules\xspace}

% \newcommand \rcf {real closed field\xspace}
% \newcommand \rcfs {real closed fields\xspace}

% \newcommand \rdl {linear dependance relation\xspace}
% \newcommand \rdls {linear dependance relations\xspace}

% \newcommand \rdi {integral dependance relation\xspace}
% \newcommand \rdis {integral dependance relations\xspace}

% \newcommand \rdij {\dij rule\xspace}
% \newcommand \rdijs {\dij rules\xspace}

% \newcommand \rdv {valuative divisibility relation\xspace}
% \newcommand \rdvs {valuative divisibility relations\xspace}

% \newcommand \rdy {dynamical rule\xspace}
% \newcommand \rdys {dynamical rules\xspace}

% \newcommand \red {direct rule\xspace}
% \newcommand \reds {direct rules\xspace}

% \newcommand \rex {existential rule\xspace}
% \newcommand \rexs {existential rules\xspace}

% \newcommand \ri {ring\xspace}
% \newcommand \ris {rings\xspace}

% %: s

% \newcommand \sad {dynamical algebraic structure\xspace}
% \newcommand \sads {dynamical algebraic structures\xspace}
% \newcommand \SAD {Dynamical algebraic structure\xspace}
% \newcommand \SADs {Dynamical algebraic structures\xspace}

% \newcommand \salg {algebraic structure\xspace}
% \newcommand \salgs {algebraic structures\xspace}

% \newcommand \sdz {without \dvz}

% \newcommand \sfio {fundamental system of orthogonal idempotents\xspace}

% \newcommand \sgr {\gtr set\xspace}%{generator \sys}
% \newcommand \sgrs {\gtr sets\xspace}%{generator \syss}

% \newcommand \sli {\lin \sys}
% \newcommand \slis {\lin \syss}

% \newcommand \spb {separable\xspace}
% \newcommand \spl {separable\xspace}

% \newcommand \sps {spectral space\xspace}
% \newcommand \spss {spectral spaces\xspace}

% \newcommand \ste {strictly étale\xspace}

% \newcommand \stf {strictly finite\xspace}

% \newcommand \sul {direct factor\xspace}

% \newcommand \Syp {\Poll \sys}
% \newcommand \sype {étale \syp}
% \newcommand \sypes {étale \syps}
% \newcommand \syp {\poll \sys}
% \newcommand \syps {\poll \syss}

% \newcommand \sys {system\xspace}
% \newcommand \syss {systems\xspace}

% \newcommand \sysN {Newton \syp}
% \newcommand \SysN {Newton \syp}
% \newcommand \sysNs {Newton \syps}

% \newcommand \sysNe {étale Newton \sys}
% \newcommand \sysNes {étale Newton \syss}

% %: t
% \newcommand \talg {Horn theory\xspace}
% \newcommand \talgs {Horn theories\xspace}

% \newcommand \tco {coherent theory\xspace}
% \newcommand \tcos {coherent theories\xspace}

% \newcommand \tdij {\dij theory\xspace}
% \newcommand \tdijs {\dij theories\xspace}

% \newcommand \Tdy {dynamical theory\xspace}
% \newcommand \tdy {dynamical theory\xspace}
% \newcommand \tdys {dynamical theories\xspace}

% \newcommand \tel {regular theory\xspace}
% \newcommand \tels {regular theories\xspace}

% \newcommand \telri {cartesian theory\xspace}
% \newcommand \telris {cartesian theories\xspace}

% \newcommand \tf {finitely generated\xspace}

% \newcommand \tfo {formal theory\xspace}
% \newcommand \tfos {theory formelles\xspace}

% \newcommand \tgm {\gmq theory\xspace}
% \newcommand \tgms {\gmq theories\xspace}

% \newcommand \Tho {Theorem\xspace}
% \newcommand \Thos {Theorems\xspace}
% \newcommand \tho {theorem\xspace}
% \newcommand \thos {theorems\xspace}

% \newcommand \tpe {purely equational theory\xspace}
% \newcommand \tpes {purely equational theories\xspace}

% \newcommand \trdi {distributive lattice\xspace}
% \newcommand \trdis {distributive lattices\xspace}


% %: u

% \newcommand \ultm {ultrametric\xspace}

% \newcommand \unt {monic\xspace}

% \newcommand \uvl {universal\xspace}

% \newcommand \vala {absolute value\xspace}
% \newcommand \valas {absolute values\xspace}

% \newcommand \valn {valuation\xspace}
% \newcommand \valns {valuations\xspace}

% \newcommand \valu {\ultm \vala}
% \newcommand \valus {\ultm \valas}

% \newcommand \vfn {verification\xspace}
% \newcommand \vfns {verifications\xspace}

% \newcommand \vmd {vector \umd}
% \newcommand \vmds {vectors \umds}


% \newcommand \vst {Valuativstellensatz\xspace}
% \newcommand \vsts {Valuativstellensätze\xspace}

% \newcommand \vstf {formal \vst}
% \newcommand \vstfs {formal \vsts}

% %: z

% \newcommand \zeH {Hensel zero\xspace}
% \newcommand \zeHs {Hensel zeroes\xspace}

% \newcommand \zed {zero-dimensional\xspace}
% \newcommand \zedr {zero-dimensional reduced\xspace}


% \newcommand \zmt {\tho de Zariski-Grothen\-dieck\xspace}


% %:  ------- maths constructives


% \newcommand \cov {constructive\xspace}

% \newcommand \coma {\cov \maths}
% \newcommand \clama {classical \maths}

% \renewcommand \cot {constructively\xspace}

% \newcommand \mathe {mathematical\xspace}
% \newcommand \maths {mathematics\xspace}

% \newcommand \matn {mathematician\xspace}

% \newcommand \pte {excluded middle principle\xspace}

% \newcommand \prco {\cov proof\xspace}
% \newcommand \prcos {constructive proofs\xspace}

% \newcommand \tcg {compactness theorem\xspace}
% \newcommand \Tcgi {The \tcg implies the following result. }
% %


% \newcommand {\junk}[1]{}

% \newcommand\rouge[1]{\textcolor{red}{#1}}
% \newcommand\bleu[1]{\textcolor{blue}{#1}}
% \newcommand\violet[1]{\textcolor{magenta}{#1}}


% %%%%%%%%%% Cadre
% \newcommand{\Cadre}[2]{%

% \medskip%
% \newskip\oldleftskip
% \newskip\oldrightskip
% \oldleftskip=\leftskip%
% \oldrightskip=\rightskip%
% \leftskip=-\tabcolsep%
% \rightskip=-\tabcolsep%
% \begin{center}\fbox{%
% \begin{tabular}%
% {p{#1\textwidth}}
% \setlength{\parindent}{5mm}%
% \vspace{-1.5mm}#2\vspace{1mm}%
% \end{tabular}}\end{center}\par\medskip%
% \leftskip=\oldleftskip%
% \rightskip=\oldrightskip%
% \setlength{\parindent}{6mm}}

% %\newcommand \cm{cm}

% \newcommand\boite[2]{\begin{minipage}[c]{#1cm}
%      \centering {#2} \end{minipage}}
% \newcommand\Boite[3]{\parbox[t][#1cm][c]{#2cm}{\boite{#2}{#3}}}


% %%%%%%%%%% Encadre
% \newcommand{\Encadre}[1]{\Cadre{.8}{#1}}

% %%%%%%%%%% Cencadre
% \newcommand{\Cencadre}[1]{\Encadre{\vspace{-3mm}
% \begin{center}
% #1 \end{center}\vspace{-8mm}}}

% \newcommand{\cen}{\centerline}
% %:  Grandcadre
% \newcommand \Grandcadre[1]{%
% \begin{center}
% \begin{tabular}{|c|}
% \hline
% ~\\[-3mm]
% #1\\[-3mm]
% ~\\
% \hline
% \end{tabular}
% \end{center}}

% \newcommand\dsp{\displaystyle}
\newcommand\ndsp{\textstyle}

% \newcommand{\eop}{\hfill \mbox{$\Box$}}

%------- med skip et autres ---------
% \newcommand \noi {\noindent}
\renewcommand \ss {\smallskip}
% \newcommand \sni {\ss\noi}
% \newcommand \snii {\noi}
% \newcommand \ms {\medskip}
% \newcommand \mni {\ms\noi}
% \newcommand \bs {\bigskip}
% \newcommand \bni {\bs\noi}
% \newcommand \hs {\qquad}
% \newcommand \alb {\allowbreak}
% \newcommand \ce {\centerline}

%:  Exists
%\newcommand \Exists {\rotatebox[origin=c]{180}{\tsbf{E}}\hspace{.1em}}
%\newcommand \Bot {\rotatebox[origin=c]{180}{\tsbf{T}}\hspace{.1em}}
%\newcommand \Top {{\tsbf{T}}\hspace{.1em}}

%:  leqslant
\renewcommand \le{\leqslant}
\renewcommand \leq{\leqslant}
\renewcommand \preceq{\preccurlyeq}
\renewcommand \ge{\geqslant}
\renewcommand \geq{\geqslant}
\renewcommand \succeq{\succcurlyeq}
% \newcommand   \nneq {\mathrel{\#}}
% \newcommand   \ineq {$_{\,\mathrel{\#}}$}

%\newcommand\tim{^\times}
\newcommand\eti{^\times}
% \newcommand \epr{^\perp}
\newcommand \etl{^*}
% \newcommand \sta{^\star}
% \newcommand \bu {{$\bullet$}}
% \newcommand \bl {^\bullet}
% \newcommand{\bul}{^{\bullet}}
%\newcommand \cir {^\circ}
% \newcommand \eci {^\circ}
% \newcommand \uci{\mathring}
% \newcommand \ep[1]{^{(#1)}}
% \newcommand \esh{^\sharp}
% \newcommand \efl{^\flat}
% \newcommand \eto{$^*$ }
% \newcommand \etoz{$^*$}
% \newcommand \ist{_\star}

% \newcommand \Ast {\gA^{\!\star}}
% \newcommand \Bst {\gB^{\star}}
% \newcommand \iBA {_{\gB/\!\gA}}
% \newcommand \iWV {_{\gW\!/\gV}}
% \newcommand \Bo{\BB\mathrm{o}}
\newcommand \Ati {\gA^{\!\times}}
% \newcommand \Bti {\gB^{\times}}
% \newcommand \Vti {\gV^{\times}}
% \newcommand \Atl {\gA^{\!*}}
% \newcommand \Btl {\gB^{*}}
% \newcommand \Ktl {\gK^{*}}
% \newcommand{\KAt}{\gK\etl\!\sur{\Ati}}
% \newcommand{\AAt}{\Atl\!\sur{\Ati}}

% \newcommand \divi {\mid}


% \newcommand\equidef{\buildrel{{\rm def}}\over{\;\Longleftrightarrow\;}}
% \newcommand\eqdef{\buildrel{\rm def}\over {\;=\;}}
% \newcommand\eqdefi{\buildrel{\rm def}\over {\;=\;}}

%------- formules a parametres --------

% \newcommand \fraC[2] {{{#1}\over {#2}}}
% \newcommand \formule[1]{{\left\{ {\arraycolsep2pt\begin{array}{lll} #1 \end{array}}\right.}}
% \newcommand \formul[1]{{\left\{ {\arraycolsep2pt\begin{array}{rcl} #1 \end{array}}\right.}}
\newcommand \formu[1]{{\arraycolsep2pt\begin{array}{rcl} #1 \end{array}}}

% \newcommand\mapright[1]{\smash{\mathop{\longrightarrow}\limits^{#1}}}
% \newcommand\maprightto[1]{\smash{\mathop{\longmapsto}\limits^{#1}}}
% \newcommand\mapdown[1]{\downarrow\rlap{$\vcenter{\hbox{$\scriptstyle
% #1$}}$}}
% %\newcommand\Land#1{\buildrel{#1}\over \&}
% \newcommand{\pref}[1]{\textup{\hbox{\normalfont(\ref{#1})}}}

% \newcommand \abs[1] {\left|{#1}\right|}
%\newcommand \norm[1] {\left\parallel{#1}\right\parallel}
% \newcommand \abS[1] {\big|{#1}\big|}
\newcommand \aqo[2] {#1\sur{\gen{#2}}\!}
% \newcommand \aQo[2] {#1/{\gEn{#2}}\!}
% \newcommand \Aqo[2] {#1\sur{\big\langle{#2}\big\rangle}\!}
% \newcommand \Al[1] {\Vi^{\!#1}}
% \newcommand \ci[1] {{{#1}^\circ}}
% \newcommand \crac[2] {\cro {\frac{#1}{#2}}}
% \newcommand \cro[1] {\left[#1\right]}
% \newcommand \eqdf[1] {\buildrel{#1}\over =}
% \newcommand \equivdf[1] {\buildrel{#1}\over \longleftrightarrow}
% \newcommand \frt[1] {\!\left|_{#1}\right.\!}
% \newcommand \impdef[1] {\buildrel{#1}\over \Longrightarrow}
% \newcommand \norme[1]{\left\lVert #1 \right\rVert}
% \newcommand \Norme[1]{\big\lVert #1 \big\rVert}
% \newcommand \tra[1] {{\,^{\rm t}\!#1}}
\newcommand \gen[1] {\left\langle{#1}\right\rangle}
% \newcommand \gEn[1] {\langle{#1}\rangle}
% \newcommand \geN[1] {\big\langle{#1}\big\rangle}
% %\newcommand\rh[1][]{\mathrel{{\rhd}_{#1}}}
% \newcommand \sing[1] {\left\{{#1}\right\}}
\newcommand \so[1] {\left\{\,{#1}\, \right\}}
% \newcommand \soo[1] {\{\,{#1}\,\}}
% \newcommand \sO[1]{\big\{{#1}\big\}}
\newcommand \sotq[2]{\so{\,#1\,\vert\,#2\,}}
% %\newcommand \sotQ[2]{\sO{\,#1\;\big\vert\;#2\,}}
% \newcommand \sotq[2]{\so{#1\mathrel{;}#2}}
% \newcommand \sootq[2]{\soo{#1\mathrel{;}#2}}
% \newcommand \sotQ[2]{\sO{#1\mathrel{;}#2}}
\newcommand \sur[1] {\!\left/#1\right.}
% \newcommand \und[1] {\underline{#1}}

% \newcommand \Sqr {\mathrm{Sqr}}

% \newcommand \idg[1] {|\,#1\,|}
% \newcommand \idG[1] {\big|\,#1\,\big|}

% \newcommand \norm[1] {\Vert\,#1\,\Vert}

% % dimension d'une extension
% \newcommand \dex[1] {[\,#1\,]}
% \newcommand \deX[1] {\big[\,#1\,\big]}

% % liste
% \newcommand \lst[1] {[\,#1\,]}
% \newcommand \lsT[1] {\big[\,#1\,\big]}


% %:   fleches longues
% \newcommand{\mt}{\mapsto}

% \newcommand{\llongrightarrow}{\relbar\joinrel\mkern-1mu\longrightarrow}
% \newcommand{\lllongrightarrow}{\relbar\joinrel\mkern-1mu\llongrightarrow}
% \newcommand{\llllongrightarrow}{\relbar\joinrel\mkern-1mu\lllongrightarrow}
% \newcommand\simarrow{\vers{_\sim}}
% \newcommand\isosim{\buildrel{_\sim}\over \longleftrightarrow }
% \newcommand\vers[1]{\buildrel{#1}\over \longrightarrow }
% \newcommand\vvers[1]{\buildrel{#1}\over \llongrightarrow }
% \newcommand\vvvers[1]{\buildrel{#1}\over \lllongrightarrow }
% \newcommand \lora {\longrightarrow}
% \newcommand \llra {\llongrightarrow}
% \newcommand \lllra {\lllongrightarrow}

% %:  leqslant
\renewcommand \leq{\leqslant}
\renewcommand \geq{\geqslant}

\newcommand \som {\sum\nolimits}
% \newcommand \Ex {{\exists}}
% \newcommand \Tt {{\forall}}
% \newcommand \te {\otimes}
% \newcommand \vep{{\varepsilon}}


%:  macros \`a parametres


% \newcommand\lra[1]{\langle{#1}\rangle}
% \newcommand\lrb[1] {\llbracket #1 \rrbracket}
% \newcommand\lrbd {\lrb{1..d}}
% \newcommand\lrbn {\lrb{1..n}}
% \newcommand\lrbl {\lrb{1..\ell}}
% \newcommand\lrbm {\lrb{1..m}}
% \newcommand\lrbk {\lrb{1..k}}
% \newcommand\lrbp {\lrb{1..p}}
% \newcommand\lrbq {\lrb{1..q}}
% \newcommand\lrbr {\lrb{1..r}}
% \newcommand\lrbs {\lrb{1..s}}

%\newcommand \vdg {\mathrel{\vrule height6.94444pt width1pt\vrule height3.97222pt width5.11111pt depth-2.97222pt}}
% en 10pt
%\newcommand \vdg {\mathrel{\vrule height8.33333pt width1pt\vrule height4.66667pt width6.33333pt depth-3.66667pt}} % en 12pt
%\newcommand \vd {\,\,\vdg\,\,}
%\newcommand \vdi {\,\,\MA{\vdg}}

% \newcommand \vda {\,\vdash\,}

% \newcommand \vdw {\,\vdash_w\,}

\newcommand\Aq[2]{#1_{[#2]}}
\newcommand\Aqj[2]{#1_{\{#2\}}}

% %\newcommand \im {\rightarrow} % fleche des treillis implicatifs
% \newcommand \dar[1] {\MA{\downarrow \!#1}}
% \newcommand \uar[1] {\MA{\uparrow \!#1}}
% \newcommand \clps[1] {{\downarrow #1\,\downarrow}}

% \newcommand\tsbf[1]{\textsf{\textbf{\textup{#1}}}}
% \newcommand\lab[1]{\item[\tsbf{#1}]}
% \newcommand\Lab[1]{\rdb\item[\tsbf{#1}]\label{Ax#1}}
% \newcommand\Tsbf[1]{\hyperref[Ax#1]{\tsbf{#1}}}

% %:  mathpzc  \DeclareMathAlphabet{\mathpzc}{OT1}{pzc}{m}{it}
% %\newcommand\sa[1]{\hbox{\large\usefont{T1}{pzc}{m}{it}#1}\,}
% %\newcommand\sab[1]{\hbox{\large\usefont{T1}{pzc}{m}{it}#1}\,\,}
% \newcommand\SA[1]{\rdb\sa{#1}\label{theorie#1}}
% \newcommand\Sa[1]{\hyperref[theorie#1]{\sa{#1}}}
% \newcommand\sa[1]{\hbox{\usefont{T1}{pzc}{m}{it}#1}\,}
% \newcommand\sab[1]{\hbox{\usefont{T1}{pzc}{m}{it}#1}\,\,}
% \newcommand\sA[1]{\hbox{\small\usefont{T1}{pzc}{m}{it}#1}\,}
% \newcommand\sAb[1]{\hbox{\small\usefont{T1}{pzc}{m}{it}#1}\,\,}



% \newcommand \snic[1] {\sni\centerline{$#1$}

% \ss}

% \newcommand \snac[1]{\sni
% {\small\centering$#1$\par}

% \ss}

\newcommand \eoe {\hbox{}\nobreak\hfill
\vrule width .5em height .5em depth 0mm \par \smallskip}

%\newcommand \rF[1]{\MA{{\rm F}_{\!#1}}}
%\newcommand \rR[1]{\MA{{\rm R}_{#1}}}
%\newcommand \rRs[1]{\MA{\Rs_{#1}}}

% \newcommand \bal[1] {^\rK_{#1}}
% \newcommand \ul[1] {_\rK^{#1}}


% \newcommand \ov[1] {\overline{#1}}


% \newcommand \wh[1] {\widehat{#1} }
% \newcommand \wi[1] {\widetilde{#1} }

% \newcommand\dessus[2]{{\textstyle {#1} \atop \textstyle {#2}}}

% \newcommand\carray[2]{{\left[\begin{array}{#1} #2 \end{array}\right]}}
% \newcommand\cmatrix[1]{\left[\matrix{#1}\right]}
% \newcommand\clmatrix[1]{{\left[\begin{array}{lllllll} #1 \end{array}\right]}}
% \newcommand\dmatrix[1]{\abs{\matrix{#1}}}
% \newcommand\Cmatrix[2]{\setlength{\arraycolsep}{#1}\left[\matrix{#2}\right]}
% \newcommand\Dmatrix[2]{\setlength{\arraycolsep}{#1}\left|\matrix{#2}\right|}

% \newcommand \bloc[4]{\left[
% \begin{array}{cc}
% #1 & #2   \\
% #3 & #4
% \end{array}
% \right]}

% \newcommand \cm{em}

% \newcommand{\blocs}[8]{%
% {\setlength{\unitlength}{.0833\textwidth}
% \tabcolsep0pt\renewcommand{\arraystretch}{0}%
% \begin{tabular}{|c|c|}
% \hline
% \parbox[t][#3\cm][c]{#1\cm}{\begin{minipage}[c]{#1\cm}
% \centering#5
% \end{minipage}}&
% \parbox[t][#3\cm][c]{#2\cm}{\begin{minipage}[c]{#2\cm}
% \centering#6
% \end{minipage}}\\
% \hline
% \parbox[t][#4\cm][c]{#1\cm}{\begin{minipage}[c]{#1\cm}
% \centering#7
% \end{minipage}}&
% \parbox[t][#4\cm][c]{#2\cm}{\begin{minipage}[c]{#2\cm}
% \centering#8
% \end{minipage}}\\
% \hline
% \end{tabular}
% }}

% \newcommand \UneCol[1]{%
% \sni\mbox{\hspace{.02\textwidth}%
% \parbox[t]{.98\textwidth}{#1}%
% }}

% \newcommand \Unecol[1]{%
% \sni\mbox{\hspace{.1\textwidth}%
% \parbox[t]{.9\textwidth}{#1}%
% }}

% \newcommand \Deuxcol[4]{%
% \sni\mbox{\parbox[t]{#1\textwidth}{#3}%
% \hspace{.05\textwidth}%
% \parbox[t]{#2\textwidth}{#4}}}

% \newcommand \DeuxCol[2]{%
% \Deuxcol{.475}{.475}{#1}{#2}}

% \newcommand \DeuxCols[2]{%
% \sni\mbox{\hspace{.02\textwidth}%
% \parbox[t]{.475\textwidth}{#1}%
% \hspace{.03\textwidth}%
% \parbox[t]{.475\textwidth}{#2}}}

% \newcommand \DeuxRegles[2]{%
% \vspace{-1em}\DeuxCols
% {\begin{enumerate}  #1
% \end{enumerate}
% }
% {\begin{enumerate}  #2
% \end{enumerate}
% }
% \vspace{-.3em}
% }

% \newcommand \UneRegle[2]{%
% \vspace{-1em}\UneCol{
% \begin{enumerate}
% \lab{#1}{#2}
% \end{enumerate}
% }
% \vspace{-.3em}
% }

% \newcommand \Regles[1]{%
% \vspace{-1em}\UneCol{
% \begin{enumerate}
% {#1}
% \end{enumerate}
% }
% \vspace{-.3em}
% }

% \newcommand \regles[1]{%
% \vspace{-1em}\Unecol{
% \begin{enumerate}
% {#1}
% \end{enumerate}
% }
% \vspace{-.3em}
% }

% \newcommand \itbu {\item[$\bullet$]}
% \newcommand \labu {\lab{$\bullet$}}

% \newcommand \Deuxbu[2]{%
% \vspace{-.6em}\DeuxCols
% {\begin{itemize}  #1
% \end{itemize}}
% {\begin{itemize}  #2
% \end{itemize}}}


% %: revdots
% \makeatletter
% \def\revddots{\mathinner{\mkern1mu\raise\p@
% \vbox{\kern7\p@\hbox{.}}\mkern2mu
% \raise4\p@\hbox{.}\mkern2mu\raise7\p@\hbox{.}\mkern1mu}}
% \makeatother

%------- lettres formatees --------
%: standards maths
% \newcommand \BB{\mathbb {B}}
% \newcommand \CC{\mathbb {C}}
% \newcommand \FF{\mathbb {F}}
% \newcommand \II{\mathbb {I}}
% \newcommand \KK{\mathbb {K}}
% \newcommand \MM{\mathbb {M}}
\newcommand \NN{\mathbb {N}}
% \newcommand \ZZ{\mathbb {Z}}
% \newcommand \OO{\mathbb {O}}
% \newcommand \PP{\mathbb {P}}
% \newcommand \QQ{\mathbb {Q}}
% \newcommand \RR{\mathbb {R}}




%: gras math
% \newcommand \gk {\mathbf{k}}
% \newcommand \gkb {\ov\gk}
% \newcommand \gl {\mathbf{l}}
\newcommand \gA {\mathbf{A}}
\newcommand \gB {\mathbf{B}}
\newcommand \gC {\mathbf{C}}
% \newcommand \gD {\mathbf{D}}
% \newcommand \gd {\mathbf{d}}
% \newcommand \gDd {\mathbf{Dd}}
% \newcommand \gE {\mathbf{E}}
% \newcommand \gF {\mathbf{F}}
% \newcommand \gG {\mathbf{G}}
% \newcommand \gI {\mathbf{I}}
% \newcommand \gIo {\mathbf{Io}}
\newcommand \gK {\mathbf{K}}
% \newcommand \gKb {\ov\gK}
% \newcommand \gAh {\widehat\gA}
\newcommand \gKh {\widehat\gK}
\newcommand \gVh {\widehat\gV}
% \newcommand \gKt {\widetilde\gK}
\newcommand \rhe {^{\mathrm{h}}}
\newcommand \rHe {^{\mathrm{H}}}
% \newcommand \rNe {^{\mathrm{N}}}
% \newcommand \rhs {^{\mathrm{hs}}}
\newcommand \Khe {\gK\rhe}
\newcommand \KHe {\gK\rHe}
\newcommand \gV {\mathbf{V}}
\newcommand \Vhe {\gV\rhe}
\newcommand \VHe {\gV\rHe}

\newcommand \gL {\mathbf{L}}

\newcommand \fmhe {\fm\rhe}
\newcommand \fmHe {\fm\rHe}
\newcommand \mhe {\fmhe}
\newcommand \mHe {\fmHe}

\newcommand \Ahe {\gA\!\rhe}


\newcommand \KV {(\gK,\gV)}

\newcommand \gW {\mathbf{W}}

\newcommand \Kac {{\gK^\mathrm{ac}}}

\newcommand \Vac {{\gV^\mathrm{ac}}}





% %:     SCO  (suites complementaires)
% \newdimen\xyrowsp
% \xyrowsp=3pt
% \newcommand{\SCO}[6]{
% \xymatrix @R = \xyrowsp {
%                                   &1 \ar@{-}[dl] \ar@{-}[dr] \\
% #3 \ar@{-}[ddr]                   &   & #6 \ar@{-}[ddl] \\
%                                   &\bullet\ar@{-}[d] \\
%                                   &\bullet   \\
% #2 \ar@{-}[ddr] \ar@{-}[uur]      &   & #5 \ar@{-}[ddl] \ar@{-}[uul] \\
%                                   &\bullet \ar@{-}[d] \\
%                                   &\bullet  \\
% #1 \ar@{-}[uur]                   &   & #4 \ar@{-}[uul] \\
%                                   & 0 \ar@{-}[ul] \ar@{-}[ur] \\
% }
% }

% %:  mots mathematiques rm
% \newcommand \Adj {\MA{\mathrm{Adj}}}
% \newcommand \adj {\MA{\mathrm{adj}}}
% \newcommand \Adu {\MA{\mathrm{Adu}}}
\newcommand \Ann {\mathrm{Ann}}
% \newcommand \Atom {\mathrm{Atom}}
% \newcommand \Aut {\MA{\mathrm{Aut}}}
% \newcommand \BZ {\MA{\mathrm{BZ}}}
% \newcommand \car {\MA{\mathrm{car}}}
% \newcommand \Cl {\MA{\mathrm{Cl}}}
% \newcommand \ClW {\MA{\mathrm{Cl}_{\mathrm{W}}}}
% \newcommand \Coker {\MA{\mathrm{Coker}}}
% \newcommand \Cont{\mathrm{Co}}
% \newcommand \Dc {\MA{\mathrm{Dc}}}
% \newcommand \DDiv {\MA{\mathrm{Dv}}}
\renewcommand \det {\MA{\mathrm{det}}}
\renewcommand \deg {\MA{\mathrm{deg}}}
% \newcommand \Diag {\MA{\mathrm{Diag}}}
%
%\newcommand \di {\MA{\mathrm{di}}}
\newcommand \disc {\MA{\mathrm{disc}}}
\newcommand \Disc {\MA{\mathrm{Disc}}}
\newcommand \Div {\MA{\mathrm{Div}}}
\newcommand \DivA {\Div\gA }
\newcommand \DivAp {(\Div\gA)^{+} }
\newcommand \DivB {\Div\gB }
\newcommand \DivBp {(\Div\gB)^{+} }
\newcommand \DkM {\MA{\mathrm{DkM}}}
\newcommand \dv {\MA{\mathrm{div}} }
\newcommand \dvA {\dv_\gA }
\newcommand \dvB {\dv_\gB }
\newcommand \ev {{\mathrm{ev}}}
\newcommand \End {\MA{\mathrm{End}}}
\newcommand \fsac {\MA{\mathrm{fsa}}}
\newcommand \Fix {\MA{\mathrm{Fix}}}
\newcommand \Frac {\MA{\mathrm{Frac}}}
\newcommand \Gal {\MA{\mathrm{Gal}}}
\newcommand \Gfr {\MA{\mathrm{Gfr}}}
\newcommand \Gr {\MA{\mathrm{Gr}}}
\newcommand \gr {\MA{\mathrm{gr}}}
\newcommand \Gram {\MA{\mathrm{Gram}}}
\newcommand \gram {\MA{\mathrm{gram}}}
\newcommand \Grl {\MA{\mathrm{Grl}}}
\newcommand \hauteur {\mathrm{hauteur}}
\newcommand \Hom {\MA{\mathrm{Hom}}}
\newcommand \Id {\MA{\mathrm{Id}}}
\newcommand \Iv {\MA{\mathrm{Iv}}}
\newcommand \I {\mathrm{I}}
\newcommand \Idif {\MA{\mathrm{Idif}}}
\newcommand \Idv {\MA{\mathrm{Idv}}}
\newcommand \Ifr {\MA{\mathrm{Ifr}}}
\newcommand \Icl {\MA{\mathrm{Icl}}}
\renewcommand \Im {\MA{\mathrm{Im}}}
\newcommand \Inf {\MA{\mathrm{Inf}}}
\newcommand \Itf {\MA{\mathrm{Itf}}}
\newcommand \Ker {\MA{\mathrm{Ker}}}
%\newcommand \KR {{\MA{\mathrm{Kr}}}}
\newcommand \Lst {\MA{\mathrm{Lst}}}
\newcommand \LIN {\mathrm{Lin}}
\newcommand \Lsf {\MA{\mathrm{Lsf}}}
\newcommand \Mat {\MA{\mathrm{Mat}}}
\newcommand \Mip {\mathrm{Min}}
\newcommand \md {\mathrm{md}}
\newcommand \Mgcd {\MA{\mathrm{Mgcd}}}
%:\renewcommand \mod
\renewcommand \mod {\;\mathrm{mod}\;}
\newcommand \Mor {\MA{\mathrm{Mor}}}
\newcommand \NDc {\MA{\mathrm{NDc}}}
\newcommand \poids {\mathrm{poids}}
\newcommand \poles {\hbox {\rm p\^oles}}
\newcommand \pgcd {\MA{\mathrm{pgcd}}}
\newcommand \ppcm {\MA{\mathrm{ppcm}}}
%\newcommand \Pr {\MA{\mathrm{Pr}}}
\newcommand \Rad {\MA{\mathrm{Rad}}}
\newcommand \Reg {\MA{\mathrm{Reg}}}
%\newcommand \Rn {\MA{\mathrm{Rn}}}
\newcommand \rg{\MA{\mathrm{rg}}}
\newcommand \rgst {\mathrm{rgst}}
\newcommand \Res {\mathrm{Res}}
\newcommand \Rs {\MA{\mathrm{Rs}}}
\newcommand \rPr{\MA{\mathrm{Pr}}}
\newcommand \Rv {\mathrm{Rv}}
\newcommand \Sli {\MA{\mathrm{Sli}}}
\newcommand \Som {\MA{\mathrm{Som}}}
\newcommand \Sup {\MA{\mathrm{Sup}}}
\newcommand \Sace {\MA{\mathrm{Sace}}}
\newcommand \Smtf {\MA{\mathrm{Smtf}}}
\newcommand \Stp {\MA{\mathrm{Stp}}}
\newcommand \St {\mathrm{St}}
\newcommand \Tri {\MA{\mathrm{Tri}}}
\newcommand \Tor {\MA{\mathrm{Tor}}}
\newcommand \tr {\MA{\mathrm{tr}}}
\newcommand \Tr {\MA{\mathrm{Tr}}}
\newcommand \Tsc {\MA{\mathrm{Tsch}}}
\newcommand \Um {\MA{\mathrm{Um}}}
\newcommand \val {\MA{\mathrm{val}}}

\newcommand \SIPD {\MA{\mathrm{SIPD}}}
\newcommand \ARC {\MA{\mathrm{ARC}}}
\newcommand \AFR {\MA{\mathrm{AFR}}}
\newcommand \AFRRV {\MA{\mathrm{AFRRV}}}
\newcommand \AFRNZ {\MA{\mathrm{AFRNZ}}}
\newcommand \PPM {\MA{\mathrm{PPM}}}
\newcommand \PB {\MA{\mathrm{PB}}}

\newcommand \Suslin{{\rm Suslin}}
\newcommand{\DBxk}{{\Der \gk\gB\xi}}%
\newcommand{\DAxk}{{\Der \gk\gA\xi}}%
\newcommand{\DkXxk}{{\Der \gk\kuX\xi}}%
\newcommand \DAbul {\rD_{\!\Abul}}


%:  MA
\newcommand\MA[1]{\mathop{#1}\nolimits}

%:   mots mathematiques  sf
\newcommand \sfa {\mathsf{a}}
\newcommand \sfb {\mathsf{b}}
\newcommand \sfc {\mathsf{c}}
\newcommand \sfd {\mathsf{d}}
\newcommand \sfe {\mathsf{e}}
\newcommand \sff {\mathsf{f}}
\newcommand \sfx {\mathsf{x}}
\newcommand \sfy {\mathsf{y}}
\newcommand \sfz {\mathsf{z}}
\newcommand \sbv {\tsbf{v}}
\newcommand \sbw {\tsbf{w}}
\newcommand \sfv {\mathsf{v}}
\newcommand \sfu {\mathsf{u}}
\newcommand \sft {\mathsf{t}}
\newcommand \sfw {\mathsf{w}}

\newcommand \Cdim {\MA{\mathsf{Cdim}}}
\newcommand \Divdim {\MA{\mathsf{Divdim}}}
\newcommand \Glo {\MA{\mathsf{Glo}}}
\newcommand \GK {\MA{\mathsf{GK}}}
\newcommand \GKO {\MA{\mathsf{GK}_0}}
\newcommand \HO {\MA{\mathsf{H}_0}}
\newcommand \HOp {\MA{\mathsf{H}_0^+}}
\newcommand \Hdim {\MA{\mathsf{Hdim}}}
\newcommand \HeA {{\Heit\gA}}
\newcommand \Heit {\MA{\mathsf{Heit}}}
%\newcommand \Hom {\MA{\mathsf{Hom}}}
\newcommand \Hspec {\MA{\mathsf{Hspec}}}
\newcommand \Jdim {\MA{\mathsf{Jdim}}}
\newcommand \jdim {\MA{\mathsf{jdim}}}
\newcommand \Jspec {\MA{\mathsf{Jspec}}}
\newcommand \jspec {\MA{\mathsf{jspec}}}
\newcommand \KO {\MA{\mathsf{K}_0}}
\newcommand \KOp {\MA{\mathsf{K}_0^+}}
\newcommand \KTO {\wi{\mathsf{K}}_0}
\newcommand \Kdim {\MA{\mathsf{Kdim}}}
\newcommand \Lin {\mathsf{L}}
\newcommand \Max {\MA{\mathsf{Max}}}
\newcommand \Min {\MA{\mathsf{Min}}}
\newcommand \OQC {\MA{\mathsf{Oqc}}}
\newcommand \Pic {\MA{\mathsf{Pic}}}
\newcommand \Reel {\MA{\mathsf{Reel}}}
\newcommand \Spec {\MA{\mathsf{Spec}}}
\newcommand \Speclin {\MA{\mathsf{Speclin}}}
\newcommand \Spv {\MA{\mathsf{Spv}}}
\newcommand \Spev {\MA{\mathsf{Spev}}}
\newcommand \Sper {\MA{\mathsf{Sper}}}
\newcommand \Val {\MA{\mathsf{Val}}}
\newcommand \Valp {\MA{\mathsf{Val'}}}
\newcommand \SpecA {\Spec\gA}
\newcommand \SpevA {\Spev\gA}
\newcommand \SpvA {\Spv\gA}
\newcommand \SperA {\Sper\gA}
\newcommand \SpecT {\Spec\gT}
\newcommand \Zar {\MA{\mathsf{Zar}}}
\newcommand \ZF {\MA{\mathsf{ZF}}}
\newcommand \ValA {{\Val\gA}}
\newcommand \ValpA {{\Valp\gA}}
\newcommand \ZarA {{\Zar\gA}}



%: calligraphique
\newcommand \cA {{\cal A}}
\newcommand \cB {{\cal B}}
\newcommand \cC {{\cal C}}
\newcommand \cD {{\cal D}}
\newcommand \cI {{\cal I}}
\newcommand \cJ {{\cal J}}
\newcommand \cF {{\cal F}}
\newcommand \cH {{\cal H}}
\newcommand \cK {{\cal K}}
\newcommand \cL {{\cal L}}
\newcommand \cM {{\cal M}}
\newcommand \cN {{\cal N}}
\newcommand \cP {{\cal P}}
\newcommand \cQ {{\cal Q}}
\newcommand \cR {{\cal R}}
\newcommand \cS {{\cal S}}
\newcommand \cT {{\cal T}}
\newcommand \cV {{\cal V}}

\newcommand \ccd{\mathcal{CD}}
\newcommand \cco{\mathcal{CO}}


\newcommand \Cin{C^{\infty}}

\newcommand \SK {\cS^\rK}
\newcommand \IK {\cI^\rK}
\newcommand \JK {\cJ^\rK}
\newcommand \IH {\cI\rHe}
\newcommand \JH {\cJ\rHe}


%: roman
%\newcommand \JAC {\mathrm{JAC}}
\newcommand \JAC {J}
\newcommand \Jac {\mathrm{Jac}}
\newcommand \rc {\mathrm{c}}
\newcommand \Df {\MA{\mathrm{Df}}}
\newcommand \Dfr {\MA{\mathrm{Df}}^\mathrm{R}}
\newcommand \Dfmc {\MA{\mathrm{Dfmc}}}
\newcommand \rd {\mathrm{d}}
\newcommand \rv {\mathrm{v}}
\newcommand \rI {\mathrm{I}}
\newcommand \Ic {\mathrm{Ic}}
\newcommand \rC {\mathrm{C}}
\newcommand \rD {\mathrm{D}}
\newcommand \rF {\mathrm{F}}
\newcommand \rG {\mathrm{G}}
\newcommand \rH {\mathrm{H}}
\newcommand \rJ {\mathrm{J}}
\newcommand \Li {\MA{\mathrm{Li}}}
\newcommand \rK {\mathrm{K}}
\newcommand \rL {\mathrm{L}}
\newcommand \Mc {\mathrm{Mc}}
\newcommand \rN {\mathrm{N}}
\newcommand \rP {\mathrm{P}}
\newcommand \rR {\mathrm{R}}
\newcommand \rmSa {\MA{\mathrm{Sa}}}
\newcommand \rmSamc {\MA{\mathrm{Samc}}}
\newcommand \rS {\mathrm{S}}
\newcommand \rU {\mathrm{U}}
\newcommand \rV {\mathrm{V}}
\newcommand \DA {\rD_{\!\gA}}
\newcommand \JA {\rJ_\gA}
\newcommand \JT {\rJ_\gT}


%: gothique
\newcommand\fa{\mathfrak{a}}
\newcommand\fb{\mathfrak{b}}
\newcommand\fc{\mathfrak{c}}
\newcommand\fA{\mathfrak{A}}
\newcommand\fB{\mathfrak{B}}
\newcommand\fD{\mathfrak{D}}
\newcommand\fI{\mathfrak{i}}
\newcommand\fII{\mathfrak{I}}
\newcommand\fj{\mathfrak{j}}
\newcommand\fJ{\mathfrak{J}}
\newcommand\fF{\mathfrak{F}}
\newcommand\ff{\mathfrak{f}}
\newcommand\ffg{\mathfrak{g}}
\newcommand\fG{\mathfrak{G}}
\newcommand\fh{\mathfrak{h}}
\newcommand\fl{\mathfrak{l}}
\newcommand\fm{\mathfrak{m}}
\newcommand\mV{{\fm_\gV}}
\newcommand\mW{{\fm_\gW}}
\newcommand\fM{\mathfrak{M}}
\newcommand\fp{\mathfrak{p}}
\newcommand\fP{\mathfrak{P}}
\newcommand\fq{\mathfrak{q}}
\newcommand\fU{\mathfrak{U}}
\newcommand\fV{\mathfrak{V}}
\newcommand\fx{\mathfrak{x}}
\newcommand\fy{\mathfrak{y}}

%:  mathscr  \usepackage{mathrsfs}
\newcommand \scC{\mathscr{C}}
\newcommand \scR{\mathscr{R}}




% %:  gras math avec \bm
% \newcommand{\bma}{\bm{a}}
% \newcommand{\bmb}{\bm{b}}
% \newcommand{\bmc}{\bm{c}}
% \newcommand{\bmd}{\bm{d}}
% \newcommand{\bme}{\bm{e}}
% \newcommand{\bmf}{\bm{f}}
% \newcommand{\bmu}{\bm{u}}
% \newcommand{\bmv}{\bm{v}}
% \newcommand{\bmw}{\bm{w}}
% \newcommand{\bmy}{\bm{y}}
% \newcommand{\bmx}{\bm{x}}
% \newcommand{\bmz}{\bm{z}}

% \newcommand \LLPO {\tsbf{LLPO}}
% \newcommand \LPO  {\tsbf{LPO}}


% % anneaux, ideaux, ...
% \newcommand \Zg {{\Z[G]}}

% %: treillis distributifs
% \newcommand \vu {\vee} % sup
% \newcommand \vi {\wedge} % inf
% %\newcommand \vii {\hbox{\,{\footnotesize $\bm{\wedge}$}\,}}
% %\newcommand \vuu {\hbox{\,{\footnotesize $\bm{\vee}$}\,}}
% \newcommand \Vu {\bigvee}
% \newcommand \Vi {\bigwedge}
% \newcommand \im {\rightarrow} % fleche des treillis implicatifs
% \newcommand \da {\,\downarrow\!}
% %\newcommand \ua {\,\uparrow\!}


% \newcommand \vdu[1] {\vdash^{#1}}
% \newcommand \vdb[1] {\vdash_{#1}}

% \newcommand \Vrai {\mathsf{Vrai}}
% \newcommand \Faux {\mathsf{Faux}}
% \newcommand \Un {\mathbf{1}}
% \newcommand \Deux {\mathbf{2}}
% \newcommand \Trois {\mathbf{3}}
% \newcommand \Quatre {\mathbf{4}}
% \newcommand \Cinq {\mathbf{5}}


%:  souligné tout pret
\newcommand \una {{\underline{a}}}
\newcommand \ual {{\underline{\alpha}}}
\newcommand \ua  {{\underline{a}}}
\newcommand \ub  {{\underline{b}}}
\newcommand \ube {{\underline{\beta}}}
\newcommand \uc  {{\underline{c}}}
\newcommand \ud  {{\underline{d}}}
\newcommand \udel{{\underline{\delta}}}
\newcommand \ue  {{\underline{e}}}
\newcommand \uf  {{\underline{f}}}
\newcommand \uF  {{\underline{F}}}
\newcommand \ug  {{\underline{g}}}
\newcommand \uh  {{\underline{h}}}
\newcommand \uga {{\underline{\gamma}}}
\newcommand \uP  {{\underline{P}}}
\newcommand \ur{{\underline{r}}}
\newcommand \ut{{\underline{t}}}
\newcommand \uu{{\underline{u}}}
\newcommand \ux {{\underline{x}}}
\newcommand \uxi {{\underline{\xi}}}
\newcommand \uX {\underline{X}}
\newcommand \uy{{\underline{y}}}
\newcommand \uY  {{\underline{Y}}}
\newcommand \uz{{\underline{z}}}
\newcommand \uze {{\underline{0}}}


\newcommand \ak {a_1,\ldots,a_k}
\newcommand \am {a_1,\ldots,a_m}
\newcommand \an {a_1,\ldots,a_n}
\newcommand \aq {a_1,\ldots,a_q}
\newcommand \aln {\alpha_1,\ldots,\alpha_n}
\newcommand \bn {b_1,\ldots,b_n}
\newcommand \bzn {b_0,\ldots,b_n}
\newcommand \bbm {b_1,\ldots,b_m}
\newcommand \ck {c_1,\ldots,c_k}
\newcommand \rcr {c_1,\ldots,c_r}
\newcommand \cq {c_1,\ldots,c_q}
\newcommand \gan {\gamma_1,\ldots,\gamma_n}
\newcommand \un {u_1,\ldots,u_n}
\newcommand \xk {x_1,\ldots,x_k}
\newcommand \Xk {X_1,\ldots,X_k}
\newcommand \xm {x_1,\ldots,x_m}
\newcommand \Xm {X_1,\ldots,X_m}
\newcommand \fn {f_1,\ldots,f_n}
\newcommand \lfm {f_1,\ldots,f_m}
\newcommand \Fn {F_1,\ldots,F_n}
\newcommand \lFm {F_1,\ldots,F_m}
\newcommand \Fp {\FF_p}
\newcommand \Zp {\ZZ_p}
\newcommand \Qp {\QQ_p}
\newcommand \Cp {\CC_p}
\newcommand \sn {s_1,\ldots,s_n}
\newcommand \xn {x_1,\ldots,x_n}
\newcommand \xzn {x_0,\ldots,x_n}
\newcommand \xhn {x_0:\ldots:x_n}
\newcommand \Xn {X_1,\ldots,X_n}
\newcommand \xr {x_1,\ldots,x_r}
\newcommand \Xr {X_1,\ldots,X_r}
\newcommand \xin {\xi_1,\ldots,\xi_n}
\newcommand \xizn {\xi_0,\ldots,\xi_n}
\newcommand \xihn {\xi_0:\ldots:\xi_n}
\newcommand \ym {y_1,\ldots,y_m}
\newcommand \yr {y_1,\ldots,y_r}
\newcommand \Yr {Y_1,\ldots,Y_r}
\newcommand \Yn {Y_1,\ldots,Y_n}
\newcommand \Ym {Y_1,\ldots,Y_m}
\newcommand \yn {y_1,\ldots,y_n}

\newcommand \AT {\gA[T]}
\newcommand \AX {\gA[X]}
\newcommand \Ax {\gA[x]}
\newcommand \Ared {\gA\red}
\newcommand \AuX {\gA[\uX]}
\newcommand \Aux {\gA[\ux]}
\newcommand \ArX {\gA\lra X}
\newcommand \Axn {\gA[\xn]}
\newcommand \AXn {\gA[\Xn]}

\newcommand \AXm {\gA[\Xm]}
\newcommand \KKXm {{\KK[\Xm]}}
\newcommand \KKuX {{\KK[\uX]}}

\newcommand \AY {\gA[Y]}
\newcommand \Ayn {\gA[\yn]}

\newcommand \BuX {\gB[\uX]}
\newcommand \BuY {\gB[\uY]}
\newcommand \BX {{\gB[X]}}
\newcommand \BT {{\gB[T]}}
\newcommand \BY {{\gB[Y]}}
\newcommand \Bxn {\gB[\xn]}
\newcommand \BXn {{\gB[\Xn]}}
\newcommand \BYm {\gB[\Ym]}

\newcommand \CT {{\gC[T]}}
\newcommand \CX {{\gC[X]}}
\newcommand \CXn {{\gC[\Xn]}}

\newcommand \kX {{\gk[X]}}
\newcommand \KX {\gK[X]}
\newcommand \Kx {\gK[x]}
\newcommand \VX {\gV[X]}
\newcommand \Vx {\gV[x]}
\newcommand \VT {\gV[T]}
\newcommand \KT {\gK[T]}
\newcommand \KuX {\gK[\uX]}
\newcommand \kuX {\gk[\uX]}
\newcommand \VuX {\gV[\uX]}
\newcommand \Vuxi {\gV[\uxi]}
\newcommand \Vux {\gV[\ux]}
\newcommand \Kux {\gK[\ux]}
\newcommand \kux {\gk[\ux]}
\newcommand \KXk {\gK[\Xk]}
\newcommand \KXm {\gK[\Xm]}
\newcommand \KXn {\gK[\Xn]}
\newcommand \kxm {\gk[\xm]}
\newcommand \kxn {\gk[\xn]}
\newcommand \Ky {\gK[y]}
\newcommand \KY {\gK[Y]}
\newcommand \Kz {\gK[z]}
\newcommand \KZ {\gK[Z]}
\newcommand \kZ {\gk[Z]}
\newcommand \KYn {\gK[\Yn]}
\newcommand \KYm {\gK[\Ym]}
\newcommand \kXr {\gk[\Xr]}
\newcommand \KXr {\gK[\Xr]}
\newcommand \Kxr {\gK[\xr]}

\newcommand \Vxn {\gV[\xn]}
\newcommand \VXn {\gV[\Xn]}


\newcommand \KuY {\gK[\uY]}
\newcommand \Kuy {\gK[\uy]}
\newcommand \Kyn {\gK[\yn]}
\newcommand \Kyr {\gK[\yr]}
\newcommand \kYr {\gk[\Yr]}
\newcommand \KYr {\gK[\Yr]}
\newcommand \Kxn {\gK[\xn]}

\newcommand \LuX {\gL[\uX]}
\newcommand \lXn {\gl[\Xn]}
\newcommand \lxn {\gl[\xn]}
\newcommand \LXn {\gL[\Xn]}
\newcommand \lXr {\gl[\Xr]}
\newcommand \LXr {\gL[\Xr]}
\newcommand \lYr {\gl[\Yr]}
\newcommand \LYr {\gL[\Yr]}

\newcommand \QQXn {\QQ[\Xn]}

\newcommand \Rx {\gR[x]}
\newcommand \Rux {\gR[\ux]}
\newcommand \RuX {\gR[\uX]}
\newcommand \RXk {{\gR[\Xk]}}
\newcommand \RXm {{\gR[\Xm]}}
\newcommand \Rxm {{\gR[\xm]}}
\newcommand \RXn {{\gR[\Xn]}}
\newcommand \Rxn {{\gR[\xn]}}
\newcommand \RXzn {{\gR[\Xzn]}}
\newcommand \Rxzn {{\gR[\xzn]}}
\newcommand \RXr {\gR[\Xr]}

\newcommand \Ruy {\gR[\uy]}
\newcommand \Ryn {{\gR[\yn]}}
\newcommand \RRX {\RR[X]}
\newcommand \RRXn {\RR[\Xn]}
\newcommand \RRxn {\RR[\xn]}
\newcommand \RYr {\gR[\Yr]}
\newcommand \RRuX {\RR[\uX]}
\newcommand \RRux {\RR[\ux]}

\newcommand \CCX {\CC[X]}

\newcommand \ZZXn {\ZZ[\Xn]}
\newcommand \ZG {\ZZ[G]}

\newcommand \RRXk {{\RR[\Xk]}}
\newcommand \RRxk {{\RR[\xk]}}
\newcommand \RRXm {{\RR[\Xm]}}
\newcommand \RRxm {{\RR[\xm]}}
%\newcommand \RRXn {{\RR[\Xn]}}


\newcommand \lfs {f_1,\ldots,f_s}
\newcommand \lfn {f_1,\ldots,f_n}


% %:  Foncteurs grasmanniennes, GLn,SLn ...
% \newcommand \Gn  {\gG_n}
% \newcommand \Gnk {\gG^n_{k}}
% \newcommand \Gnr {\gG^n_{r}}
% \newcommand \cGn {\cG_n}
% \newcommand \cGnk{\cG_{n,k}}
% \newcommand \GGn {\GG^n}
% \newcommand \GGnk{\GGn_{k}} % Grasmannienne ``projective'' usuelle
% \newcommand \GGnr{\GGn_{r}}
% \newcommand \GA  {\mathbb{GA}}
% \newcommand \GAn {\GA^n}  % Grasmannienne ``affine'': matrices de proj
% \newcommand \GAq {\GA^q}
% \newcommand \GAnk{\GAn_{k}}
% \newcommand \GAnr{\GAn_{r}}
% \newcommand \GL {\mathbb{GL}}
% \newcommand \GLn {{\GL_n}}
% \newcommand \SL {\mathbb{SL}}
% \newcommand \SLn {{\SL_n}}
% \newcommand \EE {\mathbb{E}}
% \newcommand \En {\EE_n}
% \newcommand \Pn {\PP^n}
% \newcommand \An {\AA^n}
% \newcommand \Sl {\mathbf{SL}}
% \newcommand \Sln {{\Sl_n}}


% \newcommand \Mm {\MM_{m}}
% \newcommand \Mn {\MM_{n}}
% \newcommand \Mk {\MM_{k}}
% \newcommand \Mq {\MM_{q}}
% \newcommand \Mr {\MM_{r}}
% \newcommand \MMn {\MM_{n}}


% \newcommand \Pf {{{\cal P}_{\mathrm{f}}}}
% \newcommand \Pfe {{\rm P}_{{\rm fe}}}



% %: hsu
% \newcommand\hsz{\\ }
% \newcommand\hsu{\\ \hspace*{4mm}}
% \newcommand\hsd{\\ \hspace*{8mm}}
% \newcommand\hst{\\ \hspace*{1,2cm}}
% \newcommand\hsq{\\ \hspace*{1,6cm}}
% \newcommand\hsc{\\ \hspace*{2cm}}
% \newcommand\hsix{\\ \hspace*{2,4cm}}
% \newcommand\hsept{\\ \hspace*{2,8cm}}







%

% \renewcommand{\tr}{\mathrm{tr}}

% \DeclareMathAlphabet{\mathpzc}{OT1}{pzc}{m}{it}

%\makeindex


%: \sibrouillon
\newcommand \sibrouillon[1]{#1}
%\newcommand \sibrouillon[1]{}

\newcommand \hum[1] {\sibrouillon{\noindent {\sf hum: #1}}}



% \pagestyle{headings}

\patchcmd{\sectionmark}{\MakeUppercase}{}{}{}
%:DEBUT

\usepackage{authblk}
\renewcommand\Affilfont{\small}

\begin{document}%\raggedright\pagestyle{empty}

\author[$\dag$,1]{María Emilia Alonso García}
\author[$\ddag$]{Henri Lombardi}
\author[$\ddag$]{Stefan Neuwirth}
\affil[$\dag$]{Departamento de Álgebra, Geometría y Topología, Facultad de Ciencias Matemáticas, Universidad Complutense Madrid, Spain, \url{mariemi@mat.ucm.es}.}
\affil[$\ddag$]{Université Marie et Louis Pasteur, CNRS, LmB (UMR 6623), 25000 Besançon, France, \url{henri.lombardi@univ-fcomte.fr}, \url{stefan.neuwirth@univ-fcomte.fr}.}
\refstepcounter{footnote}\footnotetext{Partially supported by the research project PID2020-114750GB-C32 (Agencia Estatal de Investigación, Spain) and by the Instituto de Matemática Interdisciplinar (IMI, Universidad Complutense Madrid, Spain).}
\title{Note on the coincidence of two henselisations}
\date{}
\maketitle%\thispagestyle{empty}
\refstepcounter{footnote}

\begin{abstract} 
We compare two henselisations of a residually discrete valuation domain. Our constructive proof that a certain natural morphism is an isomorphism is also a proof in classical mathematics. Although this isomorphism is implicitly accepted as obvious in the literature, it seems that no proof was previously available.  
\end{abstract}

This note is written in Bishop's style of constructive mathematics \citep*{Bi67,BB85,BR1987,MRR,CACM,CCAPM}.

\medskip \noindent 
{\bf Terminology, notation.} 

\smallskip \noindent This paragraph clarifies the usual constructive terminology for a number of classical notions. From a constructive point of view, the development of good definitions\footnote{A ``good definition'' must have a clear constructive meaning, apply to cases usually dealt with in current literature, and be equivalent in classical mathematics to the most common definition. Naturally, this is not always a simple matter. Several ``good'' constructively inequivalent definitions can apply to a single classical notion and it is sometimes useful to consider them.} is a decisive part of the work which consists in extracting the constructive content of a concrete result obtained by means of a classical proof.

\smallskip \noindent A ring is \textsl{normal} if every principal ideal is integrally closed. 
In classical mathematics, this constructive definition is shown to be equivalent to the more usual definition according to which the ring becomes an integrally closed domain by localisation at any prime ideal. 

\smallskip \noindent A ring is \textsl{connected} if every idempotent is equal to~$0$ 
 or~$1$.

 \smallskip \noindent Let $\gK$ be a discrete field. A $\gK$-vector space~$E$ is \textsl{finite} over~$\gK$ (respectively \textsl{strictly} finite over~$\gK$) if it is a $\gK$-vector space of finite type (respectively if we know a finite basis of~$E$ over~$\gK$). 

 \smallskip \noindent A $\gK$-algebra~$\gL$ is \textsl{étale} if it is strictly finite and if the trace form  of the extension \(\gL/\gK\) is nondegenerate; equivalently, it is strictly finite and generated by separable elements over~$\gK$. % More generally, if $\gA$ is a ring, an $\gA$-algebra~$\gB$ is \textsl{strictly étale} if it is strictly finite and if the trace form is nondegenerate. 
 See for example \citet[Definition~VI-1.1, Theorems~VI-1.4 and~VI-1.7, taking into account Proposition and Definition~II-5.33 and Proposition~III-5.10]{CACM}.

\smallskip \noindent The \textsl{Jacobson radical} of a ring~$\gA$, denoted by $\Rad(\gA)$, is the ideal formed by the~$x\in\gA$ such that $1+x\gA\subseteq \Ati$ (the multiplicative group of units).

\smallskip \noindent A \textsl{pp-ring} (or \textsl{quasi-integral ring}) is a ring in which the annihilator of any element is generated by an idempotent. A quasi-integral ring is normal if, and only if, it is integrally closed in its total ring of fractions. An integral domain is none other than a connected quasi-integral ring.

\smallskip \noindent Let $\gA$~be a \textsl{local ring}, i.e., for any~$x\in\gA$, $x$ or~$1-x$ is a unit. Its Jacobson radical $\Rad(\gA)$, also denoted by~$\fm$ or~$\fm_\gA$, is equal to the ideal formed by the nonunits. It is called a \textsl{Heyting field} if $\Rad(\gA)=\{0\}$. 
The residual field of~$\gA$  is the quotient ring~$\gA/\Rad(\gA)$; $\gA$~is \textsl{residually discrete} when the residual field is a discrete field; this is equivalent to having a test for ``$x\in\Ati$ or $x\in\Rad(\gA)$?'' in~$\gA$.

\smallskip\noindent A morphism in the category of local rings is a ring morphism $\varphi\colon\gA\to\gC$ which reflects units, i.e.\ such that
$\varphi(x)\in\gC\eti$ implies $x\in\Ati$. Such a morphism is sometimes called local, to distinguish it from mere ring morphisms.  
In the category of residually discrete local rings, the morphism $\varphi\colon\gA\to\gC$ is said to define~$\gC$ as an \textsl{$\gA$-local-algebra}.\footnote{``$\gA$-local-algebra'' must be read as a single word: it is an abbreviation in which the word ``local'' refers to both the object~$\gC$ and the morphism $\varphi$.}

\smallskip \noindent A \textsl{Hensel code} in a residually discrete local ring $(\gA,\fm)$ is a pair
$(f,a)\in \AX\times \gA$ with~$f$ monic, $f(a)\in\fm$ and $f'(a)\in\Ati$.
 
\smallskip \noindent For a residually discrete local ring~$\gA$ and a Hensel code $(f,a)$, \textsl{a Hensel zero of code $(f,a)$} in an $\gA$-local-algebra $\varphi\colon\gA\to\gC$ is an element $\alpha\in\gC$ which verifies $f(\alpha)=0$ and 
$\alpha-\varphi(a)\in\Rad(\gC)$ (we then have $f'(\alpha)\in\gC\eti$). This zero is necessarily unique. A \textsl{special polynomial} is a polynomial 
$g(X)=X^n-X^{n-1}+a_{n-2}X^{n-2}+\dots+a_0%\sum_{k=0}^{n-2} a_kX^k
$ with the~$a_k$'s in~$\fm$; in this case, $(g,1)$ is a Hensel code whose Hensel zero is \textsl{the special zero} of~\(g\). A polynomial $f\in\AX$ such that $(f,0)$ is a Hensel code is called a \textsl{Hensel polynomial}; in this case the Hensel zero of code $(f,0)$ is simply called the Hensel zero of~$f$ in~$\gC$.

\smallskip \noindent A residually discrete local ring~$\gA$ is said to be \textsl{henselian} if every Hensel polynomial has a Hensel zero %(of code $(f,0)$)
in~$\gA$.

\smallskip \noindent A \textsl{discrete valued field}~$\KV$ is a discrete field~$\gK$ with a subring~$\gV$ which verifies: $xy=1\in\gK \implies x\in\gV$ or $y\in\gV$. 
In this case $\gV$ is a normal local ring. We also require that $\gV$ be residually discrete. This is equivalent to requiring that we have a test for ``$\exists x\in\gV$ such that $a=xb$?'', where $a,b\in\gK$.  


\smallskip \noindent Let $\gA$ be an arbitrary commutative ring and $f\in\AX$ a monic polynomial; we shall use the notation \fbox{$\Aq \gA f=\aqo\AX f$} and~\fbox{$\Aqj \gA f=\Aq \gA f[1/f']$}.


\smallskip \citet[Theorem 6.3]{CL2016b} state the following helpful nontrivial result.

\begin{theoremcinqtrois}
  If $\gA$ is a normal ring and $f\in\AX$ a monic polynomial, then $\gA_{\{ f\}}$ is also a normal ring.
\end{theoremcinqtrois}

\rdb\addcontentsline{toc}{subsection}{Presentation of the problem} \subsection*{Presentation of the problem}
 We answer a natural question that arises from the articles \citealt{KL00} and \citealt*{ALP08}. 

 \smallskip The henselisation of a residually discrete local ring $(\gA,\fm)$, denoted by $(\Ahe,\fmhe)$, is constructed in \citealt*{ALP08}. It solves the universal problem for the full subcategory of henselian residually discrete local rings in the category of residually discrete local rings. In other words the construction is functorial and the functor ``henselisation'' is the left adjoint functor to the inclusion functor.
 
\smallskip The henselisation of a discrete valued field $(\gK,\gV)$, denoted by $(\KHe,\VHe)$, is constructed in \citealt{KL00}. It solves the universal problem for the full subcategory of henselian discrete valued fields in the category of discrete valued fields. 

Since $\gV$ is a residually discrete local ring, it is natural to compare the two henselisations~$\Vhe$ and~$\VHe$. 

This problem does not seem to be addressed in the classical literature, perhaps because the answer seems obvious. But it has not been obvious to us, hence this note.
It also answers the problem from the point of view of classical mathematics, since our constructive definitions are equivalent to the usual definitions in classical mathematics.  

Given the universal property that characterises $(\Vhe,\mhe)$, and since $(\VHe,\mHe)$ is a residually discrete henselian local ring, we have a unique local morphism of $\gV$-algebras, viz.~\hbox{$\varphi\colon\Vhe\to \VHe$}. Our main result is the following.

\begin{theorem}\label{conj1}\label{thm3}
  Let $(\gK,\gV)$ be a discrete valued field with henselisation $(\KHe,\VHe)$. Let $(\Vhe,\mhe)$ be the henselisation of the residually discrete local ring $(\gV,\fm)$. The unique local morphism of local $\gV$-algebras $\varphi\colon\Vhe\to \VHe$ is an isomorphism.
\end{theorem}

 

\subsubsection*{The construction of the henselisation of a residually discrete local ring}

An elementary step in the construction of the henselisation~$\Ahe$ of a residually discrete local ring $(\gA,\fm)$ is as follows.
Let $f$ be a Hensel polynomial. 
Consider $\Ax=\Aq \gA f$, $S=1+\fm+\gen{x}$, and $\gA_f:=S^{-1}\Ax$. The ring $\gA_f$ is a residually discrete local ring with $\Rad(\gA_f)=\fm\gA_f$ and \(\xi=\frac x1\)~is the Hensel zero of~\(f\) in~$\gA_f$. The natural morphism $\gA\to\gA_f$ is local, faithfully flat, and we identify~$\gA$ with a subring of $\gA_f$. This morphism solves the universal problem for the Hensel code~\((f,0)\) in the category of $\gA$-algebras which are residually discrete local rings. 

We obtain the henselisation~$\Ahe$ as a filtered colimit of faithfully flat extensions of type 
\[\gA\to\gA_{f_1}\to((\gA_{f_1})_{f_2})\to\cdots.\]
Here $f_1$ is a Hensel polynomial in $\gA[T_1]$, $f_2$ is a Hensel polynomial in $\gA_{f_1}[T_2]$, and so on.
This filtered colimit is well defined because of the universal property satisfied by the morphism $\gA\to\gA_f$. We thus obtain a residually discrete local ring~$\Ahe$ with $\Rad(\Ahe)=\fm\Ahe$, and the morphism $\gA\to\Ahe$
yields the henselian residually discrete local ring ``generated by~$\gA$'' in the sense of the left adjoint functor to the inclusion functor in the category of residually discrete local rings. The morphism $\gA\to\Ahe$ is faithfully flat and we can identify $\gA_{f_1}$, $(\gA_{f_1})_{f_2}$, and so on with local subrings of $\Ahe$.

\subsubsection*{Special polynomials}

The following lemma, directly inspired by \citet*[Lemma~5.3 and Proposition~5.4]{ALP08}, tells us that in the construction of the henselisation, we can restrict ourselves to the case where we add a special zero of a special polynomial. 
 
\smallskip %:     Lemma{lemTrick1}
\begin{lemma} \label{lemTrick1} Let $(\gA,\fm)$ be a residually discrete local ring 
and $f(X)=a_0+a_1X+\dots+a_nX^n\in\AX$ with $a_0\in\fm$ and $a_1\in\Ati$.
%
\begin{enumerate}
%
\item We define the special polynomial 
\[
\formu{  
    g(X)&=&X^n-X^{n-1}+a_{0}%\cdot
\big(a_1^{-2}a_2X^{n-2}-a_0a_1^{-3}a_3X^{n-3}+\dots+(-1)^na_0^{n-2}a_1^{-n}a_n\bigr)%=\som_{j=2}^{n}(-1)^j a_{j}a_{0}^{j-2} a_{1}^{-j} X^{n-j}\big) 
\\[.4em]
&=& X^n-X^{n-1}+a_{0}\ell(X) \quad \hbox{with } \ell(X)\in\AX
  } 
\]
and ${g_1}(X)=g(X+1)$: \(g_1\) is a Hensel polynomial with Hensel zero~\(\mu\in\fm \gA_{g_1}\) and the special zero of~\(g\) is~\(\delta=1+\mu\in{\gA_{g_1}}\!\!\eti\). The polynomial~$f$ has the zero $\gamma=-a_0 (a_1\delta)^{-1}$ in $a_0\gA_{g_1}\subseteq \fm\gA_{g_1}\subseteq \fm\Ahe$, with~$f'(\gamma)$ a unit in $\gA_{g_1}$, and $\gamma$~is the unique zero of~$f$ in~$\fm\gA_{g_1}$.
%
\item In the particular case where \(f\)~is monic, it is a Hensel polynomial, \(\gA_f=\gA_{g_1}\),
  and \(\gamma\)~is the Hensel zero of~\(f\).%
%\item 
%
\end{enumerate}
\end{lemma}
%----------- end lemma ----------------------------------- 
%
\begin{proof}
The following equality occurs in $\gA[X,1/X]$:
\[
  a_0g(X) = X^nf\Bigl(\frac{-a_0a_1^{-1}}X\Bigr).  \eqno (*)
\]
Note that $\delta\in{\gA_{g_1}}\!\!\eti$.  
Let $\gamma=-a_0 (a_1\delta)^{-1}\in\fm\gA_{g_1}$. Applying~$(*)$ we get
$a_0 g(\delta)=\delta^n f(\gamma)$, so $f(\gamma)=0$. Moreover $f'(\gamma)\in{\gA_{g_1}}\!\!\eti$ because $f'(0)\in\Ati$.
% and $\gamma\in\fm\gA_{g_1}=\Rad(\gA_{g_1})$.

\noindent Uniqueness is straightforward (without the need to assume that $f$ be monic).
\end{proof}

In our article we use only the particular case \textsl{2.}\ of this lemma. 

\subsubsection*{Equality to~\(0\) in the henselisation of a discrete valued field}



For any discrete valued field $\KV$, we recall now the proof that $\KHe$ is again a discrete field. This proof is given in \citet[beginning of the proof of proposition 2.3]{KL00}. 

%l
%:     Lemma{lemKHediscretefield}
\begin{lemma} \label{lemKHediscretefield}
The field $\KHe$ is a discrete field. 
\end{lemma}
%----------- fin lemma ----------------------------------- 

%
\begin{proof}
Let \(\gK[x]=\aqo{\gK[X]}{g_1}=\Aq \gK {g_1}\) and compute the characteristic polynomial $q(T)\in\VT$ of~$p(x)$ in this $\gK$-algebra.
 The zeros of~$q$ in an algebraic closure of~$\gK$ are the $\alpha'_i=p(\mu'_i)$ where the~$\mu'_i$ are the zeros of ${g_1}$ (let $\mu'_1=\mu'$ and $\alpha'_1=\alpha'$). If~$q(0)\neq 0$, $\alpha'\neq 0$ because $q(\alpha')= 0$. If $q(0)=0$ we still do not know whether $\alpha'=0$. 
 We then calculate the characteristic polynomial~$r(T)\in\VT$ of $xp(x)$ in the $\gK$-algebra~$\Kx$. 
 The $\mu'_i$ for $i\geq 2$ are units, their valuation is zero.
 The zeros of~$r$ in~$\Kac$ are the $\mu'_i\alpha'_i$. 
 The valuation of the zeros of~$r$ is therefore the same as that of the zeros of~$q$, except in general the valuation of $\alpha'=\alpha'_1$ which increases by $v(\mu')$ when $v(\alpha')$ is finite, i.e.\ when $\alpha'\neq 0$. On the other hand $\infty+v(\mu')=\infty$ and we therefore obtain that $\alpha'=0$ if, and only if, the valuation of the zeros has not changed. The valuation of the zeros of a polynomial is given by Newton's polygon method. We therefore have an explicit test for~\hbox{$\alpha'=0$}.
\end{proof}
%

\subsubsection*{Isolated slope of a Newton polygon}

The Newton polygon of a polynomial $p\in\VT$ with respect to the valuation~\(v\) provides information about its zeros in extensions. An ``isolated slope'' of this polygon corresponds to a \textsl{$v$-isolated} zero in~$\KHe$;
\citet[Proposition~2.2]{KL00} give a precise description of this zero% which ends as follows
.

\begin{lemma}\label{lem4}
A zero $\beta$ corresponding to an isolated slope (from $p_kX^k$ to $p_{k+1}X^{k+1}$) of the Newton polygon of $p\in\VX$ has always the form $-\frac{p_k}{p_{k+1}}(1+\epsilon)$ where $\epsilon$ is the Hensel zero of a Hensel polynomial $q\in\VX$. So $v(\beta)=v(p_k)-v(p_{k+1})$.
\end{lemma}


\smallskip We shall also need the following observation.
% :     Lemma{lem5}
\begin{lemma}\label{lem5} If $\eta\in\gK[\delta]$,
where $\delta$ is a special zero of a special polynomial,
there exists an exponent~$m$ such that $\delta^m\eta$ is a $v$-isolated zero of a polynomial $p\in\VT$.
\end{lemma}
%----------- end lemma ----------------------------------- 
%
\begin{proof}
Result given in \citealt[proof of proposition 2.3]{KL00}.
\end{proof}
%

\rdb\addcontentsline{toc}{subsection}{Proof of Theorem~\ref{thm3}} \subsection*{Proof of Theorem~\ref{thm3}}



\subsubsection*{Injectivity of $\varphi\colon\Vhe\to \VHe$}

For injectivity, it is sufficient to prove it for an elementary step $\gV\!_f$ of the construction of~$\Vhe$, where $f$ is a Hensel polynomial.

We use Item~\textsl{2.}\ of Lemma \ref{lemTrick1} with $\gA=\gV$ and the monic polynomial $f$.
We have $\gV\!_f=\gV\!_{g_1}$, where $g_1=g(1+X)$ and $g$ is a special polynomial with special zero $\delta=1+\mu$. We consider the unique $\gV$-local morphism $\theta\colon\gV\!_{g_1}\to\VHe$. This morphism $\theta$ is the restriction of $\varphi$ to $\gV\!_{g_1}$ and it sends the Hensel zero~$\mu$ of~$g_1$ in $\gV\!_{g_1}$ to the Hensel zero~$\mu'$ of~$g_1$ in~$\VHe$. So, for $p\in\gV[X]$, it sends \(\alpha=p(\mu)\)~to~\(\alpha'=p(\mu')\). 
We have to show that $\theta$ is injective, i.e.\ to show that \(\alpha'=0\implies\alpha=0\). Recall that we have a zero test in $\VHe$.

Let \(q\)~be the characteristic polynomial of~$p(x)$ in the $\gK$-algebra $\Kx=\Aq \gK {g_1}$. If $q(0)\neq 0$ then $\alpha'\neq 0$, so that $\lnot(\alpha= 0)$ because $\alpha=0$ implies $\alpha'=0$.\footnote{Note that here, at this stage of the proof, we do not yet know whether we have a zero test in~$\Vhe$.} 
Otherwise let us write $q(T)=T^mq_1(T)$ with $m> 0$ and $q_1(0)\neq 0$. If $\alpha'=0$, then $q_1(\alpha')\neq 0$. This implies $q_1(\alpha)\neq 0$, and as \hbox{$q(\alpha)=\alpha^mq_1(\alpha)=0$}, we get $\alpha=0$.
The injectivity is proved. % the natural morphism $\theta\colon\gV\!_{g_1}\to\VHe$ is injective and $\gV\!_{g_1}$ itself is integral.  

\medskip The construction of $\Vhe$ shows that we can identify any ring $\gV\!_f$ with its image in~$\Vhe$. Now we see that we can moreover identify $\Vhe$ with its image in~$\VHe$.
 

We remark also that the previous proof shows that $\gV\!_{g_1}$ has itself has a zero test. 

Since $\gV$ is integrally closed, $\gV\!_{g_1}$ is normal and without zerodivisor \citep[Theorem~6.3]{CL2016b}.\footnote{By Theorem 6.3, the ring $\Aqj{\gV\!} f$ is normal. $\gV\!_{g_1}$ is a localisation of $\Aqj{\gV\!} f$, so that it is also normal, and as it is local it has no zerodivisor.} We deduce that $\gV\!_{g_1}$  is in fact integral and integrally closed.

As $\gV\!_f=\gV\!_{g_1}$ is an elementary step in the construction of $\Vhe$, it follows that $\Vhe$ is itself integral and integrally closed.
Hence we can consider the field of fractions $\Khe$ of $\Vhe$ and the inclusion $\Vhe\subseteq \VHe$ extends to an inclusion $\Khe\subseteq \KHe$. 

In the appendix, we shall give two independent constructive proofs of the fact that~$\gV\!_{g_1}$ is integral and integrally closed. 


\subsubsection*{Surjectivity of $\varphi\colon\Vhe\to \VHe$}

We consider again an elementary step $\gV\!_f=\gV\!_{g_1}$ of the construction of~$\Vhe$. For the Hensel zero $\mu$ of $g_1$,\footnote{This Hensel zero $\mu$ was denoted by $\mu'$ in the paragraph on injectivity. We have identified $\mu$ and $\mu'$.} $\delta=1+\mu$
is the special zero of the special polynomial $g(X)=g_1(X-1)$. 

To ensure that $\varphi\colon\Vhe\to \VHe$ is surjective is equivalent to showing that for the special zero $\delta\in\Vhe$ of a special polynomial in~$\VT$, any element $\eta$ of
$\gW=\gK[\delta]\cap \VHe$ is in $\Vhe$.

We use Lemma~\ref{lem5}. It shows that, for an exponent $m>0$, $\beta=\delta^m\eta$ is~a $v$-isolated zero of a polynomial $p\in\VT$.
Lemma \ref{lem4} says that $\beta=-\frac{p_k}{p_{k+1}}(1+\epsilon)$ where~$\epsilon$ is the Hensel zero of a Hensel polynomial $q\in\VT$. Moreover, since $v(\beta)=v(\epsilon)\geq 0$, we have $\frac{p_k}{p_{k+1}}\in\gV$. So $\beta\in\gV\!_q\subseteq \Vhe$. 
 As $1/\delta$ is in~$\Vhe$, this shows that $\eta\in\Vhe$.  
%

%c
%:     Comment
\begin{comment} 
It should be interesting to investigate whether a classical proof using the law of excluded middle and Zorn's lemma can be simpler than our constructive proof.    
\end{comment}
%--------- fin comment ------------------------------- 
%This completes the proof of the surjectivity of $\varphi$. 
%
%We have completed the proof of the fact that the canonical morphism 
%is an isomorphism. 
\[*\ *\ *\]

The above proof relies on the nontrivial Theorem~6.3 of \citet{CL2016b} for showing that $\Vhe$ is integral and integrally closed. Appendix~1 explains how to deduce this from the more elementary Theorem~2 of \citet*{ALN2021}. Appendix~2 provides a direct proof.
%We now turn to the appendices. 

%:Appendix 1 

 
\rdb\addcontentsline{toc}{subsection}{Appendix 1} \subsection*{Appendix 1}

Here is another constructive proof, different from the one given in the above proof, for the fact that $\gV\!_f$ is an integrally closed ring.

\smallskip \citet*{ALN2021} consider the situation of a Hensel polynomial~$f$ for a residually discrete local ring $(\gA,\fm_\gA)$ when $\gA$ is integral. The assumption is that $(\gA,\fm_\gA)$ is an integral local ring dominated by a valuation ring~$\gV$ of the field of fractions~$\gK$ of~$\gA$ (so $ \fm_\gA=\gA\cap\fm_\gV$). We consider a step of the construction of each of the henselisations~$\Ahe$ and~$\VHe$.
We thus have a residually discrete local ring $\gA_f\subseteq \Ahe$ obtained by adding the Hensel zero~$\beta$ of~$f$ and a valuation ring~$\gW$ extension of~$\gV$ obtained by adding the Hensel zero~$\beta'$ of~$f$.

Precisely $\gW=\sotq{\zeta\in\gK[\beta']}{v(\zeta)\geq 0}$.\footnote{$\gK[\beta']$ is constructed as a discrete valued field according to a procedure specific to discrete valued fields. It is a finite separable extension of~$\gK$, but its dimension as a $\gK$-vector space is not generally known. A similar phenomenon occurs when we construct the real closure of a discrete ordered field.}
Consider the morphism $\theta_f\colon\gA_f\to \gW$ which extends the inclusion morphism $\gA\to \gV$. The paper shows that $\Ker(\theta_f)$ is a \textsl{minimal detachable prime ideal} of $\gA_f$.
We apply this result to the present situation where $\gA=\gV$ is self-dominated: the kernel $\Ker(\theta_f)$ of the natural morphism $\theta_f\colon\gV\!_f\to \gW$ is a minimal detachable prime ideal. 

\smallskip $\gV\!_{f}$ is a residually discrete local ring, localisation of~$\gV\!_{\{ f\}}$, which is normal by Theorem~6.3 because $\gV$ is a valuation domain. So $\gV\!_{f}$ is a local normal ring and therefore has no zerodivisor: this gives the result used in the previous proof. In other words the ideal $\{0\}$ of $\gV\!_{f}$ is a prime ideal (in the sense that the quotient ring has no zerodivisors). We conclude by saying that since $\Ker(\theta_f)$ is a minimal detachable prime ideal and $\{0\}$ is a prime ideal, $\{0\}$ is detachable and $\gV\!_{f}$ is integral.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%:Appendix 2 

\rdb\addcontentsline{toc}{subsection}{Appendix 2} \subsection*{Appendix 2}

We now give a third, more direct, proof for the fact that 
the ring $\gV\!_f\subseteq \Vhe$ is integrally closed. The calculations underlying the three proofs are undoubtedly more similar than is apparent at first glance.

In fact Lemma~\ref{lemLND2} below and the analogous Theorem 6.3 in \citealt{CL2016b}
are both based on the formula of~Tate\footnote{A classical result is that if a ring~$\gA$ is a normal domain (i.e.\ integrally closed),
the same applies to~$\AX$.
A difficulty from an algorithmic point of view is that the usual proof of the previous result no longer works when we assume only that $\gA$ has no zerodivisor and not that it is integral. This was the primary motivation for the article \citealt{CL2016b}.} in Lemma~\ref{lemTate}.

%: Lemma{lemTate}
\begin{lemma}[Tate] \label{lemTate} 
Let $\gA$ be a commutative ring and $f\in \AX$ a monic polynomial of degree~$d$. 
Let us write \[f(X)=f(Y)+(X-Y)g(X,Y)\text{ with }g(X,Y)=\som_{j=0}^{d-1}g_j(Y)X^{j}\] and let us denote by~$\tr\colon\Aq\gA f\to\gA $ the trace form
of the extension $\Aq\gA f$. Then we have, for all $b\in\Aq\gA f=\Ax$,
%
\begin{equation}\label{eqnTate}
f'(x)b= \som_{j=0}^{d-1}\tr(g_j(x)b)\,x^{j}\text.  
\end{equation}
Note that $b,f'(x),g_j(x)\in \Aq\gA f$ and $\tr(g_j(x)b)\in \gA$.
\end{lemma}
%--------- fin lemma---------------------------------------------- 
%
\begin{proof}
See \citet[Chapter VII, corollary page~74]{Raynaud70} or Appendix~3.
\end{proof}
%

Remark~\ref{note1} prepares the corollary which follows.
% n
%:     Note{note1}
\begin{remark} \label{note1}
 Let $h\in \AX$ be a monic polynomial of degree~$d$ and $\Delta=uh+vh'=\pm\Res(h,h')$ be the discriminant of~$h$. Then~$h'$ is a unit in $\Aq\gA h$ if, and only if, $\Delta$ is a unit in~$\gA$ \citep[Basic elimination lemma III-7.5]{CACM}. Let us suppose that $\gA$ is an integral domain with field of fractions~$\gK$ and that $h$ is separable over~$\gK$.
We clearly have $\Aq\gA h \subseteq \Aq\gK h$ (respectively free over~$\gA$ and $\gK$ with basis $1,x,\dots,x^{d-1}$). Since~$h'$, $v$, and $\Delta$ are units in $\Aq\gK h$, they are regular in $\Aq\gA h$. We have $\Aq\gK h=\Aqj\gK h=\Aq\gK h[\frac 1 \Delta]$. Furthermore 
we have $\Aqj\gA h[\frac 1 v]=\Aq{\gA[\frac 1 \Delta]} h\subseteq \Aq\gK h$.
Thus the natural morphism $\Aq \gA h\to \Aq \gK h$ factorises into
% equation label {eqnote1}
\begin{equation} \label {eqnote1} \ndsp
\Aq \gA h \to \Aqj \gA h\to {\Aqj \gA h}[\frac 1 v]=\Aq{\gA[\frac 1 \Delta]} h\to  \Aq \gK h= \Aqj \gK h\text,
\end{equation}
where the morphisms are canonical injections which are localisation morphisms obtained by inverting regular monoids (successively ${h'}^\NN$,~$v^\NN$, and the nonzero elements of~\(\gA\)).\eoe
% end-equation
\end{remark}
%--------- fin note ------------------------------ 





%c
%:     Corollary{corlemTate}
\begin{corollary} \label{corlemTate}
Let $\gA$ be integrally closed and $\gK$ its field of fractions. Let $h$ be a separable monic polynomial of~$\AX$. Then 
$\Aqj \gA h$ is normal quasi-integral, with $\Aq \gK h=\Aqj \gK h$ as total ring of fractions. 
\end{corollary}
%--------- end corollary ------------------------------- 
%
\begin{proof}
If $d=\deg h$, $\Aq \gA h$ is free of dimension~$d$ over~$\gA$ and $\Aq \gK h=\gK\otimes_\gA \Aq \gA h$ is an étale $\gK$-algebra of dimension~$d$.  
We therefore have $\Aq \gA h\subseteq \Aq \gK h$; then $\Aqj \gA h= \Aq \gA h[1/h']\subseteq \Aq \gK h= \Aqj \gK h$.  To show that $\Aqj \gA h$ is integrally closed, we start by showing that any element~$b\in \Aq \gK h$ integral over $\Aq \gA h$ is in  
$\Aqj \gA h$. Let $b\in \Aq \gK h$ be integral over $\Aq \gA h$. As $\Aq \gA h$ is integral over~$\gA$, $b$ is integral over~$\gA$. 
We have $h' b\in \Aq \gA h$ according to Lemma~\ref{lemTate} (Equation~\eqref{eqnTate} with~$h$ in place of~$f$ and $\gK$ in place of~$\gA$):
since $b$ is integral over~$\gA$ and~$h_j(x)\in\gA$ for each~$j$, $\tr(h_j(x)b)$ is integral over~$\gA$, therefore in~$\gA$. Consequently~\hbox{$h' b\in \Aq \gA h$} and $b\in \Aqj \gA h$.

\noindent In particular, since any idempotent of $\Aq \gK h$ is integral over any subring, it belongs to $\Aqj \gA h$. 
Let $c$ be an arbitrary element of $\Aqj \gA h\subseteq \Aq \gK h$.
If $e^2=e$ and $\gen{e}=\Ann(c)$ in $\Aq \gK h$, a fortiori $e^2=e$ and $\gen{e}=\Ann(c)$ in
$\Aqj \gA h$. So $\Aqj \gA h$ is quasi-integral and 
its total ring of fractions is $\Aq \gK h$. Thus $\Aqj \gA h$ is quasi-integral and integrally closed in its total ring of fractions, so it is normal.
\end{proof}
%


%: Lemma{lemLND0}
\begin{lemma} \label{lemLND0}
Let $f\in \AX$ be a monic polynomial. The pairs of complementary idempotents of $\Aq \gA f$ are in bijective correspondence with the factorisations~$f=gh$ with~$g,h$ monic and $\gen{g,h}=\gen{1}$. For such a factorisation we obtain a natural isomorphism $\Aq \gA f\simeq \Aq \gA g\times \Aq \gA h$. 
\end{lemma}
%--------- end lemma ---------------------------------------------- 
%
\begin{proof}
If $gu+hv=1$ in $\Aq \gA f=\Ax$, the factorisation corresponds to the idempotents~$e=gu$ and $1-e=hv$. If $\gA$ is a discrete field~$\gK$, an idempotent~$e(x)$ corresponds to the element~$g(x)$, where $g(X)=\pgcd(f(X),e(X))$ in~$\KX$.  
\citet*{ALP08} give a proof in the case of a ring. We will use this lemma with a discrete field only.
\end{proof}
%
%: Lemma{lemLND01}
\begin{lemma} \label{lemLND01}
Let $\gK$ be a discrete field, $f\in \KX$ a monic polynomial, and $b\in \Aq \gK f$. We have a factorisation~$f=gh$ as in Lemma~\ref{lemLND0} with~$b$ a unit in $\Aq \gK h$ and nilpotent in $\Aq \gK g$. 
\end{lemma}
%--------- fin lemma ---------------------------------------------- 
%
\begin{proof}
The algebra $\gB:=\Aq \gK f$ is strictly finite zerodimensional. In a reduced zerodimensional ring, for any element~$b$ there is an idempotent~$e$ such that $\gen{b}=\gen{e}$, $b$ is a unit in $\gB[1/e]\simeq \aqo \gB {1-e} $ and nilpotent in $\aqo\gB e$. Apply Lemma~\ref{lemLND0}. 
\end{proof}
%


%: Lemma{lemLND1}
\begin{lemma} \label{lemLND1}
Let $\gK$ be a discrete field and $f\in \KX$ be a monic polynomial.\\
Then $\Aqj\gK f \simeq \Aqj\gK h=\Aq\gK h$
for a monic separable polynomial~$h$ which divides~$f$. 
In particular the $\gK$-algebra $\Aqj\gK f$ is étale. 
\end{lemma}
%--------- end lemma ---------------------------------------------- 
%
\begin{proof}  
Apply Lemma~\ref{lemLND01} with $b=f'(x)$. We have~$f=gh$ in~$\KX$, $f'=gh'+hg'$, $\Aq\gK f\simeq \Aq\gK g\times \Aq\gK h$.
The $\gK$-algebra $\Aqj\gK f$ is isomorphic to $\Aq \gK h$ because $f'$ is a unit in $\Aq \gK h$ and nilpotent in $\Aq \gK g$. In the $\gK$-algebra $\Aq \gK h$, $g$ and $f'=h'g$ are units, so $h'$ is also a unit and $h$ is separable over~$\gK$. Thus $\Aqj\gK h=\Aq\gK h$ is an étale $\gK$-algebra.
%
\end{proof}

Note that $\Aqj\gK f$ is zero when $f$ divides a power of~$f'$ in~$\KX$.

  


%: Lemma{lemLND2}
\begin{lemma} \label{lemLND2}
Let $\gA$ be a normal domain and $f\in \AX$
a monic polynomial. Then $\Aqj \gA f$ is 
% isomorphic to an $\gA$-algebra $\Aq \gA h$ for a polynomial separable of $\AX$, i.e.\
a normal quasi-integral ring. 
\end{lemma}
%--------- end lemma ---------------------------------------------- 
%
\begin{proof} %We assume that $\gA$ is nontrivial.
Let $\gK=\Frac\gA$% and $\varphi\colon\Aqj \gA f \to \Aqj \gK f$ be the natural morphism
.  
We apply Lemma~\ref{lemLND01} with $b=f'$ and Lemma~\ref{lemLND1}, we write {$f=gh$} with monic polynomials~$g$ and~$h$ in~$\KX$. We have $g,h\in \AX$ because $\gA$ is integrally closed.
Moreover $g$ monic divides a power of~$f'$ in~$\KX$ so in~$\AX$ (the division takes place entirely in~$\AX$). So $g$ is a unit in $\Aqj\gA f$, which implies~$h=0$ in $\Aqj\gA f$ because $gh=f=0$. 
We therefore obtain 
\[\ndsp
\Aqj\gA f=\Aq\gA{gh}[\frac 1{f'g}]\simeq \Aq\gA{gh}[\frac 1{g}][\frac 1{h'}]\simeq \Aq\gA{h}[\frac 1{g}][\frac 1{h'}]=\Aqj\gA h[1/g]\text.
\]
Relative to the natural inclusion $\Aq \gA h\to \Aq \gK h$, the elements~$h'$, $f'$, and~$g$, units in $\Aq \gK h$, are regular in $\Aq \gA h$. We therefore obtain the canonical injective morphisms of localisation at regular monoids shown below:
\[\Aq \gA h \to\Aqj \gA h \to \Aqj\gA f%\simeq \Aq \gA h[1/f']%\simeq \Aqj \gA h[1/g]
\to   \Aq\gK h\simeq \Aqj\gK f.
\] 



\noindent 
We conclude with Corollary~\ref{corlemTate} that $\Aqj\gA h$ is normal quasi-integral, and therefore also its localisation~$\Aqj\gA f\simeq\Aqj \gA h[1/g]$.
% 
\end{proof}

%:     Lemma{lemLND3}
\begin{lemma} \label{lemLND3}
Let $\gA$ be an integrally closed residually discrete local ring and $f\in \AX$
a monic polynomial. Then $\gA_f $ is an integrally closed residually discrete local ring. 
\end{lemma}
%--------- end lemma ---------------------------------------------- %
%
\begin{proof}
We know that $\gA_f $ is a residually discrete local ring.  As a localisation of~$\Aqj \gA f$, it is a normal quasi-integral ring.  And every local ring is connected.
\end{proof}
%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%:Appendix 3 

\rdb\addcontentsline{toc}{subsection}{Appendix 3} \subsection*{Appendix 3}

In this appendix, we recall a proof of Tate's lemma given in
\citealt{CL2016b} which is simpler than the one of \citet[Chapter~VII, §1]{Raynaud70}.
%
\begin{proof}[Proof of Lemma~{\ref{lemTate}}] We have $\Aq\gA f=\Ax=\aqo\AX f$.
Let $\gB=\gA[x_1,\dots,x_d]$ be the universal decomposition algebra of~$\gA$ for~$f$, where $f(X)=\prod_{i=1}^d(X-x_i)$ \citep[Definition III-4.1]{CACM}. Each $\gA[x_i]\subseteq \gB$ is isomorphic to $\gA[x]$ and we can take $x=x_1$.  
We write $b=h(x) \in \Aq\gA f$. For all $\ell(x)\in \Aq\gA f$ we have $\tr (\ell(x))=\som_{i=1}^d\ell(x_i)\in\gA$.\footnote{See for example \citet[Lemma III-5.12]{CACM}.} We have $g(Y,Y)=f'(Y)$ and $g(x_1,x_i)=g(x_i,x_1)=0$ if $i\neq 1$: in fact $g(X,x_1)=\prod_{i=2}^d(X-x_i)$ because $(X-x_1)g(X,x_1)=f(X)-f(x_1)=f(X)=\prod_{i=1}^d(X-x_i)$.
So 
\[f'(x_1)b=g(x_1,x_1)h(x_1)=\som_{j=0}^{d-1} g_j(x_1)h(x_1)x_1^j\]
and for $i\neq 1$ 
\[0=g(x_1,x_i)h(x_i)=\som_{j=0}^{d-1} g_j(x_i)h(x_i)x_1^j\text.\]
Summation gives the Tate formula announced.
\end{proof}
%

%\hum{In \cite{CL2016b}, we do not say that $f$ is separable but we assume that $\gA$ is normal. This assumption is used to show that $\tr(b)$ has a value in $a\gA$ if $b$ is integral over $a\gA$, but this intermediate result disappears in the calculation that follows, reproduced above.
%Moreover, the result $g(x_1,x_j)=0$ if $jneq 1$ seems absolutely necessary~$f$ separable.}.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%:References \newpage
% \small
\bibliographystyle{plainnat}
\bibliography{Note2Hbib}


\end{document}



