Commit 2025-07-16 13:02 e1097802

feat(RingTheory/TensorProduct/FG) : direct limit properties of tensor products wrt finitely generated submodules (#26717) This PR uses the fact that a module is the directed limit of its finitely generated submodules to establish various existence properties of finitely generated submodules wrt tensor products. For any element u : M ⊗[R] N, there exists a finitely generated submodule P of M and an element t : P ⊗[R] N whose image in M ⊗[R] N is equal to u. For t : P ⊗[R] N and t' : P' ⊗[R] N as above, there exists a finitely generated submodule Q of M containing P ⊔ P' such that the images of t and t' in Q ⊗[R] N coincide. Similar results for base change, where M is replaced by an R-algebra A, and P, P', Q by finitely generated subalgebras of A.