Etale morphisms of formal schemes

Remarks. a) This definition is independent of the choice of the Ideal of definition. We omit the easy proof which depends on EGA 

The morphism f is tale because fetaleness is preserved by the base change S for every n.  

Proposition 6.1.3. If Et( X ) (resp. Et(SQ)) denotes the category of formal S-schemes (resp. So-schemes) fetale over xf (resp. over SQ) then the natural functor 

Descent lemma. Let p xf — be an fetale. quasi-compact surjective morphism of locally noetherian formal schemes. Put / = /Xy r and cp.p = p.P2= Then  

Assertion i) follows from the corresponding statement for the p after taking the projective limit, ii) follows for coherent sheaves from EGAI 10.11.3 and the corresponding statement for pn. In case of locally free 0y-4todules one uses [3], Alg. Comm.,chap. Ill, Th.l 5 Next iii) follows from ii) applied on the 0 -Algebra f+(0 )  

Finally iv) follows from EGA I 10.12.3 and the corresponding statement for usual schemes applied to o).  

---