mathlib3 documentation

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]
Equations
@[protected, 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
@[protected, instance, irreducible]

The category of R-modules has all limits.

@[protected, instance]
@[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 : ι), module R (G i)] (f : Π (i j : ι), i j (G i →ₗ[R] G j)) [directed_system G (λ (i j : ι) (h : i j), (f i j h))] (i : ι) :
def Module.direct_limit_diagram {R : Type u} [ring R] {ι : Type v} [preorder ι] (G : ι Type v) [Π (i : ι), add_comm_group (G i)] [Π (i : ι), module R (G i)] (f : Π (i j : ι), i j (G i →ₗ[R] G j)) [directed_system G (λ (i j : ι) (h : i j), (f i j h))] :
ι 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} [preorder ι] (G : ι Type v) [Π (i : ι), add_comm_group (G i)] [Π (i : ι), module R (G i)] (f : Π (i j : ι), i j (G i →ₗ[R] G j)) [directed_system G (λ (i j : ι) (h : i j), (f i j h))] (i j : ι) (hij : 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 : ι), module R (G i)] (f : Π (i j : ι), i j (G i →ₗ[R] G j)) [directed_system G (λ (i j : ι) (h : i j), (f i j h))] [decidable_eq ι] :
def Module.direct_limit_cocone {R : Type u} [ring R] {ι : Type v} [preorder ι] (G : ι Type v) [Π (i : ι), add_comm_group (G i)] [Π (i : ι), module R (G i)] (f : Π (i j : ι), i j (G i →ₗ[R] G j)) [directed_system G (λ (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 : ι), module R (G i)] (f : Π (i j : ι), i j (G i →ₗ[R] G j)) [directed_system G (λ (i j : ι) (h : i j), (f i j h))] [decidable_eq ι] (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 : ι), module R (G i)] (f : Π (i j : ι), i j (G i →ₗ[R] G j)) [directed_system G (λ (i j : ι) (h : i j), (f i j h))] [decidable_eq ι] [nonempty ι] [is_directed ι has_le.le] :

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 : ι), module R (G i)] (f : Π (i j : ι), i j (G i →ₗ[R] G j)) [directed_system G (λ (i j : ι) (h : i j), (f i j h))] [decidable_eq ι] [nonempty ι] [is_directed ι has_le.le] (s : category_theory.limits.cocone (Module.direct_limit_diagram G f)) :