mathlib documentation

algebra.category.Module.limits

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.

@[instance]
def Module.add_comm_group_obj {R : Type u} [ring R] {J : Type v} [category_theory.small_category J] (F : J Module R) (j : J) :

Equations
@[instance]
def Module.module_obj {R : Type u} [ring R] {J : Type v} [category_theory.small_category J] (F : J Module R) (j : J) :

Equations
def Module.sections_submodule {R : Type u} [ring R] {J : Type v} [category_theory.small_category J] (F : J Module R) :
submodule R (Π (j : J), (F.obj j))

The flat sections of a functor into Module R form a submodule of all sections.

Equations

Construction of a limit cone in Module R. (Internal use only; use the limits API.)

Equations
@[instance]

The category of R-modules has all limits.