The category of R-modules has all limits #
Further, these limits are preserved by the forgetful functor --- that is, the underlying types are just the limits in the category of types.
The flat sections of a functor into ModuleCat R
form a submodule of all sections.
Instances For
limit.π (F ⋙ forget Ring) j
as a RingHom
.
Instances For
Construction of a limit cone in ModuleCat R
.
(Internal use only; use the limits API.)
Instances For
Witness that the limit cone in ModuleCat R
is a limit cone.
(Internal use only; use the limits API.)
Instances For
The category of R-modules has all limits.
An auxiliary declaration to speed up typechecking.
Instances For
The forgetful functor from R-modules to abelian groups preserves all limits.
The forgetful functor from R-modules to types preserves all limits.
The diagram (in the sense of CategoryTheory
)
of an unbundled directLimit
of modules.
Instances For
The Cocone
on directLimitDiagram
corresponding to
the unbundled directLimit
of modules.
In directLimitIsColimit
we show that it is a colimit cocone.
Instances For
The unbundled directLimit
of modules is a colimit
in the sense of CategoryTheory
.