Commit 2023-11-10 13:09 f3baa4cf

View on Github →

feat(CategoryTheory): more API for limit kernel forks (#8200) In this PR, we introduce KernelFork.mapIsoOfIsLimit which is the isomorphism between the "points" of two limit kernel forks of maps which are isomorphic in the category of arrows. This generalizes kernel.mapIso which is the case where the limit kernel forks are given by limit.isLimit.

Estimated changes

Modified Mathlib/CategoryTheory/Arrow.lean

added theorem CategoryTheory.Arrow.hom_inv_id_left

added theorem CategoryTheory.Arrow.hom_inv_id_right

added theorem CategoryTheory.Arrow.inv_hom_id_left

added theorem CategoryTheory.Arrow.inv_hom_id_right

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

added def CategoryTheory.Limits.CokernelCofork.mapIsoOfIsColimit

added def CategoryTheory.Limits.CokernelCofork.mapOfIsColimit

added theorem CategoryTheory.Limits.CokernelCofork.π_mapOfIsColimit

added def CategoryTheory.Limits.KernelFork.mapIsoOfIsLimit

added def CategoryTheory.Limits.KernelFork.mapOfIsLimit

added theorem CategoryTheory.Limits.KernelFork.mapOfIsLimit_ι