Commit 2025-01-02 19:57 cc5b32e6

feat(Algebra/Colimit): the directed system of finitely generated submodules (#20264) We show that every module is the direct limit of its finitely generated submodules. As a consequence of this and the fact that tensor products preserves colimits, we show that if M and P are arbitrary modules and N is a finitely generated submodule of a module P, then two elements of N ⊗ M have the same image in P ⊗ M if and only if they already have the same image in N' ⊗ M for some finitely generated submodule N' ≥ N. This is the theorem Submodule.FG.exists_rTensor_fg_inclusion_eq.