Documentation

Mathlib.Algebra.Category.ModuleCat.Images

The category of R-modules has images. #

Note that we don't need to register any of the constructions here as instances, because we get them from the fact that ModuleCat R is an abelian category.

def ModuleCat.image {R : Type u} [Ring R] {G : ModuleCat R} {H : ModuleCat R} (f : G H) :

The image of a morphism in ModuleCat R is just the bundling of LinearMap.range f

Instances For
    def ModuleCat.image.ι {R : Type u} [Ring R] {G : ModuleCat R} {H : ModuleCat R} (f : G H) :

    The inclusion of image f into the target

    Instances For
      def ModuleCat.factorThruImage {R : Type u} [Ring R] {G : ModuleCat R} {H : ModuleCat R} (f : G H) :

      The corestriction map to the image

      Instances For
        noncomputable def ModuleCat.image.lift {R : Type u} [Ring R] {G : ModuleCat R} {H : ModuleCat R} {f : G H} (F' : CategoryTheory.Limits.MonoFactorisation f) :

        The universal property for the image factorisation

        Instances For

          The factorisation of any morphism in ModuleCat R through a mono.

          Instances For
            noncomputable def ModuleCat.isImage {R : Type u} [Ring R] {G : ModuleCat R} {H : ModuleCat R} (f : G H) :

            The factorisation of any morphism in ModuleCat R through a mono has the universal property of the image.

            Instances For
              noncomputable def ModuleCat.imageIsoRange {R : Type u} [Ring R] {G : ModuleCat R} {H : ModuleCat R} (f : G H) :

              The categorical image of a morphism in ModuleCat R agrees with the linear algebraic range.

              Instances For