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.moduleObj {R : Type u} [Ring R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (ModuleCat R)) (j : J) :
Module R ((F.comp (CategoryTheory.forget (ModuleCat R))).obj j)
Equations
def ModuleCat.sectionsSubmodule {R : Type u} [Ring R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (ModuleCat R)) :
Submodule R ((j : J) → (F.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.
Instances For

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

    Equations
    Instances For

      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.
      Instances For

        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.
        Instances For

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

          Equations
          • =

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

          @[instance 10000]
          Equations
          • =

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

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

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

          Equations
          • One or more equations did not get rendered due to their size.
          Equations
          • ModuleCat.forget₂AddCommGroupPreservesLimits = ModuleCat.forget₂AddCommGroupPreservesLimitsOfSize

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

          Equations
          • One or more equations did not get rendered due to their size.
          Equations
          • ModuleCat.forgetPreservesLimits = ModuleCat.forgetPreservesLimitsOfSize
          Equations
          • One or more equations did not get rendered due to their size.
          Equations
          Equations
          @[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 jG i →ₗ[R] G j) [DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] (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 jG 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).map hij = f 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 jG i →ₗ[R] G j) [DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] :

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

          Equations
          Instances For
            @[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 jG i →ₗ[R] G j) [DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] [DecidableEq ι] :
            @[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 jG i →ₗ[R] G j) [DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] [DecidableEq ι] (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 : ι) → i jG i →ₗ[R] G j) [DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] [DecidableEq ι] :

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

            In directLimitIsColimit we show that it is a colimit cocone.

            Equations
            Instances For
              @[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 jG 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
              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 jG 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] :

              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.
              Instances For