If $X$ is a smooth rigid analytic space over a $p$-adic field $K$ (of characteristic zero), then every coherent $\mathcal{O}\_X$-module with integrable connection is locally free. In his paper ["Finiteness theorems for the cohomology of an overconvergent isocrystal on a curve"](http://www.numdam.org/numdam-bin/fitem?id=ASENS_1998_4_31_6_717_0) Crew gives a proof of this result in the particular case of a 1-dimensional annulus over $K$ as follows.


Let $I$ be a closed interval of $[0,\infty)$, and $A\_I$ the ring of Laurent series in 1 variable over $K$ which are convergent for $\vert x \vert\in I$. Let $M$ be a finitely generated $A\_I$-module with connection, we wish to prove that $M$ is a projective $A\_I$-module. Since $A\_I$ is a PID it suffices to show that $M$ is torsion free. Let $f$ generate the annihilator of $M\_{\mathrm{tors}}$, one can easily show using the axioms of a connection that $f'\in (f)$. (Here $f'$ means differentiation with respect to the variable).


Crew now argues as follows: "Since $A\_I$ is a PID and contains the rational numbers, $(f)$ must be the unit ideal, and hence $M\_{\mathrm{tors}}=0$".


**Why does this implication hold? That is, why does the fact that $A\_I$ is a PID and a $\mathbb{Q}$-algebra, together with the fact that $f'\in (f)$, imply that $(f)=A\_I$?**


For example, would this implication still hold if I worked instead over the ring $K\otimes\_{\mathcal{O}\_K} \mathcal{O}\_K[[t]]$ of power series with bounded coefficients?



Modules with connection over $p$-adic laurent series rings
There are two possible arguments, I think. First, using $A\_I$ is a PID you can factor $f$ into prime factors, and work with each of them. We need to prove that if $g$ is prime and $f=g^e$ for some $e\geq 1$ is such that $f'\in f$, then $f$ is a constant. Now, the first option is that you redo the theory of resultants for convergent series, which is more or less the Fredholm theory Crew develops in the first chapters (or in Serre, *Endmorphismes complètement continus...*, 12\_69\_0">http://www.numdam.org/item?id=PMIHES\_1962\_*12*\_69\_0 ): you see that a series of our form must have multiple roots, and since we are in characteristic $0$ you deduce $e>1$, so replace $f$ by $f'$ (divide by $e$, which you can do because you are in a $\mathbb{Q}$-algebra) and reduce to $f=g$ prime, where it becomes a contradiction.


The second option is to use a simple structure theorem telling you that your series (as well as the formal ones with bounded denominators, positively answering your second question) can be "uniquely" factored as $f=cUg$ with $c\in K^\times,U\in A\_I^\times,g\in\mathcal{O}\_K[t]$, where quotes around unique are there because you need to impose some constraint to really have uniqueness (eg: $g$ monic and $U(0)=1$), as units in $K$ mess things up. Now, since you work with generators of ideals, you can throw units away and are left with the usual theory of polynomials over a field, where you have a degree argument telling you that if $f'=qf$ for some $q$, then $q=0$: since you are *not* in positive characteristic (where pathologies like $(t^p)'=0$ can occur), you conclude $f$ is a constant.


For a reference to the structure theorem, you can look at Washington's book *Introduction to cyclotomic fields*, chapter 13 for power series; and Fresnel-van der Put, *Rigid Analytic Geometry and Its Applications*, chapter 2 for converging series.


