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 : ModuleCat R} {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 : ModuleCat R} {N : ModuleCat R} (f : M ⟶ N) :
    CategoryTheory.Limits.IsLimit (ModuleCat.kernelCone f)

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def ModuleCat.cokernelCocone {R : Type u} [Ring R] {M : ModuleCat R} {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 : ModuleCat R} {N : ModuleCat R} (f : M ⟶ N) :
        CategoryTheory.Limits.IsColimit (ModuleCat.cokernelCocone f)

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

        Equations
        • One or more equations did not get rendered due to their size.
        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 : ModuleCat R} {H : ModuleCat R} (f : G ⟶ H) :
          CategoryTheory.Limits.kernel f ≅ ModuleCat.of R ↥(LinearMap.ker f)

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

          Equations
          Instances For
            source
            theorem ModuleCat.kernelIsoKer_inv_kernel_ι_apply {R : Type u} [Ring R] {G : ModuleCat R} {H : ModuleCat R} (f : G ⟶ H) (x : (CategoryTheory.forget (ModuleCat R)).obj (ModuleCat.kernelCone f).pt) :
            (CategoryTheory.Limits.kernel.ι f) ((CategoryTheory.Limits.limit.isoLimitCone { cone := ModuleCat.kernelCone f, isLimit := ModuleCat.kernelIsLimit f }).inv x) = (CategoryTheory.Limits.Fork.ι (ModuleCat.kernelCone f)) x
            source
            @[simp]
            theorem ModuleCat.kernelIsoKer_inv_kernel_ι {R : Type u} [Ring R] {G : ModuleCat R} {H : ModuleCat R} (f : G ⟶ H) :
            CategoryTheory.CategoryStruct.comp (ModuleCat.kernelIsoKer f).inv (CategoryTheory.Limits.kernel.ι f) = Submodule.subtype (LinearMap.ker f)
            source
            theorem ModuleCat.kernelIsoKer_hom_ker_subtype_apply {R : Type u} [Ring R] {G : ModuleCat R} {H : ModuleCat R} (f : G ⟶ H) (x : (CategoryTheory.forget (ModuleCat R)).obj (CategoryTheory.Limits.limit.cone (CategoryTheory.Limits.parallelPair f 0)).pt) :
            (CategoryTheory.Limits.Fork.ι (ModuleCat.kernelCone f)) ((CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso (ModuleCat.kernelIsLimit f) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Limits.parallelPair f 0))).inv x) = (CategoryTheory.Limits.kernel.ι f) x
            source
            @[simp]
            theorem ModuleCat.kernelIsoKer_hom_ker_subtype {R : Type u} [Ring R] {G : ModuleCat R} {H : ModuleCat R} (f : G ⟶ H) :
            CategoryTheory.CategoryStruct.comp (ModuleCat.kernelIsoKer f).hom (Submodule.subtype (LinearMap.ker f)) = CategoryTheory.Limits.kernel.ι f
            source
            noncomputable def ModuleCat.cokernelIsoRangeQuotient {R : Type u} [Ring R] {G : ModuleCat R} {H : ModuleCat R} (f : G ⟶ H) :
            CategoryTheory.Limits.cokernel f ≅ ModuleCat.of R (↑H ⧸ LinearMap.range f)

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

            Equations
            Instances For
              source
              theorem ModuleCat.cokernel_π_cokernelIsoRangeQuotient_hom_apply {R : Type u} [Ring R] {G : ModuleCat R} {H : ModuleCat R} (f : G ⟶ H) (x : (CategoryTheory.forget (ModuleCat R)).obj ((CategoryTheory.Limits.parallelPair f 0).obj CategoryTheory.Limits.WalkingParallelPair.one)) :
              (CategoryTheory.Limits.colimit.isoColimitCocone { cocone := ModuleCat.cokernelCocone f, isColimit := ModuleCat.cokernelIsColimit f }).hom ((CategoryTheory.Limits.cokernel.π f) x) = (CategoryTheory.Limits.Cofork.π (ModuleCat.cokernelCocone f)) x
              source
              @[simp]
              theorem ModuleCat.cokernel_π_cokernelIsoRangeQuotient_hom {R : Type u} [Ring R] {G : ModuleCat R} {H : ModuleCat R} (f : G ⟶ H) :
              CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π f) (ModuleCat.cokernelIsoRangeQuotient f).hom = Submodule.mkQ (LinearMap.range f)
              source
              theorem ModuleCat.range_mkQ_cokernelIsoRangeQuotient_inv_apply {R : Type u} [Ring R] {G : ModuleCat R} {H : ModuleCat R} (f : G ⟶ H) (x : (CategoryTheory.forget (ModuleCat R)).obj ((CategoryTheory.Limits.parallelPair f 0).obj CategoryTheory.Limits.WalkingParallelPair.one)) :
              (CategoryTheory.Limits.colimit.isoColimitCocone { cocone := ModuleCat.cokernelCocone f, isColimit := ModuleCat.cokernelIsColimit f }).inv ((CategoryTheory.Limits.Cofork.π (ModuleCat.cokernelCocone f)) x) = (CategoryTheory.Limits.cokernel.π f) x
              source
              @[simp]
              theorem ModuleCat.range_mkQ_cokernelIsoRangeQuotient_inv {R : Type u} [Ring R] {G : ModuleCat R} {H : ModuleCat R} (f : G ⟶ H) :
              CategoryTheory.CategoryStruct.comp (ModuleCat.asHomLeft (Submodule.mkQ (LinearMap.range f))) (ModuleCat.cokernelIsoRangeQuotient f).inv = CategoryTheory.Limits.cokernel.π f
              source
              theorem ModuleCat.cokernel_π_ext {R : Type u} [Ring R] {M : ModuleCat R} {N : ModuleCat R} (f : M ⟶ N) {x : ↑N} {y : ↑N} (m : ↑M) (w : x = y + f m) :
              (CategoryTheory.Limits.cokernel.π f) x = (CategoryTheory.Limits.cokernel.π f) y