# Documentation

Mathlib.Algebra.Category.ModuleCat.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 ModuleCat.addCommGroupObj {R : Type u} [Ring R] {J : Type v} (F : ) (j : J) :
instance ModuleCat.moduleObj {R : Type u} [Ring R] {J : Type v} (F : ) (j : J) :
Module R (().obj j)
def ModuleCat.sectionsSubmodule {R : Type u} [Ring R] {J : Type v} (F : ) :
Submodule R ((j : J) → ↑(F.obj j))

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

Instances For
instance ModuleCat.limitAddCommMonoid {R : Type u} [Ring R] {J : Type v} (F : ) :
instance ModuleCat.limitAddCommGroup {R : Type u} [Ring R] {J : Type v} (F : ) :
instance ModuleCat.limitModule {R : Type u} [Ring R] {J : Type v} (F : ) :
def ModuleCat.limitπLinearMap {R : Type u} [Ring R] {J : Type v} (F : ) (j : J) :

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

Instances For
def ModuleCat.HasLimits.limitCone {R : Type u} [Ring R] {J : Type v} (F : ) :

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

Instances For
def ModuleCat.HasLimits.limitConeIsLimit {R : Type u} [Ring R] {J : Type v} (F : ) :

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

Instances For
theorem ModuleCat.hasLimitsOfSize {R : Type u} [Ring R] :

The category of R-modules has all limits.

instance ModuleCat.hasLimits {R : Type u} [Ring R] :
instance ModuleCat.hasLimits' {R : Type u} [Ring R] :

An auxiliary declaration to speed up typechecking.

Instances For

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

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

@[simp]
theorem ModuleCat.directLimitDiagram_obj {R : Type u} [Ring R] {ι : Type v} [] (G : ιType v) [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i jG i →ₗ[R] G j) [DirectedSystem G fun i j h => ↑(f i j h)] (i : ι) :
().obj i = ModuleCat.of R (G i)
@[simp]
theorem ModuleCat.directLimitDiagram_map {R : Type u} [Ring R] {ι : Type v} [] (G : ιType v) [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i jG i →ₗ[R] G j) [DirectedSystem G fun i j h => ↑(f i j h)] :
∀ {X Y : ι} (hij : X Y), ().map hij = f X Y (_ : X Y)
def ModuleCat.directLimitDiagram {R : Type u} [Ring R] {ι : Type v} [] (G : ιType v) [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i jG i →ₗ[R] G j) [DirectedSystem G fun i j h => ↑(f i j h)] :

The diagram (in the sense of CategoryTheory) of an unbundled directLimit of modules.

Instances For
@[simp]
theorem ModuleCat.directLimitCocone_ι_app {R : Type u} [Ring R] {ι : Type v} [] (G : ιType v) [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i jG i →ₗ[R] G j) [DirectedSystem G fun i j h => ↑(f i j h)] [] (i : ι) :
().ι.app i =
@[simp]
theorem ModuleCat.directLimitCocone_pt {R : Type u} [Ring R] {ι : Type v} [] (G : ιType v) [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i jG i →ₗ[R] G j) [DirectedSystem G fun i j h => ↑(f i j h)] [] :
().pt =
def ModuleCat.directLimitCocone {R : Type u} [Ring R] {ι : Type v} [] (G : ιType v) [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i jG i →ₗ[R] G j) [DirectedSystem G fun i j h => ↑(f i j h)] [] :

The Cocone on directLimitDiagram corresponding to the unbundled directLimit of modules.

In directLimitIsColimit we show that it is a colimit cocone.

Instances For
@[simp]
theorem ModuleCat.directLimitIsColimit_desc {R : Type u} [Ring R] {ι : Type v} [] (G : ιType v) [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i jG i →ₗ[R] G j) [DirectedSystem G fun i j h => ↑(f i j h)] [] [] [IsDirected ι fun x x_1 => x x_1] :
= Module.DirectLimit.lift R ι G f s.app (_ : ∀ (i j : ι) (h : i j) (x : G i), ↑(s.app j) (↑(f i j h) x) = ↑(s.app i) x)
def ModuleCat.directLimitIsColimit {R : Type u} [Ring R] {ι : Type v} [] (G : ιType v) [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i jG i →ₗ[R] G j) [DirectedSystem G fun i j h => ↑(f i j h)] [] [] [IsDirected ι fun x x_1 => x x_1] :

The unbundled directLimit of modules is a colimit in the sense of CategoryTheory.

Instances For