Commit 2026-03-17 19:40 d99fdfbf

View on Github →

feat(CategoryTheory/ObjectProperty/Kernels): Object properties of (co)kernels (#36481) Introduce two object properties kernels and cokernels as well as predicates IsClosedUnderKernels and IsClosedUnderCokernels.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/ObjectProperty/Kernels.lean

added inductive CategoryTheory.MorphismProperty.cokernels

added inductive CategoryTheory.MorphismProperty.kernels

added theorem CategoryTheory.ObjectProperty.hasColimit_parallelPair_comp_ι

added theorem CategoryTheory.ObjectProperty.hasLimit_parallelPair_comp_ι

added theorem CategoryTheory.ObjectProperty.prop_cokernel

added theorem CategoryTheory.ObjectProperty.prop_kernel

added theorem CategoryTheory.ObjectProperty.prop_of_isColimit_cokernelCofork

added theorem CategoryTheory.ObjectProperty.prop_of_isLimit_kernelFork