Documentation

Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

Preserving (co)kernels #

Constructions to relate the notions of preserving (co)kernels and reflecting (co)kernels to concrete (co)forks.

In particular, we show that kernel_comparison f g G is an isomorphism iff G preserves the limit of the parallel pair f,0, as well as the dual result.

A kernel fork for f is mapped to a kernel fork for G.map f if G is a functor which preserves zero morphisms.

Instances For

    The map of a kernel fork is a limit iff the kernel fork consisting of the mapped morphisms is a limit. This essentially lets us commute KernelFork.ofι with Functor.mapCone.

    This is a variant of isLimitMapConeForkEquiv for equalizers, which we can't use directly between G.map 0 = 0 does not hold definitionally.

    Instances For

      The property of preserving kernels expressed in terms of kernel forks.

      This is a variant of isLimitForkMapOfIsLimit for equalizers, which we can't use directly between G.map 0 = 0 does not hold definitionally.

      Instances For

        A cokernel cofork for f is mapped to a cokernel cofork for G.map f if G is a functor which preserves zero morphisms.

        Instances For

          The map of a cokernel cofork is a colimit iff the cokernel cofork consisting of the mapped morphisms is a colimit. This essentially lets us commute CokernelCofork.ofπ with Functor.mapCocone.

          This is a variant of isColimitMapCoconeCoforkEquiv for equalizers, which we can't use directly between G.map 0 = 0 does not hold definitionally.

          Instances For

            The property of preserving cokernels expressed in terms of cokernel coforks.

            This is a variant of isColimitCoforkMapOfIsColimit for equalizers, which we can't use directly between G.map 0 = 0 does not hold definitionally.

            Instances For