Commit 2024-07-03 06:10 4900904c
View on Github →feat: the forget functor from ModuleCat to AddCommGrp reflects all limits (#14283) The forget functor from the category of modules to abelian groups reflects all limits (regardless of universes). This may reduce universe assumptions in #14254. This contribution was created as part of the AIM workshop "Formalizing algebraic geometry" in June 2024.