The category of R-algebras 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 AlgebraCat R
form a submodule of all sections.
Instances For
limit.π (F ⋙ forget (AlgebraCat R)) j
as a AlgHom
.
Instances For
Construction of a limit cone in AlgebraCat R
.
(Internal use only; use the limits API.)
Instances For
Witness that the limit cone in AlgebraCat R
is a limit cone.
(Internal use only; use the limits API.)
Instances For
The category of R-algebras has all limits.
The forgetful functor from R-algebras to rings preserves all limits.
The forgetful functor from R-algebras to R-modules preserves all limits.
The forgetful functor from R-algebras to types preserves all limits.