Commit 2025-10-25 10:31 4b9bae09

View on Github →

feat(CategoryTheory/Limits/Shapes): (co)kernel as a functor (#30674) and (co)kernel inclusion/projection as a natural transformation. Also fix a typo. From ClassFieldTheory

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Limits/Cones.lean

Created Mathlib/CategoryTheory/Limits/FunctorCategory/Shapes/Kernels.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean

added theorem CategoryTheory.Limits.coker.condition

added def CategoryTheory.Limits.coker.π

added theorem CategoryTheory.Limits.ker.condition

added def CategoryTheory.Limits.ker.ι