Commit 2023-03-09 06:58 6fc2d2db

View on Github →

feat: port CategoryTheory.Limits.Shapes.NormalMono.Equalizers (#2737)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/Shapes/NormalMono/Equalizers.lean

added def CategoryTheory.NormalEpiCategory.hasColimit_parallelPair

added theorem CategoryTheory.NormalEpiCategory.mono_of_cancel_zero

added theorem CategoryTheory.NormalEpiCategory.mono_of_zero_kernel

added def CategoryTheory.NormalEpiCategory.pushout_of_epi

added theorem CategoryTheory.NormalMonoCategory.epi_of_zero_cancel

added theorem CategoryTheory.NormalMonoCategory.epi_of_zero_cokernel

added def CategoryTheory.NormalMonoCategory.hasLimit_parallelPair

added def CategoryTheory.NormalMonoCategory.pullback_of_mono