[proofplan] We apply the low-degree localization sequence to the localization map $A\to F=S^{-1}A$, where $S=A\setminus\{0_A\}$. The torsion term in that sequence is identified with the divisor group by devissage: a finite torsion module contributes its local lengths at the nonzero prime ideals. Under this identification, the boundary map $K_1(F)\to \operatorname{Div}(A)$ is exactly the valuation divisor map. Exactness then identifies the kernel of $K_0(A)\to K_0(F)$ with divisor classes modulo principal divisors, which is the ideal class group. [/proofplan]

[step:Apply localization to the punctured multiplicative set] Let \begin{align*} S=A\setminus\{0_A\}. \end{align*} Since $A$ is a domain, $S$ is a multiplicative subset of $A$, and its localization is the fraction field: \begin{align*} S^{-1}A=F. \end{align*} Let $\mathcal T_S(A)$ denote the exact category of finitely generated $A$-modules $M$ such that $S^{-1}M=0$; these are exactly the finitely generated $S$-torsion $A$-modules appearing in the localization theorem. Since $A$ is a Dedekind domain, it is a regular Noetherian commutative ring, so the low-degree localization sequence [citetheorem:8670] applies to the pair $(A,S)$ and gives an exact sequence \begin{align*} K_1(A)\longrightarrow K_1(F)\xrightarrow{\partial}K_0(\mathcal T_S(A))\longrightarrow K_0(A)\longrightarrow K_0(F)\longrightarrow 0. \end{align*} Here the map $K_0(A)\to K_0(F)$ is induced by extension of scalars $M\mapsto F\otimes_A M$. [/step]

[step:Identify the torsion term with the divisor group]For every nonzero prime ideal $\mathfrak p\subset A$, the localization $A_{\mathfrak p}$ is a discrete valuation ring. For each nonzero prime ideal $\mathfrak p\subset A$, define the local-length function \begin{align*} \ell_{\mathfrak p}:\operatorname{Ob}(\mathcal T_S(A))\to \mathbb Z_{\ge 0} \end{align*} by $\ell_{\mathfrak p}(M)=\operatorname{length}_{A_{\mathfrak p}}(M_{\mathfrak p})$. Only finitely many of these integers are nonzero for a fixed object $M\in\mathcal T_S(A)$. Indeed, since $M$ is finitely generated and torsion over the Noetherian domain $A$, its annihilator $\operatorname{ann}_A(M)$ contains a nonzero element. Let $V(\operatorname{ann}_A(M))$ denote the set of prime ideals of $A$ containing $\operatorname{ann}_A(M)$. The support of $M$ is contained in $V(\operatorname{ann}_A(M))$, and in a Dedekind domain every nonzero prime ideal is maximal; hence $V(\operatorname{ann}_A(M))$ is the finite set of maximal ideals appearing over the nonzero ideal $\operatorname{ann}_A(M)$. Thus each nonzero localization $M_{\mathfrak p}$ is a finitely generated torsion module over the discrete valuation ring $A_{\mathfrak p}$ and therefore has finite length. Define \begin{align*} \lambda:K_0(\mathcal T_S(A))\to \operatorname{Div}(A) \end{align*} on classes by \begin{align*} \lambda([M])=\sum_{\mathfrak p\ne 0}\ell_{\mathfrak p}(M)[\mathfrak p]. \end{align*} Length is additive in short exact sequences, so $\lambda$ is a well-defined [group homomorphism](/page/Group%20Homomorphism). The same finite-support and local finite-length argument shows that every object of $\mathcal T_S(A)$ has a finite composition series, so $\mathcal T_S(A)$ is a length category. By devissage for the length category $\mathcal T_S(A)$, equivalently by [citetheorem:8643] applied to its simple objects, $K_0(\mathcal T_S(A))$ is the free abelian group generated by the classes of the simple torsion modules. The simple objects are precisely $A/\mathfrak p$ for nonzero prime ideals $\mathfrak p\subset A$. If $\mathfrak q=\mathfrak p$, then $(A/\mathfrak p)_{\mathfrak q}$ is the residue field of $A_{\mathfrak p}$ and has $A_{\mathfrak p}$-length $1$. If $\mathfrak q\ne \mathfrak p$, then $(A/\mathfrak p)_{\mathfrak q}=0$ and has $A_{\mathfrak q}$-length $0$. Hence the map $\lambda$ sends $[A/\mathfrak p]$ to $[\mathfrak p]$. Hence $\lambda$ is an isomorphism \begin{align*} K_0(\mathcal T_S(A))\cong \operatorname{Div}(A). \end{align*}[/step]

