let $X,Y$ be smooth schemes (or rigid spaces etc..) over a base $S$, let $f:Y \rightarrow X$ be a $S$-morphisn and let $\mathcal{F}$ be a locally free $\mathcal{O}\_X$-module with connection $\nabla$. How do we define the "pull-back connection" along $f$? We get a connection $$f^{-1}\mathcal{F} \overset{f^{-1}\nabla}{\rightarrow} f^{-1}\mathcal{F} \otimes\_{f^{-1}\mathcal{O}\_X} f^{-1} \Omega^1\_X,$$ do we extend this to $f^{\ast}\mathcal{F}$ by taking $f^{\ast}\nabla= f^{-1}\nabla \otimes d\_Y : f^{-1}\mathcal{F} \otimes\_{f^{-1}\mathcal{O}\_X} \mathcal{O}\_Y$ (as tensor product of connections) or how?


Sorry for the stupid question but it is hard to find references on connections which are not written in the language of differential geometry.



Pullback of a connection
Recall that you have a map $f^\* \colon f^{-1} \Omega\_X \to \Omega\_Y$ (pull-back of differentials). Consider the composition $$ \nabla' \colon f^{-1} E \xrightarrow{f^{-1} \nabla} f^{-1} E\otimes\_{f^{-1} \mathcal{O}\_X} f^{-1}\Omega\_X \xrightarrow{{\rm id}\otimes f^\*} f^{-1} E\otimes\_{f^{-1}\mathcal{O}\_X} \Omega\_Y = f^\* E \otimes\_{\mathcal{O}\_Y} \Omega\_Y. $$
We want to extend $\nabla'$ to $f^\* E$; i.e. we want to check that $$ (f^\*\nabla)(e\otimes y) = \nabla'(e)\cdot y + (e\otimes 1)\otimes dy, \quad y\in\mathcal{O}\_Y, ', e\in f^{-1} E$$ gives a well-defined map $f^\* E\to f^\* E \otimes\_{\mathcal{O}\_Y} \Omega\_Y$. This amounts to checking that
$$ \nabla'(e)\cdot xy + (e\otimes 1)\otimes dxy = \nabla'(ex)y + (ex\otimes 1)\otimes dy, \quad x\in f^{-1}\mathcal{O}\_X,\, y\in \mathcal{O}\_Y,\, e\in f^{-1} E. $$
For this, use the fact that the Leibniz rule for $E$ implies $\nabla'(ex) = e\otimes dx + \nabla'(e)\cdot x$.


One also needs to check that $f^\*\nabla$ satisfies the Leibniz rule.


