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.

def ModuleCat.addCommGroupObj {R : Type u} [Ring R] {J : Type v} [CategoryTheory.Category J] (F : CategoryTheory.Functor J (ModuleCat R)) (j : J) : AddCommGroup ((F.comp (CategoryTheory.forget (ModuleCat R))).obj j)

Equations

• Eq (ModuleCat.addCommGroupObj F j) (inferInstanceAs (AddCommGroup (F.obj j).carrier))

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

Equations

• Eq (ModuleCat.moduleObj F j) (inferInstanceAs (Module R (F.obj j).carrier))

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

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

Equations

• Eq (ModuleCat.sectionsSubmodule F) { carrier := (F.comp (CategoryTheory.forget (ModuleCat R))).sections, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

def ModuleCat.instAddCommMonoidElemForallObjCompForgetSections {R : Type u} [Ring R] {J : Type v} [CategoryTheory.Category J] (F : CategoryTheory.Functor J (ModuleCat R)) : AddCommMonoid (F.comp (CategoryTheory.forget (ModuleCat R))).sections.Elem

Equations

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

def ModuleCat.instModuleElemForallObjCompForgetSections {R : Type u} [Ring R] {J : Type v} [CategoryTheory.Category J] (F : CategoryTheory.Functor J (ModuleCat R)) : Module R (F.comp (CategoryTheory.forget (ModuleCat R))).sections.Elem

Equations

• Eq (ModuleCat.instModuleElemForallObjCompForgetSections F) (inferInstanceAs (Module R (Subtype fun (x : (j : J) → (F.obj j).carrier) => Membership.mem (ModuleCat.sectionsSubmodule F) x)))

theorem ModuleCat.instSmallSubtypeForallCarrierObjMemSubmoduleSectionsSubmodule {R : Type u} [Ring R] {J : Type v} [CategoryTheory.Category J] (F : CategoryTheory.Functor J (ModuleCat R)) [Small (F.comp (CategoryTheory.forget (ModuleCat R))).sections.Elem] : Small (Subtype fun (x : (j : J) → (F.obj j).carrier) => Membership.mem (sectionsSubmodule F) x)

def ModuleCat.limitAddCommMonoid {R : Type u} [Ring R] {J : Type v} [CategoryTheory.Category J] (F : CategoryTheory.Functor J (ModuleCat R)) [Small (F.comp (CategoryTheory.forget (ModuleCat R))).sections.Elem] : AddCommMonoid (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget (ModuleCat R)))).pt

Equations

• Eq (ModuleCat.limitAddCommMonoid F) (inferInstanceAs (AddCommMonoid (Shrink (Subtype fun (x : (j : J) → (F.obj j).carrier) => Membership.mem (ModuleCat.sectionsSubmodule F) x))))

def ModuleCat.limitAddCommGroup {R : Type u} [Ring R] {J : Type v} [CategoryTheory.Category J] (F : CategoryTheory.Functor J (ModuleCat R)) [Small (F.comp (CategoryTheory.forget (ModuleCat R))).sections.Elem] : AddCommGroup (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget (ModuleCat R)))).pt

Equations

• Eq (ModuleCat.limitAddCommGroup F) (inferInstanceAs (AddCommGroup (Shrink (Subtype fun (x : (j : J) → (F.obj j).carrier) => Membership.mem (ModuleCat.sectionsSubmodule F) x))))

def ModuleCat.limitModule {R : Type u} [Ring R] {J : Type v} [CategoryTheory.Category J] (F : CategoryTheory.Functor J (ModuleCat R)) [Small (F.comp (CategoryTheory.forget (ModuleCat R))).sections.Elem] : Module R (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget (ModuleCat R)))).pt

Equations

• Eq (ModuleCat.limitModule F) (inferInstanceAs (Module R (Shrink (Subtype fun (x : (j : J) → (F.obj j).carrier) => Membership.mem (ModuleCat.sectionsSubmodule F) x))))

def ModuleCat.limitπLinearMap {R : Type u} [Ring R] {J : Type v} [CategoryTheory.Category J] (F : CategoryTheory.Functor J (ModuleCat R)) [Small (F.comp (CategoryTheory.forget (ModuleCat R))).sections.Elem] (j : J) : LinearMap (RingHom.id R) (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget (ModuleCat R)))).pt ((F.comp (CategoryTheory.forget (ModuleCat R))).obj j)

limit.π (F ⋙ forget (ModuleCat.{w} R)) j as an R-linear map.

Equations

• Eq (ModuleCat.limitπLinearMap F j) { toFun := (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget (ModuleCat R)))).π.app j, map_add' := ⋯, map_smul' := ⋯ }

