Solution (source code)

= Solution

An <algebraic line bundle> over $A$ is an <invertible module>: a <finitely generated projective module> $L$ such that $L_{\mathfrak p}\cong A_{\mathfrak p}$ for every <prime ideal> $\mathfrak p$. Define the <Picard group of a ring> as the set of its isomorphism classes, with
$$
[L][K]=[L\otimes_AK].
$$
The <tensor product of modules> of two finite <projective modules> is finite projective: write each as a direct summand of a finite <free module> and tensor the two decompositions. Localization gives $(L\otimes_AK)_{\mathfrak p}\cong A_{\mathfrak p}$, so this multiplication stays within the set of <invertible modules>. It is well defined on isomorphism classes. The associativity and symmetry isomorphisms of the <tensor product> give associativity and commutativity, and $[A]$ is the identity.

Let $L^*=\operatorname{Hom}_A(L,A)$ be the <dual module>. A finite direct-summand presentation shows that $L^*$ is finite projective and that localization commutes with this dual. Since $L_{\mathfrak p}$ is free of rank one, so is $(L^*)_{\mathfrak p}$. The <evaluation homomorphism>
$$
L\otimes_AL^*\longrightarrow A,\qquad \ell\otimes\lambda\longmapsto\lambda(\ell)
$$
is an <isomorphism> after every prime localization. Its kernel and cokernel are therefore zero, by <exactness of localization> and <localization detects zero elements> for modules. Thus \b[$[L]^{-1}=[L^*]$], proving that $\operatorname{Pic}(A)$ is an <abelian group>.

For a <ring homomorphism> $f:A\to B$, tensoring a split presentation $L\oplus L'\cong A^r$ gives $(B\otimes_AL)\oplus(B\otimes_AL')\cong B^r$, so $B\otimes_AL$ is finite projective. For $\mathfrak q\in\operatorname{Spec}B$ put $\mathfrak p=f^{-1}(\mathfrak q)$. Every element of $A\setminus\mathfrak p$ becomes a <unit> in $B_{\mathfrak q}$, and
$$
(B\otimes_AL)_{\mathfrak q}\cong B_{\mathfrak q}\otimes_{A_{\mathfrak p}}L_{\mathfrak p}\cong B_{\mathfrak q}.
$$
This proves <base change of invertible modules>. Moreover, the canonical map
$$
(B\otimes_AL)\otimes_B(B\otimes_AK)\longrightarrow B\otimes_A(L\otimes_AK),\qquad (b\otimes\ell)\otimes(b'\otimes k)\longmapsto bb'\otimes(\ell\otimes k)
$$
is an <isomorphism>, with inverse $b\otimes(\ell\otimes k)\mapsto(b\otimes\ell)\otimes(1\otimes k)$. It shows that $[L]\mapsto[B\otimes_AL]$ is a <group homomorphism>. Identity maps induce the identity, and for $A\to B\to C$, the associativity isomorphism $C\otimes_B(B\otimes_AL)\cong C\otimes_AL$ proves composition compatibility. Therefore \b[$\operatorname{Pic}$ is a covariant functor to abelian groups].

The <polynomial ring> $\mathbb C[x]$ is a <principal ideal domain> by division with remainder. A submodule $N$ of a finite free module over a <principal ideal domain> is free: induct on the ambient rank, project onto the first coordinate, and note that the image is a principal <ideal>, hence either zero or a free rank-one module. This gives a split exact sequence with that image as quotient; the kernel lies in a free module of one smaller rank, completing the induction. A finite <projective module> is such a submodule, and so is free. An <invertible module> has rank one after passing to the <fraction field>, so its free rank is exactly one. Hence every <algebraic line bundle> over $\mathbb C[x]$ is trivial and
$$
\boxed{\operatorname{Pic}(\mathbb C[x])=0.}
$$