[guided]The localization sequence produces the group $K_0(\mathcal T_S(A))$, so we must translate that group into divisor language. The category $\mathcal T_S(A)$ consists of finitely generated $A$-modules killed by localization at $S=A\setminus\{0_A\}$; equivalently, these are the finitely generated torsion $A$-modules. For a nonzero prime ideal $\mathfrak p\subset A$, the local ring $A_{\mathfrak p}$ is a discrete valuation ring. Thus a finitely generated torsion $A_{\mathfrak p}$-module has finite length. For each $M\in \mathcal T_S(A)$, define \begin{align*} \ell_{\mathfrak p}(M)=\operatorname{length}_{A_{\mathfrak p}}(M_{\mathfrak p}). \end{align*} Because $M$ is finitely generated and torsion over the Noetherian domain $A$, the annihilator $\operatorname{ann}_A(M)$ contains a nonzero element. Let $V(\operatorname{ann}_A(M))$ denote the set of prime ideals of $A$ containing $\operatorname{ann}_A(M)$. The support of $M$ is contained in $V(\operatorname{ann}_A(M))$. Since $A$ is a Dedekind domain, every nonzero prime ideal is maximal, and a nonzero ideal is contained in only finitely many maximal ideals. Therefore only finitely many values $\ell_{\mathfrak p}(M)$ are nonzero. Each nonzero localization $M_{\mathfrak p}$ is a finitely generated torsion module over the discrete valuation ring $A_{\mathfrak p}$, hence has finite length. Therefore the expression \begin{align*} \sum_{\mathfrak p\ne 0}\ell_{\mathfrak p}(M)[\mathfrak p] \end{align*} is a genuine element of the direct sum defining $\operatorname{Div}(A)$, and every object of $\mathcal T_S(A)$ has a finite composition series. Now define \begin{align*} \lambda:K_0(\mathcal T_S(A))\to \operatorname{Div}(A) \end{align*} by \begin{align*} \lambda([M])=\sum_{\mathfrak p\ne 0}\ell_{\mathfrak p}(M)[\mathfrak p]. \end{align*} This is well-defined because localization preserves short exact sequences and module length is additive in short exact sequences of finite-length modules over the local ring $A_{\mathfrak p}$. Hence if \begin{align*} 0\longrightarrow M'\longrightarrow M\longrightarrow M''\longrightarrow 0 \end{align*} is exact in $\mathcal T_S(A)$, then for each nonzero prime ideal $\mathfrak p$, \begin{align*} \ell_{\mathfrak p}(M)=\ell_{\mathfrak p}(M')+\ell_{\mathfrak p}(M''). \end{align*} This is exactly the additivity relation imposed in $K_0(\mathcal T_S(A))$. It remains to see that $\lambda$ is an isomorphism. The preceding paragraph shows that $\mathcal T_S(A)$ is a length category. Its simple objects are the residue modules $A/\mathfrak p$ with $\mathfrak p$ a nonzero prime ideal. Applying the Jordan Holder computation of $K_0$ for a length category [citetheorem:8643], the classes $[A/\mathfrak p]$ form a free basis of $K_0(\mathcal T_S(A))$. For nonzero prime ideals $\mathfrak p$ and $\mathfrak q$, localizing $A/\mathfrak p$ at $\mathfrak q$ gives zero unless $\mathfrak q=\mathfrak p$, and gives the residue field of $A_{\mathfrak p}$ when $\mathfrak q=\mathfrak p$. Therefore $(A/\mathfrak p)_{\mathfrak p}$ has $A_{\mathfrak p}$-length $1$, while $(A/\mathfrak p)_{\mathfrak q}$ has $A_{\mathfrak q}$-length $0$ for $\mathfrak q\ne\mathfrak p$. So $\lambda([A/\mathfrak p])=[\mathfrak p]$. Since both sides are free abelian groups on the same indexed basis, $\lambda$ is an isomorphism.[/guided]

