Pullback of a connection 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.
 A: 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.
A: Another option is to proceed as follows : show that there exists a unique connection $f^*\nabla$ on $f^*\mathcal F$ verifying :
$$ (f^*\nabla)(f^*s) = f^*(\nabla(s))$$
where on the right-hand side  you use the canonical morphism $f^* (\mathcal F\otimes \Omega^1_X)\to  f^* \mathcal F\otimes \Omega^1_Y$.
The uniqueness follows from Leibniz rule, as the $f^*s$ generate $f^* \mathcal F$ (locally).
To show the existence locally, you can trivialize $\mathcal F$. Connections on the trivial bundle are of the form $d+\Omega$, where $\Omega$ is a matrix of $1$-forms. It is enough to take the matrix obtained by pulling back each form individually.
Finally, the uniqueness ensures that you can glue these local connections together to get a global solution.