def ModuleCat.HasLimits.limitCone {R : Type u} [Ring R] {J : Type v} [CategoryTheory.Category J] (F : CategoryTheory.Functor J (ModuleCat R)) [Small (F.comp (CategoryTheory.forget (ModuleCat R))).sections.Elem] : 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.Category J] (F : CategoryTheory.Functor J (ModuleCat R)) [Small (F.comp (CategoryTheory.forget (ModuleCat R))).sections.Elem] : CategoryTheory.Limits.IsLimit (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.hasLimit {R : Type u} [Ring R] {J : Type v} [CategoryTheory.Category J] (F : CategoryTheory.Functor J (ModuleCat R)) [Small (F.comp (CategoryTheory.forget (ModuleCat R))).sections.Elem] : CategoryTheory.Limits.HasLimit F

If (F ⋙ forget (ModuleCat R)).sections is u-small, F has a limit.

theorem ModuleCat.hasLimitsOfShape {R : Type u} [Ring R] {J : Type v} [CategoryTheory.Category J] [Small J] : CategoryTheory.Limits.HasLimitsOfShape J (ModuleCat R)

If J is u-small, the category of R-modules has limits of shape J.

theorem ModuleCat.hasLimitsOfSize {R : Type u} [Ring R] [UnivLE] : CategoryTheory.Limits.HasLimitsOfSize (ModuleCat R)

The category of R-modules has all limits.

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

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

def ModuleCat.forget₂AddCommGroup_preservesLimitsAux {R : Type u} [Ring R] {J : Type v} [CategoryTheory.Category J] (F : CategoryTheory.Functor J (ModuleCat R)) [Small (F.comp (CategoryTheory.forget (ModuleCat R))).sections.Elem] : CategoryTheory.Limits.IsLimit ((CategoryTheory.forget₂ (ModuleCat R) AddCommGrp).mapCone (HasLimits.limitCone F))

An auxiliary declaration to speed up typechecking.

Equations

• Eq (ModuleCat.forget₂AddCommGroup_preservesLimitsAux F) (AddCommGrp.limitConeIsLimit (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrp)))

theorem ModuleCat.forget₂AddCommGroup_preservesLimit {R : Type u} [Ring R] {J : Type v} [CategoryTheory.Category J] (F : CategoryTheory.Functor J (ModuleCat R)) [Small (F.comp (CategoryTheory.forget (ModuleCat R))).sections.Elem] : CategoryTheory.Limits.PreservesLimit F (CategoryTheory.forget₂ (ModuleCat R) AddCommGrp)

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

theorem ModuleCat.forget₂AddCommGroup_preservesLimitsOfSize {R : Type u} [Ring R] [UnivLE] : CategoryTheory.Limits.PreservesLimitsOfSize (CategoryTheory.forget₂ (ModuleCat R) AddCommGrp)

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

theorem ModuleCat.forget₂AddCommGroup_preservesLimits {R : Type u} [Ring R] : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ (ModuleCat R) AddCommGrp)

theorem ModuleCat.forget_preservesLimitsOfSize {R : Type u} [Ring R] [UnivLE] : CategoryTheory.Limits.PreservesLimitsOfSize (CategoryTheory.forget (ModuleCat R))

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

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

theorem ModuleCat.forget₂AddCommGroup_reflectsLimit {R : Type u} [Ring R] {J : Type v} [CategoryTheory.Category J] (F : CategoryTheory.Functor J (ModuleCat R)) : CategoryTheory.Limits.ReflectsLimit F (CategoryTheory.forget₂ (ModuleCat R) AddCommGrp)

theorem ModuleCat.forget₂AddCommGroup_reflectsLimitOfShape {R : Type u} [Ring R] {J : Type v} [CategoryTheory.Category J] : CategoryTheory.Limits.ReflectsLimitsOfShape J (CategoryTheory.forget₂ (ModuleCat R) AddCommGrp)

theorem ModuleCat.forget₂AddCommGroup_reflectsLimitOfSize {R : Type u} [Ring R] : CategoryTheory.Limits.ReflectsLimitsOfSize (CategoryTheory.forget₂ (ModuleCat R) AddCommGrp)

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 : ι) → LE.le i j → LinearMap (RingHom.id R) (G i) (G j)) [DirectedSystem G fun (i j : ι) (h : LE.le i j) => DFunLike.coe (f i j h)] : CategoryTheory.Functor ι (ModuleCat R)

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

Equations

• Eq (ModuleCat.directLimitDiagram G f) { obj := fun (i : ι) => ModuleCat.of R (G i), map := fun {X Y : ι} (hij : Quiver.Hom X Y) => ModuleCat.ofHom (f X Y ⋯), map_id := ⋯, map_comp := ⋯ }

