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.

@[simp]
theorem Module.direct_limit_diagram_obj {R : Type u} [ring R] {ι : Type v} [directed_order ι] (G : ι → Type v) [Π (i : ι), add_comm_group (G i)] [Π (i : ι), module R (G i)] (f : Π (i j : ι), i j(G i →ₗ[R] G j)) [module.directed_system G f] (i : ι) :
def Module.direct_limit_diagram {R : Type u} [ring R] {ι : Type v} [directed_order ι] (G : ι → Type v) [Π (i : ι), add_comm_group (G i)] [Π (i : ι), module R (G i)] (f : Π (i j : ι), i j(G i →ₗ[R] G j)) [module.directed_system G f] :
ι Module R

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} [directed_order ι] (G : ι → Type v) [Π (i : ι), add_comm_group (G i)] [Π (i : ι), module R (G i)] (f : Π (i j : ι), i j(G i →ₗ[R] G j)) [module.directed_system G f] (i j : ι) (hij : i j) :
@[simp]
theorem Module.direct_limit_cocone_X {R : Type u} [ring R] {ι : Type v} [directed_order ι] (G : ι → Type v) [Π (i : ι), add_comm_group (G i)] [Π (i : ι), module R (G i)] (f : Π (i j : ι), i j(G i →ₗ[R] G j)) [module.directed_system G f] [decidable_eq ι] :
def Module.direct_limit_cocone {R : Type u} [ring R] {ι : Type v} [directed_order ι] (G : ι → Type v) [Π (i : ι), add_comm_group (G i)] [Π (i : ι), module R (G i)] (f : Π (i j : ι), i j(G i →ₗ[R] G j)) [module.directed_system G f] [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} [directed_order ι] (G : ι → Type v) [Π (i : ι), add_comm_group (G i)] [Π (i : ι), module R (G i)] (f : Π (i j : ι), i j(G i →ₗ[R] G j)) [module.directed_system G f] [decidable_eq ι] (i : ι) :
def Module.direct_limit_is_colimit {R : Type u} [ring R] {ι : Type v} [directed_order ι] (G : ι → Type v) [Π (i : ι), add_comm_group (G i)] [Π (i : ι), module R (G i)] (f : Π (i j : ι), i j(G i →ₗ[R] G j)) [module.directed_system G f] [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} [directed_order ι] (G : ι → Type v) [Π (i : ι), add_comm_group (G i)] [Π (i : ι), module R (G i)] (f : Π (i j : ι), i j(G i →ₗ[R] G j)) [module.directed_system G f] [decidable_eq ι] [nonempty ι] (s : category_theory.limits.cocone (Module.direct_limit_diagram G f)) :