# mathlib3documentation

algebra.category.Module.limits

# The category of R-modules has all limits #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Further, these limits are preserved by the forgetful functor --- that is, the underlying types are just the limits in the category of types.

@[protected, instance]
def Module.add_comm_group_obj {R : Type u} [ring R] {J : Type v} (F : J ) (j : J) :
Equations
@[protected, instance]
def Module.module_obj {R : Type u} [ring R] {J : Type v} (F : J ) (j : J) :
((F .obj j)
Equations
def Module.sections_submodule {R : Type u} [ring R] {J : Type v} (F : J ) :
(Π (j : J), (F.obj j))

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

Equations
@[protected, instance]
def Module.limit_add_comm_monoid {R : Type u} [ring R] {J : Type v} (F : J ) :
Equations
@[protected, instance]
def Module.limit_add_comm_group {R : Type u} [ring R] {J : Type v} (F : J ) :
Equations
@[protected, instance]
def Module.limit_module {R : Type u} [ring R] {J : Type v} (F : J ) :
Equations
• = show , from
def Module.limit_π_linear_map {R : Type u} [ring R] {J : Type v} (F : J ) (j : J) :
→ₗ[R] (F .obj j

limit.π (F ⋙ forget Ring) j as a ring_hom.

Equations
def Module.has_limits.limit_cone {R : Type u} [ring R] {J : Type v} (F : J ) :

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

Equations
def Module.has_limits.limit_cone_is_limit {R : Type u} [ring R] {J : Type v} (F : J ) :

Witness that the limit cone in Module R is a limit cone. (Internal use only; use the limits API.)

Equations
@[protected, instance, irreducible]
def Module.has_limits_of_size {R : Type u} [ring R] :

The category of R-modules has all limits.

@[protected, instance]
def Module.has_limits {R : Type u} [ring R] :
noncomputable def Module.forget₂_AddCommGroup_preserves_limits_aux {R : Type u} [ring R] {J : Type v} (F : J ) :

An auxiliary declaration to speed up typechecking.

Equations
@[protected, instance]

The forgetful functor from R-modules to abelian groups preserves all limits.

Equations
@[protected, instance]
noncomputable def Module.forget₂_AddCommGroup_preserves_limits {R : Type u} [ring R] :
Equations
@[protected, instance]

The forgetful functor from R-modules to types preserves all limits.

Equations
@[protected, instance]
Equations
@[simp]
theorem Module.direct_limit_diagram_obj {R : Type u} [ring R] {ι : Type v} [preorder ι] (G : ι Type v) [Π (i : ι), add_comm_group (G i)] [Π (i : ι), (G i)] (f : Π (i j : ι), i j (G i →ₗ[R] G j)) [ (λ (i j : ι) (h : i j), (f i j h))] (i : ι) :
i = (G i)
def Module.direct_limit_diagram {R : Type u} [ring R] {ι : Type v} [preorder ι] (G : ι Type v) [Π (i : ι), add_comm_group (G i)] [Π (i : ι), (G i)] (f : Π (i j : ι), i j (G i →ₗ[R] G j)) [ (λ (i j : ι) (h : i j), (f i j h))] :
ι

The diagram (in the sense of category_theory) of an unbundled direct_limit of modules.

Equations
@[simp]
theorem Module.direct_limit_diagram_map {R : Type u} [ring R] {ι : Type v} [preorder ι] (G : ι Type v) [Π (i : ι), add_comm_group (G i)] [Π (i : ι), (G i)] (f : Π (i j : ι), i j (G i →ₗ[R] G j)) [ (λ (i j : ι) (h : i j), (f i j h))] (i j : ι) (hij : i j) :
hij = f i j _
@[simp]
theorem Module.direct_limit_cocone_X {R : Type u} [ring R] {ι : Type v} [preorder ι] (G : ι Type v) [Π (i : ι), add_comm_group (G i)] [Π (i : ι), (G i)] (f : Π (i j : ι), i j (G i →ₗ[R] G j)) [ (λ (i j : ι) (h : i j), (f i j h))] [decidable_eq ι] :
.X = f)
def Module.direct_limit_cocone {R : Type u} [ring R] {ι : Type v} [preorder ι] (G : ι Type v) [Π (i : ι), add_comm_group (G i)] [Π (i : ι), (G i)] (f : Π (i j : ι), i j (G i →ₗ[R] G j)) [ (λ (i j : ι) (h : i j), (f i j h))] [decidable_eq ι] :

The cocone on direct_limit_diagram corresponding to the unbundled direct_limit of modules.

In direct_limit_is_colimit we show that it is a colimit cocone.

Equations
@[simp]
theorem Module.direct_limit_cocone_ι_app {R : Type u} [ring R] {ι : Type v} [preorder ι] (G : ι Type v) [Π (i : ι), add_comm_group (G i)] [Π (i : ι), (G i)] (f : Π (i j : ι), i j (G i →ₗ[R] G j)) [ (λ (i j : ι) (h : i j), (f i j h))] [decidable_eq ι] (i : ι) :
.ι.app i = f i
def Module.direct_limit_is_colimit {R : Type u} [ring R] {ι : Type v} [preorder ι] (G : ι Type v) [Π (i : ι), add_comm_group (G i)] [Π (i : ι), (G i)] (f : Π (i j : ι), i j (G i →ₗ[R] G j)) [ (λ (i j : ι) (h : i j), (f i j h))] [decidable_eq ι] [nonempty ι]  :

The unbundled direct_limit of modules is a colimit in the sense of category_theory.

Equations
@[simp]
theorem Module.direct_limit_is_colimit_desc {R : Type u} [ring R] {ι : Type v} [preorder ι] (G : ι Type v) [Π (i : ι), add_comm_group (G i)] [Π (i : ι), (G i)] (f : Π (i j : ι), i j (G i →ₗ[R] G j)) [ (λ (i j : ι) (h : i j), (f i j h))] [decidable_eq ι] [nonempty ι]  :
= f s.ι.app _