Today I encountered the following lemma:
Let A be a ring. Let u : M —> N be an A-module map. Let R = colim_i R_i be a directed colimit of A-algebras. Assume that M is a finite A-module, N is a finitely presented A-module, and u ⊗ 1 : M ⊗ R —> N ⊗ R is an isomorphism. Then there exists an i ∈ I such that u ⊗ 1 : M ⊗ R_i —> N ⊗ R_i is an isomorphism. (All tensor products over A.)
What I like about this statement is that M only needs to be a finite A-module. This is similar to what happened in this post.
The same result holds if we replace “module” with “algebra” everywhere (and “finite” with “finite type”, but leave “finitely presented” alone). In fact, it follows by the same proof (assuming your proof is the obvious one via chasing relations and using “well-posedness” of the concept of “finite presentation” in both the module and algebra settings).
Yep, you’re right. I added the fact about algebras now to the stacks project. Thanks!