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} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J (ModuleCatMax R)) (j : J) : AddCommGroup ((CategoryTheory.Functor.comp F (CategoryTheory.forget (ModuleCat R))).toPrefunctor.obj j)

Equations

• ModuleCat.addCommGroupObj F j = let_fun this := inferInstance; this

instance ModuleCat.moduleObj {R : Type u} [Ring R] {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J (ModuleCatMax R)) (j : J) : Module R ((CategoryTheory.Functor.comp F (CategoryTheory.forget (ModuleCat R))).toPrefunctor.obj j)

Equations

• ModuleCat.moduleObj F j = let_fun this := inferInstance; this

def ModuleCat.sectionsSubmodule {R : Type u} [Ring R] {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J (ModuleCatMax R)) : Submodule R ((j : J) → ↑(F.toPrefunctor.obj j))

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

Equations

• One or more equations did not get rendered due to their size.

instance ModuleCat.limitAddCommMonoid {R : Type u} [Ring R] {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J (ModuleCatMax R)) : AddCommMonoid (CategoryTheory.Limits.Types.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget (ModuleCatMax R)))).pt

Equations

• ModuleCat.limitAddCommMonoid F = let_fun this := inferInstance; this

instance ModuleCat.limitAddCommGroup {R : Type u} [Ring R] {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J (ModuleCatMax R)) : AddCommGroup (CategoryTheory.Limits.Types.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget (ModuleCatMax R)))).pt

Equations

• ModuleCat.limitAddCommGroup F = let_fun this := inferInstance; this

instance ModuleCat.limitModule {R : Type u} [Ring R] {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J (ModuleCatMax R)) : Module R (CategoryTheory.Limits.Types.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget (ModuleCat R)))).pt

Equations

• ModuleCat.limitModule F = let_fun this := inferInstance; this

def ModuleCat.limitπLinearMap {R : Type u} [Ring R] {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J (ModuleCatMax R)) (j : J) : (CategoryTheory.Limits.Types.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget (ModuleCat R)))).pt →ₗ[R] (CategoryTheory.Functor.comp F (CategoryTheory.forget (ModuleCat R))).toPrefunctor.obj j

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

Equations

• One or more equations did not get rendered due to their size.

def ModuleCat.HasLimits.limitCone {R : Type u} [Ring R] {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J (ModuleCatMax R)) : CategoryTheory.Limits.Cone F

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

Equations

• One or more equations did not get rendered due to their size.

def ModuleCat.HasLimits.limitConeIsLimit {R : Type u} [Ring R] {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J (ModuleCatMax R)) : CategoryTheory.Limits.IsLimit (ModuleCat.HasLimits.limitCone F)

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

Equations

• One or more equations did not get rendered due to their size.

theorem ModuleCat.hasLimitsOfSize {R : Type u} [Ring R] : CategoryTheory.Limits.HasLimitsOfSize.{v, v, max v w, max (max u (v + 1)) (w + 1)} (ModuleCatMax R)

The category of R-modules has all limits.

instance ModuleCat.hasLimits {R : Type u} [Ring R] : CategoryTheory.Limits.HasLimits (ModuleCat R)

Equations

• (_ : CategoryTheory.Limits.HasLimits (ModuleCat R)) = (_ : CategoryTheory.Limits.HasLimitsOfSize.{w, w, w, max u (w + 1)} (ModuleCatMax R))

instance ModuleCat.hasLimits' {R : Type u} [Ring R] : CategoryTheory.Limits.HasLimits (ModuleCat R)

Equations

• (_ : CategoryTheory.Limits.HasLimits (ModuleCat R)) = (_ : CategoryTheory.Limits.HasLimitsOfSize.{u, u, u, u + 1} (ModuleCatMax R))

def ModuleCat.forget₂AddCommGroupPreservesLimitsAux {R : Type u} [Ring R] {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J (ModuleCatMax R)) : CategoryTheory.Limits.IsLimit ((CategoryTheory.forget₂ (ModuleCat R) AddCommGroupCat).mapCone (ModuleCat.HasLimits.limitCone F))

An auxiliary declaration to speed up typechecking.

Equations

• ModuleCat.forget₂AddCommGroupPreservesLimitsAux F = AddCommGroupCat.limitConeIsLimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ (ModuleCatMax R) AddCommGroupCat))

