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.

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

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.

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

        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.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 : ι) → i jG i →ₗ[R] G j) [DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] (i : ι) :
          ((directLimitDiagram G f).obj i) = 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 jG i →ₗ[R] G j) [DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] {X✝ Y✝ : ι} (hij : X✝ Y✝) :
          (directLimitDiagram G f).map hij = ofHom (f X✝ Y✝ )
          @[simp]
          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 : ι) → i jG i →ₗ[R] G j) [DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] (i : ι) :
          @[simp]
          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 : ι) → i jG i →ₗ[R] G j) [DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] (i : ι) :
          ((directLimitDiagram G f).obj i).isModule = inst✝ 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.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 ι] (x : ι) :
            @[simp]
            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 : ι) → i jG i →ₗ[R] G j) [DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] [DecidableEq ι] :
            @[simp]
            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 : ι) → i jG i →ₗ[R] G j) [DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] [DecidableEq ι] :
            @[simp]
            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 : ι) → i jG i →ₗ[R] G j) [DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] [DecidableEq ι] :
            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 ι] :

            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
              @[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 ι] (s : CategoryTheory.Limits.Cocone (directLimitDiagram G f)) :
              (directLimitIsColimit G f).desc s = ofHom (Module.DirectLimit.lift R ι G f (fun (i : ι) => Hom.hom (s.ι.app i)) )