Documentation

Mathlib.Algebra.Category.ModuleCat.Kernels

The concrete (co)kernels in the category of modules are (co)kernels in the categorical sense. #

source
def ModuleCat.kernelCone {R : Type u} [Ring R] {M N : ModuleCat R} (f : M ⟶ N) :
CategoryTheory.Limits.KernelFork f

The kernel cone induced by the concrete kernel.

Equations
    Instances For
      source
      def ModuleCat.kernelIsLimit {R : Type u} [Ring R] {M N : ModuleCat R} (f : M ⟶ N) :
      CategoryTheory.Limits.IsLimit (kernelCone f)

      The kernel of a linear map is a kernel in the categorical sense.

      Equations
        Instances For
          source
          def ModuleCat.cokernelCocone {R : Type u} [Ring R] {M N : ModuleCat R} (f : M ⟶ N) :
          CategoryTheory.Limits.CokernelCofork f

          The cokernel cocone induced by the projection onto the quotient.

          Equations
            Instances For
              source
              def ModuleCat.cokernelIsColimit {R : Type u} [Ring R] {M N : ModuleCat R} (f : M ⟶ N) :
              CategoryTheory.Limits.IsColimit (cokernelCocone f)

              The projection onto the quotient is a cokernel in the categorical sense.

              Equations
                Instances For
                  source
                  theorem ModuleCat.hasKernels_moduleCat {R : Type u} [Ring R] :
                  CategoryTheory.Limits.HasKernels (ModuleCat R)

                  The category of R-modules has kernels, given by the inclusion of the kernel submodule.

                  source
                  theorem ModuleCat.hasCokernels_moduleCat {R : Type u} [Ring R] :
                  CategoryTheory.Limits.HasCokernels (ModuleCat R)

                  The category of R-modules has cokernels, given by the projection onto the quotient.

                  source
                  noncomputable def ModuleCat.kernelIsoKer {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) :
                  CategoryTheory.Limits.kernel f ≅ of R ↥(LinearMap.ker (Hom.hom f))

                  The categorical kernel of a morphism in ModuleCat agrees with the usual module-theoretical kernel.

                  Equations
                    Instances For
                      source
                      @[simp]
                      theorem ModuleCat.kernelIsoKer_inv_kernel_ι {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) :
                      CategoryTheory.CategoryStruct.comp (kernelIsoKer f).inv (CategoryTheory.Limits.kernel.ι f) = ofHom (LinearMap.ker (Hom.hom f)).subtype
                      source
                      theorem ModuleCat.kernelIsoKer_inv_kernel_ι_apply {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) (x : CategoryTheory.ToType (of R ↥(LinearMap.ker (Hom.hom f)))) :
                      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.kernel.ι f)) ((CategoryTheory.ConcreteCategory.hom (kernelIsoKer f).inv) x) = ↑x
                      source
                      @[simp]
                      theorem ModuleCat.kernelIsoKer_hom_ker_subtype {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) :
                      CategoryTheory.CategoryStruct.comp (kernelIsoKer f).hom (ofHom (LinearMap.ker (Hom.hom f)).subtype) = CategoryTheory.Limits.kernel.ι f
                      source
                      theorem ModuleCat.kernelIsoKer_hom_ker_subtype_apply {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) (x : CategoryTheory.ToType (CategoryTheory.Limits.kernel f)) :
                      ↑((CategoryTheory.ConcreteCategory.hom (kernelIsoKer f).hom) x) = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.kernel.ι f)) x
                      source
                      noncomputable def ModuleCat.cokernelIsoRangeQuotient {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) :
                      CategoryTheory.Limits.cokernel f ≅ of R (↑H ⧸ LinearMap.range (Hom.hom f))

                      The categorical cokernel of a morphism in ModuleCat agrees with the usual module-theoretical quotient.

                      Equations
                        Instances For
                          source
                          @[simp]
                          theorem ModuleCat.cokernel_π_cokernelIsoRangeQuotient_hom {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) :
                          CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π f) (cokernelIsoRangeQuotient f).hom = ofHom (LinearMap.range (Hom.hom f)).mkQ
                          source
                          theorem ModuleCat.cokernel_π_cokernelIsoRangeQuotient_hom_apply {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) (x : CategoryTheory.ToType H) :
                          (CategoryTheory.ConcreteCategory.hom (cokernelIsoRangeQuotient f).hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.cokernel.π f)) x) = Submodule.Quotient.mk x
                          source
                          @[simp]
                          theorem ModuleCat.range_mkQ_cokernelIsoRangeQuotient_inv {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) :
                          CategoryTheory.CategoryStruct.comp (ofHom (LinearMap.range (Hom.hom f)).mkQ) (cokernelIsoRangeQuotient f).inv = CategoryTheory.Limits.cokernel.π f
                          source
                          theorem ModuleCat.range_mkQ_cokernelIsoRangeQuotient_inv_apply {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) (x : CategoryTheory.ToType (of R ↑H)) :
                          (CategoryTheory.ConcreteCategory.hom (cokernelIsoRangeQuotient f).inv) (Submodule.Quotient.mk x) = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.cokernel.π f)) x
                          source
                          theorem ModuleCat.cokernel_π_ext {R : Type u} [Ring R] {M N : ModuleCat R} (f : M ⟶ N) {x y : ↑N} (m : ↑M) (w : x = y + (CategoryTheory.ConcreteCategory.hom f) m) :
                          (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.cokernel.π f)) x = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.cokernel.π f)) y