Commit 2023-03-22 13:50 1bd50665

View on Github →

feat: port CategoryTheory.Limits.Shapes.KernelPair (#2871)

Estimated changes

Modified Mathlib.lean

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

added def CategoryTheory.Limits.Cofork.IsColimit.desc

added theorem CategoryTheory.Limits.Cofork.IsColimit.π_desc'

added def CategoryTheory.Limits.Fork.IsLimit.lift

added theorem CategoryTheory.Limits.Fork.IsLimit.lift_ι'

Created Mathlib/CategoryTheory/Limits/Shapes/KernelPair.lean

added theorem CategoryTheory.IsKernelPair.cancel_right

added theorem CategoryTheory.IsKernelPair.cancel_right_of_mono

added theorem CategoryTheory.IsKernelPair.comp_of_mono

added theorem CategoryTheory.IsKernelPair.id_of_mono

added theorem CategoryTheory.IsKernelPair.isIso_of_mono

added theorem CategoryTheory.IsKernelPair.lift_fst

added theorem CategoryTheory.IsKernelPair.lift_snd

added theorem CategoryTheory.IsKernelPair.mono_of_isIso_fst

added theorem CategoryTheory.IsKernelPair.of_isIso_of_mono

added def CategoryTheory.IsKernelPair.toCoequalizer

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

added def CategoryTheory.Limits.PullbackCone.IsLimit.lift

added theorem CategoryTheory.Limits.PullbackCone.IsLimit.lift_fst

added theorem CategoryTheory.Limits.PullbackCone.IsLimit.lift_snd

added def CategoryTheory.Limits.PushoutCocone.IsColimit.desc

added theorem CategoryTheory.Limits.PushoutCocone.IsColimit.inl_desc

added theorem CategoryTheory.Limits.PushoutCocone.IsColimit.inr_desc