Finite generation from finitely many principal localizations (source code)

= Finite generation from finitely many principal localizations

Suppose a $k$-algebra $A$ has elements $f_i,g_i$ with $\sum_i g_if_i=1$, and each $A_{f_i}$ is a <finitely generated algebra>. Let $B\subseteq A$ contain the $f_i,g_i$ and numerators of finite generating sets of all $A_{f_i}$. Then $B$ is finitely generated and $B_{f_i}=A_{f_i}$. For $a\in A$, clear denominators so that all $f_i^Na$ belong to $B$. A <unit-ideal identity for powers> gives $1=\sum_i c_if_i^N$ in $B$, hence $a=\sum_i c_i f_i^Na\in B$. Thus $A=B$.