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.

source
theorem Subtype.ext_val_iff {α : Sort u_1} {p : α → Prop} {a1 a2 : { x : α // p x }} :
a1 = a2 ↔ ↑a1 = ↑a2
source
def ModuleCat.image {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) :
ModuleCat R

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

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

      The inclusion of image f into the target

      Equations
        Instances For
          source
          instance ModuleCat.instMonoι {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) :
          CategoryTheory.Mono (image.ι f)
          source
          def ModuleCat.factorThruImage {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) :
          G ⟶ image f

          The corestriction map to the image

          Equations
            Instances For
              source
              theorem ModuleCat.image.fac {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) :
              CategoryTheory.CategoryStruct.comp (factorThruImage f) (ι f) = f
              source
              noncomputable def ModuleCat.image.lift {R : Type u} [Ring R] {G H : ModuleCat R} {f : G ⟶ H} (F' : CategoryTheory.Limits.MonoFactorisation f) :
              image f ⟶ F'.I

              The universal property for the image factorisation

              Equations
                Instances For
                  source
                  theorem ModuleCat.image.lift_fac {R : Type u} [Ring R] {G H : ModuleCat R} {f : G ⟶ H} (F' : CategoryTheory.Limits.MonoFactorisation f) :
                  CategoryTheory.CategoryStruct.comp (lift F') F'.m = ι f
                  source
                  def ModuleCat.monoFactorisation {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) :
                  CategoryTheory.Limits.MonoFactorisation f

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

                  Equations
                    Instances For
                      source
                      noncomputable def ModuleCat.isImage {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) :
                      CategoryTheory.Limits.IsImage (monoFactorisation f)

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

                      Equations
                        Instances For
                          source
                          noncomputable def ModuleCat.imageIsoRange {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) :
                          CategoryTheory.Limits.image f ≅ of R ↥(LinearMap.range (Hom.hom f))

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

                          Equations
                            Instances For
                              source
                              @[simp]
                              theorem ModuleCat.imageIsoRange_inv_image_ι {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) :
                              CategoryTheory.CategoryStruct.comp (imageIsoRange f).inv (CategoryTheory.Limits.image.ι f) = ofHom (LinearMap.range (Hom.hom f)).subtype
                              source
                              theorem ModuleCat.imageIsoRange_inv_image_ι_assoc {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) {Z : ModuleCat R} (h : H ⟶ Z) :
                              CategoryTheory.CategoryStruct.comp (imageIsoRange f).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) h) = CategoryTheory.CategoryStruct.comp (ofHom (LinearMap.range (Hom.hom f)).subtype) h
                              source
                              theorem ModuleCat.imageIsoRange_inv_image_ι_apply {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) (x : CategoryTheory.ToType (of R ↥(LinearMap.range (Hom.hom f)))) :
                              (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.image.ι f)) ((CategoryTheory.ConcreteCategory.hom (imageIsoRange f).inv) x) = ↑x
                              source
                              @[simp]
                              theorem ModuleCat.imageIsoRange_hom_subtype {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) :
                              CategoryTheory.CategoryStruct.comp (imageIsoRange f).hom (ofHom (LinearMap.range (Hom.hom f)).subtype) = CategoryTheory.Limits.image.ι f
                              source
                              theorem ModuleCat.imageIsoRange_hom_subtype_assoc {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) {Z : ModuleCat R} (h : of R ↑H ⟶ Z) :
                              CategoryTheory.CategoryStruct.comp (imageIsoRange f).hom (CategoryTheory.CategoryStruct.comp (ofHom (LinearMap.range (Hom.hom f)).subtype) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) h
                              source
                              theorem ModuleCat.imageIsoRange_hom_subtype_apply {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) (x : CategoryTheory.ToType (CategoryTheory.Limits.image f)) :
                              ↑((CategoryTheory.ConcreteCategory.hom (imageIsoRange f).hom) x) = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.image.ι f)) x