I am trying to prove $\text{Cl}(X\times\mathbb{P}^n)\cong \text{Cl}(X)\times \mathbb{Z}$, where $X$ is a Noetherian integral separated regular in codimension 1 scheme, and $\text{Cl}(X)$ is the (Weil) divisor class group of $X$. I also want to see this isomorphism as explicitly as possible. I think I've got most of it, but still have some points which I would like to understand better.
First of all, $X\times\mathbb{P}^n$ is regular in codimension 1. The interesting codimension 1 points are those points $y$ that map to a generic point of a codimension 1 point $x$ in $X$ under the projection, their local rings are of the form $O_{X,x}[t_1,\ldots,t_n]_{(m_x)}$, where $m_x$ is the generator of the maximal ideal of $O_{X,x}$. Since $O_{X,x}$ is a DVR, this larger ring is also a DVR. The valuation takes an element $f/g$ in $K(X)(t_1,\ldots,t_n)$ to $\text{cont}(f)-\text{cont}(g)$, where $\text{cont}(f)$ is the minimal valuation (in $K(X)$) of the coefficients of $f$.
Now I have an exact sequence $$\mathbb{Z}\longrightarrow \text{Cl}(X\times \mathbb{P^n)}\longrightarrow\text{Cl}(X\times \mathbb{A}^n)\longrightarrow 0,$$
coming from the leftmost map which takes 1 to the class of $X\times \mathbb{P}^{n-1}$ with some fixed embedding $\mathbb{P}^{n-1}\to\mathbb{P}^{n}$. To be more specific, let's realize $\mathbb{P}^n_k$ as $\text{Proj}(\mathbb{Z}[x_0,\ldots,x_n])$ and then embed the smaller space as the clossed subscheme corresponding to $(x_0).$
Now we know that $\text{Cl}(X\times \mathbb{A}^n)\cong \text{Cl}(X)$, and the key step in the argument there is something like this:
Using induction on the dimension $n$, we may assume $n=1$. Then assume a codimension 1 point (i.e. prime divisor) $Z$ projects to the generic point $\xi$ in $X$. Hartshorne writes "Localizing at the generic point of $X$, we get a prime divisor in $\text{Spec } K[t]$, which corresponds to a prime ideal $p \in K[t]$". My understanding of that: the fiber of the generic point of $X$ is $\text{Spec } K[t],$ the preimage of $Z$ in $\text{Spec } K[t]$ is a prime divisor given by some principal ideal $(f)$. Then considering $f$ as a rational function on $X\times \mathbb{A^1}$ we get that the divisor of $f$ consists of $Z$ plus some prime divisor that do not map to the generic point of $X$. Pictorially, by 'wiggling' things 'vertically' we may take a divisor from the whole $X$ to a closed subset of it. Question: Is my translation correct?
I am now trying to proceed in a similar way. Consider a prime divisor $Z$ on $X\times\mathbb{P}^n$. If it is our previously defined subscheme $X\times \mathbb{P}^{n-1}$, we map it to 1 in $\mathbb{Z}$. Otherwise, consider the intersection with the complement $Z'=Z\cap X\times\mathbb{A}^n$. By the argument for the case of product with the affine space, we have that there exists some $f\in K(X)(t_{1/0},\ldots,t_{n/0})$ such that $Z'=(f)+T$, where $T$ is a sum of divisors which do not map to the generic point of $X$ under projection. Now we identify the field of functions of $K(X\times \mathbb{P}^n)$ with the fractions of homogeneous polynomials in $K(X)[t_0,\ldots,t_n]$ of total degree 0. Then for some $m\in\mathbb{Z},\ t_0^mf(t_1,\ldots,t_n)$ is such a rational function on $K(X\times \mathbb{P}^n)$. Question: is this step correct? I am reasonably confident it is, and it is definitely correct when $X$ is an affine scheme, but does anything break when $X$ is an arbitrary scheme?
Now we have $Z=\overline{Z'}+\overline{T}+m(X\times{\mathbb{P}}^{n-1})$, and we map $Z$ to $m\in\mathbb{Z}$. This gives the desired splitting of the exact sequence above, and a left-split short exact sequence of groups describes the middle group as the product of the two other groups.