Module of finite presentation and categorical def

Stream: mathlib4

[Liran Shaul]

I have a commutative ring R, and a Module.FinitePresentation R P. I would like to deduce that IsFinitelyPresentable.{u} (ModuleCat.of R P). Is there a result in mathlib that says it? thank you.

[Robin Carlier]

I’m afraid mathlib only has the result for algebras and not for module (loogling for |- CategoryTheory.IsFinitelyPresentable _ only yields docs#isFinitelyPresentable, which for some reason is not in any namespace).

[Robin Carlier]

(by proving first that the free module of rank one is finitely presentable in the categorical sense, mathlib knows that finitely presentable objects are stable under finite colimits (through the results in Mathlib.CategoryTheory.Presentable.Limits), so from there one should probably be able to get the result from docs#Module.finitePresentation_iff_exists_presentation, but I bet there will be some missing glue in that plan.)

[Joël Riou]

docs#CategoryTheory.isCardinalPresentable_of_isColimit implies that finitely presentable objects are stable under finite colimits. In particular, they are stable under cokernels (and finite coproducts). It follows that it suffices to show that R as a module over itself is finitely presentable, which is easy.