instance ModuleCat.forget₂AddCommGroupPreservesLimitsOfSize {R : Type u} [Ring R] : CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, max v w, max v w, max (max u (v + 1)) (w + 1), max (v + 1) (w + 1)} (CategoryTheory.forget₂ (ModuleCatMax R) AddCommGroupCat)

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

Equations

• ModuleCat.forget₂AddCommGroupPreservesLimitsOfSize = CategoryTheory.Limits.PreservesLimitsOfSize.mk

instance ModuleCat.forget₂AddCommGroupPreservesLimits {R : Type u} [Ring R] : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ (ModuleCat R) AddCommGroupCat)

Equations

• ModuleCat.forget₂AddCommGroupPreservesLimits = ModuleCat.forget₂AddCommGroupPreservesLimitsOfSize

instance ModuleCat.forgetPreservesLimitsOfSize {R : Type u} [Ring R] : CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, max v w, max v w, max (max u (v + 1)) (w + 1), max (v + 1) (w + 1)} (CategoryTheory.forget (ModuleCatMax R))

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

Equations

• ModuleCat.forgetPreservesLimitsOfSize = CategoryTheory.Limits.PreservesLimitsOfSize.mk

instance ModuleCat.forgetPreservesLimits {R : Type u} [Ring R] : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget (ModuleCat R))

Equations

• ModuleCat.forgetPreservesLimits = ModuleCat.forgetPreservesLimitsOfSize

@[simp]

theorem ModuleCat.directLimitDiagram_obj {R : Type u} [Ring R] {ι : Type v} [Preorder ι] (G : ι → Type v) [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)] (i : ι) : (ModuleCat.directLimitDiagram G f).toPrefunctor.obj i = ModuleCat.of R (G i)

@[simp]

theorem ModuleCat.directLimitDiagram_map {R : Type u} [Ring R] {ι : Type v} [Preorder ι] (G : ι → Type v) [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)] : ∀ {X Y : ι} (hij : X ⟶ Y), (ModuleCat.directLimitDiagram G f).toPrefunctor.map hij = f X Y (_ : X ≤ Y)

def ModuleCat.directLimitDiagram {R : Type u} [Ring R] {ι : Type v} [Preorder ι] (G : ι → Type v) [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)] : CategoryTheory.Functor ι (ModuleCat R)

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

Equations

• ModuleCat.directLimitDiagram G f = CategoryTheory.Functor.mk { obj := fun (i : ι) => ModuleCat.of R (G i), map := fun {X Y : ι} (hij : X ⟶ Y) => f X Y (_ : X ≤ Y) }

@[simp]

theorem ModuleCat.directLimitCocone_ι_app {R : Type u} [Ring R] {ι : Type v} [Preorder ι] (G : ι → Type v) [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)] [DecidableEq ι] (i : ι) : (ModuleCat.directLimitCocone G f).ι.app i = Module.DirectLimit.of R ι G f i

@[simp]

theorem ModuleCat.directLimitCocone_pt {R : Type u} [Ring R] {ι : Type v} [Preorder ι] (G : ι → Type v) [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)] [DecidableEq ι] : (ModuleCat.directLimitCocone G f).pt = ModuleCat.of R (Module.DirectLimit G f)

def ModuleCat.directLimitCocone {R : Type u} [Ring R] {ι : Type v} [Preorder ι] (G : ι → Type v) [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)] [DecidableEq ι] : CategoryTheory.Limits.Cocone (ModuleCat.directLimitDiagram G f)

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

In directLimitIsColimit we show that it is a colimit cocone.

Equations

• ModuleCat.directLimitCocone G f = { pt := ModuleCat.of R (Module.DirectLimit G f), ι := CategoryTheory.NatTrans.mk (Module.DirectLimit.of R ι G f) }

@[simp]

theorem ModuleCat.directLimitIsColimit_desc {R : Type u} [Ring R] {ι : Type v} [Preorder ι] (G : ι → Type v) [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)] [DecidableEq ι] [IsDirected ι fun (x x_1 : ι) => x ≤ x_1] (s : CategoryTheory.Limits.Cocone (ModuleCat.directLimitDiagram G f)) : (ModuleCat.directLimitIsColimit G f).desc s = 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} [Preorder ι] (G : ι → Type v) [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)] [DecidableEq ι] [IsDirected ι fun (x x_1 : ι) => x ≤ x_1] : CategoryTheory.Limits.IsColimit (ModuleCat.directLimitCocone G f)

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

Equations

• One or more equations did not get rendered due to their size.