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 u}
[category_theory.small_category J]
(F : J ⥤ Module R)
(j : J) :
add_comm_group ((F ⋙ category_theory.forget (Module R)).obj j)
Equations
- Module.add_comm_group_obj F j = id (F.obj j).is_add_comm_group
@[instance]
def
Module.module_obj
{R : Type u}
[ring R]
{J : Type u}
[category_theory.small_category J]
(F : J ⥤ Module R)
(j : J) :
module R ((F ⋙ category_theory.forget (Module R)).obj j)
Equations
- Module.module_obj F j = id (F.obj j).is_module
def
Module.sections_submodule
{R : Type u}
[ring R]
{J : Type u}
[category_theory.small_category J]
(F : J ⥤ Module R) :
The flat sections of a functor into Module R form a submodule of all sections.
@[instance]
def
Module.limit_add_comm_group
{R : Type u}
[ring R]
{J : Type u}
[category_theory.small_category J]
(F : J ⥤ Module R) :
Equations
@[instance]
def
Module.limit_module
{R : Type u}
[ring R]
{J : Type u}
[category_theory.small_category J]
(F : J ⥤ Module R) :
module R (category_theory.limits.limit (F ⋙ category_theory.forget (Module R)))
Equations
def
Module.limit_π_linear_map
{R : Type u}
[ring R]
{J : Type u}
[category_theory.small_category J]
(F : J ⥤ Module R)
(j : J) :
category_theory.limits.limit (F ⋙ category_theory.forget (Module R)) →ₗ[R] (F ⋙ category_theory.forget (Module R)).obj j
limit.π (F ⋙ forget Ring) j as a ring_hom.
Equations
- Module.limit_π_linear_map F j = {to_fun := category_theory.limits.limit.π (F ⋙ category_theory.forget (Module R)) j, map_add' := _, map_smul' := _}
def
Module.has_limits.limit
{R : Type u}
[ring R]
{J : Type u}
[category_theory.small_category J]
(F : J ⥤ Module R) :
Construction of a limit cone in Module R.
(Internal use only; use the limits API.)
Equations
- Module.has_limits.limit F = {X := Module.of R (category_theory.limits.limit (F ⋙ category_theory.forget (Module R))) (Module.limit_module F), π := {app := Module.limit_π_linear_map F, naturality' := _}}
def
Module.has_limits.limit_is_limit
{R : Type u}
[ring R]
{J : Type u}
[category_theory.small_category J]
(F : J ⥤ Module R) :
Witness that the limit cone in Module R is a limit cone.
(Internal use only; use the limits API.)
Equations
- Module.has_limits.limit_is_limit F = category_theory.limits.is_limit.of_faithful (category_theory.forget (Module R)) (category_theory.limits.limit.is_limit (F ⋙ category_theory.forget (Module R))) (λ (s : category_theory.limits.cone F), {to_fun := λ (v : ((category_theory.forget (Module R)).map_cone s).X), ⟨λ (j : J), ((category_theory.forget (Module R)).map_cone s).π.app j v, _⟩, map_add' := _, map_smul' := _}) _
@[instance]
The category of R-modules has all limits.
Equations
- Module.has_limits = {has_limits_of_shape := λ (J : Type u) (𝒥 : category_theory.small_category J), {has_limit := λ (F : J ⥤ Module R), {cone := Module.has_limits.limit F, is_limit := Module.has_limits.limit_is_limit F}}}
@[instance]
The forgetful functor from R-modules to abelian groups preserves all limits.
Equations
- Module.forget₂_AddCommGroup_preserves_limits = {preserves_limits_of_shape := λ (J : Type u) (𝒥 : category_theory.small_category J), {preserves_limit := λ (F : J ⥤ Module R), category_theory.limits.preserves_limit_of_preserves_limit_cone (category_theory.limits.limit.is_limit F) (category_theory.limits.limit.is_limit (F ⋙ category_theory.forget₂ (Module R) AddCommGroup))}}
@[instance]
The forgetful functor from R-modules to types preserves all limits.
Equations
- Module.forget_preserves_limits = {preserves_limits_of_shape := λ (J : Type u) (𝒥 : category_theory.small_category J), {preserves_limit := λ (F : J ⥤ Module R), category_theory.limits.preserves_limit_of_preserves_limit_cone (category_theory.limits.limit.is_limit F) (category_theory.limits.limit.is_limit (F ⋙ category_theory.forget (Module R)))}}