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.

theorem Subtype.ext_val_iff {α : Sort u_1} {p : αProp} {a1 : { x : α // p x }} {a2 : { x : α // p x }} :
a1 = a2 a1 = a2
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

Equations
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

    Equations
    Instances For
      instance ModuleCat.instMonoι {R : Type u} [Ring R] {G : ModuleCat R} {H : ModuleCat R} (f : G H) :
      Equations
      • =
      def ModuleCat.factorThruImage {R : Type u} [Ring R] {G : ModuleCat R} {H : ModuleCat R} (f : G H) :

      The corestriction map to the image

      Equations
      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

        Equations
        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.

          Equations
          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.

            Equations
            Instances For