A model theoretic proof for o-minimal coherence theorem

Bakker, Brunebarbe, Tsimerman showed in \cite{bakker2022minimal} that the definable structure sheaf $\mathcal{O}_{\mathbb{C}^n}$ of $\mathbb{C}^n$ is a coherent $\mathcal{O}_{\mathbb{C}^n}$-module as a sheaf on the site $\underline{\mathbb{C}^n}$, where the coverings are finite coverings by definable open sets. In general, let $\mathcal{K}$ be an algebraically closed field of characteristic zero. We give another proof of the coherence of $\mathcal{O}_{\mathcal{K}^n}$ as a sheaf of $\mathcal{O}_{\mathcal{K}^n}$-modules on the site $\underline{\mathcal{K}^n}$ using spectral topology on the type space $S_n(\mathcal{K})$. (Here $S_n(\mathcal{K})$ means $S_{2n}(\mathcal{R})$ for some real closed field $\mathcal{R}$.) It also gives an example of how the intuition that sheaves on the type space are the same as sheaves on the site with finite coverings (see \cite[Proposition~3.2]{edmundo2006sheaf}) can be applied.