mathlib3 documentation

category_theory.limits.preserves.shapes.kernels

Preserving (co)kernels #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

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 kernel_fork.of_ι with functor.map_cone.

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

Equations

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 cokernel_cofork.of_π with functor.map_cocone.

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

Equations