theorem ModuleCat.directLimitDiagram_obj_isAddCommGroup {R : Type u} [Ring R] {ι : Type v} [Preorder ι] (G : ι → Type v) [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → LE.le i j → LinearMap (RingHom.id R) (G i) (G j)) [DirectedSystem G fun (i j : ι) (h : LE.le i j) => DFunLike.coe (f i j h)] (i : ι) : Eq ((directLimitDiagram G f).obj i).isAddCommGroup (inst✝ i)

theorem ModuleCat.directLimitDiagram_obj_isModule {R : Type u} [Ring R] {ι : Type v} [Preorder ι] (G : ι → Type v) [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → LE.le i j → LinearMap (RingHom.id R) (G i) (G j)) [DirectedSystem G fun (i j : ι) (h : LE.le i j) => DFunLike.coe (f i j h)] (i : ι) : Eq ((directLimitDiagram G f).obj i).isModule (inst✝ i)

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 : ι) → LE.le i j → LinearMap (RingHom.id R) (G i) (G j)) [DirectedSystem G fun (i j : ι) (h : LE.le i j) => DFunLike.coe (f i j h)] {X✝ Y✝ : ι} (hij : Quiver.Hom X✝ Y✝) : Eq ((directLimitDiagram G f).map hij) (ofHom (f X✝ Y✝ ⋯))

theorem ModuleCat.directLimitDiagram_obj_carrier {R : Type u} [Ring R] {ι : Type v} [Preorder ι] (G : ι → Type v) [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → LE.le i j → LinearMap (RingHom.id R) (G i) (G j)) [DirectedSystem G fun (i j : ι) (h : LE.le i j) => DFunLike.coe (f i j h)] (i : ι) : Eq ((directLimitDiagram G f).obj i).carrier (G i)

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 : ι) → LE.le i j → LinearMap (RingHom.id R) (G i) (G j)) [DirectedSystem G fun (i j : ι) (h : LE.le i j) => DFunLike.coe (f i j h)] [DecidableEq ι] : CategoryTheory.Limits.Cocone (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

• Eq (ModuleCat.directLimitCocone G f) { pt := ModuleCat.of R (Module.DirectLimit G f), ι := { app := fun (x : ι) => ModuleCat.ofHom (Module.DirectLimit.of R ι G f x), naturality := ⋯ } }

theorem ModuleCat.directLimitCocone_pt_carrier {R : Type u} [Ring R] {ι : Type v} [Preorder ι] (G : ι → Type v) [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → LE.le i j → LinearMap (RingHom.id R) (G i) (G j)) [DirectedSystem G fun (i j : ι) (h : LE.le i j) => DFunLike.coe (f i j h)] [DecidableEq ι] : Eq (directLimitCocone G f).pt.carrier (Module.DirectLimit G f)

theorem ModuleCat.directLimitCocone_pt_isModule {R : Type u} [Ring R] {ι : Type v} [Preorder ι] (G : ι → Type v) [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → LE.le i j → LinearMap (RingHom.id R) (G i) (G j)) [DirectedSystem G fun (i j : ι) (h : LE.le i j) => DFunLike.coe (f i j h)] [DecidableEq ι] : Eq (directLimitCocone G f).pt.isModule (Module.DirectLimit.module G f)

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 : ι) → LE.le i j → LinearMap (RingHom.id R) (G i) (G j)) [DirectedSystem G fun (i j : ι) (h : LE.le i j) => DFunLike.coe (f i j h)] [DecidableEq ι] (x : ι) : Eq ((directLimitCocone G f).ι.app x) (ofHom (Module.DirectLimit.of R ι G f x))

theorem ModuleCat.directLimitCocone_pt_isAddCommGroup {R : Type u} [Ring R] {ι : Type v} [Preorder ι] (G : ι → Type v) [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → LE.le i j → LinearMap (RingHom.id R) (G i) (G j)) [DirectedSystem G fun (i j : ι) (h : LE.le i j) => DFunLike.coe (f i j h)] [DecidableEq ι] : Eq (directLimitCocone G f).pt.isAddCommGroup (Module.DirectLimit.addCommGroup G f)

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 : ι) → LE.le i j → LinearMap (RingHom.id R) (G i) (G j)) [DirectedSystem G fun (i j : ι) (h : LE.le i j) => DFunLike.coe (f i j h)] [DecidableEq ι] : CategoryTheory.Limits.IsColimit (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.

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 : ι) → LE.le i j → LinearMap (RingHom.id R) (G i) (G j)) [DirectedSystem G fun (i j : ι) (h : LE.le i j) => DFunLike.coe (f i j h)] [DecidableEq ι] (s : CategoryTheory.Limits.Cocone (directLimitDiagram G f)) : Eq ((directLimitIsColimit G f).desc s) (ofHom (Module.DirectLimit.lift R ι G f (fun (i : ι) => Hom.hom (s.ι.app i)) ⋯))