[step:Identify the boundary with the valuation divisor map] By the field case for $K_1$ [citetheorem:8661], applied to the field $F$, the determinant gives an isomorphism \begin{align*} K_1(F)\cong F^\times. \end{align*} The hypotheses of the codimension-one divisor boundary theorem [citetheorem:8691] apply because $A$ is a Dedekind domain with fraction field $F$, and the multiplicative set used here is $S=A\setminus\{0_A\}$. Under the determinant identification of $K_1(F)$ with $F^\times$ and the length-devissage identification of $K_0(\mathcal T_S(A))$ with $\operatorname{Div}(A)$, that theorem identifies the localization boundary \begin{align*} \partial:K_1(F)\to K_0(\mathcal T_S(A)) \end{align*} with the homomorphism sending $x\in F^\times$ to \begin{align*} \sum_{\mathfrak p\ne 0}v_{\mathfrak p}(x)[\mathfrak p]. \end{align*} This homomorphism is exactly the divisor map $\operatorname{div}:F^\times\to \operatorname{Div}(A)$ from the theorem statement. Thus, after the above identifications, \begin{align*} \partial=\operatorname{div}:F^\times\to \operatorname{Div}(A). \end{align*} [/step]

[step:Replace the localization sequence by the divisor sequence] Substituting the identifications from the previous steps into the localization exact sequence gives an exact sequence \begin{align*} K_1(A)\longrightarrow F^\times\xrightarrow{\operatorname{div}}\operatorname{Div}(A)\longrightarrow K_0(A)\longrightarrow K_0(F)\longrightarrow 0. \end{align*} The image of $K_1(A)\to F^\times$ is $A^\times$. Indeed, the determinant map $K_1(A)\to A^\times$ followed by the inclusion $A^\times\hookrightarrow F^\times$ is the displayed map to $F^\times$. Here $GL_1(A)$ denotes the group of invertible $1\times 1$ matrices over $A$, canonically identified with $A^\times$, and every unit of $A$ is represented by the corresponding element of $GL_1(A)$. Therefore the beginning of the exact sequence may be written as \begin{align*} A^\times\longrightarrow F^\times\xrightarrow{\operatorname{div}}\operatorname{Div}(A). \end{align*} Equivalently, $\ker(\operatorname{div})=A^\times$: if $x\in F^\times$ has $v_{\mathfrak p}(x)=0$ for every nonzero prime ideal $\mathfrak p$, then the fractional ideal $xA$ has zero valuation at every nonzero prime and hence $xA=A$, so $x\in A^\times$. Thus we obtain the exact sequence \begin{align*} A^\times \longrightarrow F^\times \xrightarrow{\operatorname{div}} \operatorname{Div}(A) \longrightarrow K_0(A) \longrightarrow K_0(F) \longrightarrow 0. \end{align*} [/step]

[step:Interpret the final map as rank and identify its kernel] By the division ring computation for $K_0$ [citetheorem:8677], applied to the field $F$, there is an isomorphism \begin{align*} K_0(F)\cong \mathbb Z \end{align*} sending the class of a finite-dimensional $F$-[vector space](/page/Vector%20Space) to its dimension. For a finitely generated projective $A$-module $P$, the image of $[P]\in K_0(A)$ in $K_0(F)$ is \begin{align*} [F\otimes_A P]. \end{align*} Under $K_0(F)\cong \mathbb Z$, this class maps to \begin{align*} \dim_F(F\otimes_A P)=\operatorname{rank}(P). \end{align*} Hence $K_0(A)\to K_0(F)\cong \mathbb Z$ is the rank map. By exactness, the kernel of this rank map is the image of \begin{align*} \operatorname{Div}(A)\to K_0(A). \end{align*} Again by exactness, this image is the quotient of $\operatorname{Div}(A)$ by the image of $\operatorname{div}:F^\times\to \operatorname{Div}(A)$. The quotient \begin{align*} \operatorname{Div}(A)/\operatorname{div}(F^\times) \end{align*} is, by definition of the ideal class group of a Dedekind domain, naturally isomorphic to $\operatorname{Cl}(A)$. Therefore \begin{align*} \ker\bigl(K_0(A)\to K_0(F)\cong \mathbb Z\bigr)\cong \operatorname{Cl}(A). \end{align*} This proves both the displayed exact sequence and the asserted identification of the kernel with the ideal class group. [/step]