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}
[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
@[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) :
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 v}
[category_theory.small_category J]
(F : J ⥤ Module R) :
The flat sections of a functor into Module R form a submodule of all sections.
@[protected, instance]
def
Module.limit_add_comm_monoid
{R : Type u}
[ring R]
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ Module R) :
Equations
@[protected, instance]
def
Module.limit_add_comm_group
{R : Type u}
[ring R]
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ Module R) :
Equations
@[protected, instance]
def
Module.limit_module
{R : Type u}
[ring R]
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ Module R) :
Equations
- Module.limit_module F = show module R ↥(Module.sections_submodule F), from (Module.sections_submodule F).module
def
Module.limit_π_linear_map
{R : Type u}
[ring R]
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ Module R)
(j : J) :
(category_theory.limits.types.limit_cone (F ⋙ category_theory.forget (Module R))).X →ₗ[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.types.limit_cone (F ⋙ category_theory.forget (Module R))).π.app j, map_add' := _, map_smul' := _}
def
Module.has_limits.limit_cone
{R : Type u}
[ring R]
{J : Type v}
[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_cone F = {X := Module.of R (category_theory.limits.types.limit_cone (F ⋙ category_theory.forget (Module R))).X (Module.limit_module F), π := {app := Module.limit_π_linear_map F, naturality' := _}}
def
Module.has_limits.limit_cone_is_limit
{R : Type u}
[ring R]
{J : Type v}
[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_cone_is_limit F = category_theory.limits.is_limit.of_faithful (category_theory.forget (Module R)) (category_theory.limits.types.limit_cone_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' := _}) _
@[protected, instance, irreducible]
The category of R-modules has all limits.
@[protected, instance]
noncomputable
def
Module.forget₂_AddCommGroup_preserves_limits_aux
{R : Type u}
[ring R]
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ Module R) :
An auxiliary declaration to speed up typechecking.
@[protected, instance]
The forgetful functor from R-modules to abelian groups preserves all limits.
Equations
- Module.forget₂_AddCommGroup_preserves_limits_of_size = {preserves_limits_of_shape := λ (J : Type v) (𝒥 : category_theory.category J), {preserves_limit := λ (F : J ⥤ Module R), category_theory.limits.preserves_limit_of_preserves_limit_cone (Module.has_limits.limit_cone_is_limit F) (Module.forget₂_AddCommGroup_preserves_limits_aux F)}}
@[protected, instance]
@[protected, instance]
The forgetful functor from R-modules to types preserves all limits.
Equations
- Module.forget_preserves_limits_of_size = {preserves_limits_of_shape := λ (J : Type v) (𝒥 : category_theory.category J), {preserves_limit := λ (F : J ⥤ Module R), category_theory.limits.preserves_limit_of_preserves_limit_cone (Module.has_limits.limit_cone_is_limit F) (category_theory.limits.types.limit_cone_is_limit (F ⋙ category_theory.forget (Module R)))}}
@[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 : ι) :
(Module.direct_limit_diagram G f).obj i = Module.of R (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 : ι), 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))] :
The diagram (in the sense of category_theory)
of an unbundled direct_limit of modules.
@[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) :
(Module.direct_limit_diagram G f).map 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 : ι), 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 ι] :
(Module.direct_limit_cocone G f).X = Module.of R (module.direct_limit G f)
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
- Module.direct_limit_cocone G f = {X := Module.of R (module.direct_limit G f) (module.direct_limit.module G f), ι := {app := module.direct_limit.of R ι G f, naturality' := _}}
@[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 : ι) :
(Module.direct_limit_cocone G f).ι.app i = module.direct_limit.of R ι G 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 : ι), 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
- Module.direct_limit_is_colimit G f = {desc := λ (s : category_theory.limits.cocone (Module.direct_limit_diagram G f)), module.direct_limit.lift R ι G f s.ι.app _, fac' := _, uniq' := _}
@[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)) :
(Module.direct_limit_is_colimit G f).desc s = module.direct_limit.lift R ι G f s.ι.app _