Commit 2023-03-08 17:04 b14d04a2

View on Github →

feat: port CategoryTheory.Limits.Shapes.Kernels (#2636)

Estimated changes

Modified Mathlib.lean

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

added def CategoryTheory.Limits.CokernelCofork.IsColimit.desc'

added def CategoryTheory.Limits.CokernelCofork.IsColimit.ofπ

added theorem CategoryTheory.Limits.CokernelCofork.condition

added theorem CategoryTheory.Limits.CokernelCofork.π_eq_zero

added theorem CategoryTheory.Limits.CokernelCofork.π_ofπ

added def CategoryTheory.Limits.IsCokernel.cokernelIso

added def CategoryTheory.Limits.IsCokernel.ofIsoComp

added def CategoryTheory.Limits.IsKernel.isoKernel

added def CategoryTheory.Limits.IsKernel.ofCompIso

added def CategoryTheory.Limits.KernelFork.IsLimit.lift'

added def CategoryTheory.Limits.KernelFork.IsLimit.ofι

added theorem CategoryTheory.Limits.KernelFork.app_one

added theorem CategoryTheory.Limits.KernelFork.condition

added theorem CategoryTheory.Limits.KernelFork.ι_ofι

added theorem CategoryTheory.Limits.MonoFactorisation.kernel_ι_comp

added theorem CategoryTheory.Limits.coequalizer_as_cokernel

added def CategoryTheory.Limits.cokernel.cokernelIso

added theorem CategoryTheory.Limits.cokernel.condition

added def CategoryTheory.Limits.cokernel.desc'

added theorem CategoryTheory.Limits.cokernel.desc_zero

added def CategoryTheory.Limits.cokernel.isColimitCoconeZeroCocone

added def CategoryTheory.Limits.cokernel.mapIso

added theorem CategoryTheory.Limits.cokernel.map_desc

added def CategoryTheory.Limits.cokernel.ofEpi

added def CategoryTheory.Limits.cokernel.ofIsoComp

added def CategoryTheory.Limits.cokernel.zeroCokernelCofork

added theorem CategoryTheory.Limits.cokernel.π_desc

added theorem CategoryTheory.Limits.cokernel.π_of_epi

added theorem CategoryTheory.Limits.cokernel.π_of_zero

added def CategoryTheory.Limits.cokernelCompIsIso

added def CategoryTheory.Limits.cokernelComparison

added theorem CategoryTheory.Limits.cokernelComparison_map_desc

added def CategoryTheory.Limits.cokernelEpiComp

added def CategoryTheory.Limits.cokernelImageι

added def CategoryTheory.Limits.cokernelIsCokernel

added def CategoryTheory.Limits.cokernelIsoOfEq

added theorem CategoryTheory.Limits.cokernelIsoOfEq_hom_comp_desc

added theorem CategoryTheory.Limits.cokernelIsoOfEq_inv_comp_desc

added theorem CategoryTheory.Limits.cokernelIsoOfEq_refl

added theorem CategoryTheory.Limits.cokernelIsoOfEq_trans

added def CategoryTheory.Limits.cokernelZeroIsoTarget

added theorem CategoryTheory.Limits.cokernelZeroIsoTarget_hom

added theorem CategoryTheory.Limits.cokernelZeroIsoTarget_inv

added theorem CategoryTheory.Limits.cokernel_map_comp_cokernelComparison

added theorem CategoryTheory.Limits.cokernel_not_iso_of_nonzero

added theorem CategoryTheory.Limits.cokernel_not_mono_of_nonzero

added def CategoryTheory.Limits.compNatIso

added theorem CategoryTheory.Limits.eq_zero_of_epi_kernel

added theorem CategoryTheory.Limits.eq_zero_of_mono_cokernel

added theorem CategoryTheory.Limits.equalizer_as_kernel

added def CategoryTheory.Limits.isCokernelEpiComp

added theorem CategoryTheory.Limits.isCokernelEpiComp_desc

added def CategoryTheory.Limits.isCokernelOfComp

added def CategoryTheory.Limits.isColimitAux

added def CategoryTheory.Limits.isKernelCompMono

added theorem CategoryTheory.Limits.isKernelCompMono_lift

added def CategoryTheory.Limits.isKernelOfComp

added def CategoryTheory.Limits.isLimitAux

added def CategoryTheory.Limits.isoOfι

added def CategoryTheory.Limits.isoOfπ

added theorem CategoryTheory.Limits.kernel.condition

added def CategoryTheory.Limits.kernel.isLimitConeZeroCone

added def CategoryTheory.Limits.kernel.isoKernel

added def CategoryTheory.Limits.kernel.lift'

added theorem CategoryTheory.Limits.kernel.lift_map

added theorem CategoryTheory.Limits.kernel.lift_zero

added theorem CategoryTheory.Limits.kernel.lift_ι

added def CategoryTheory.Limits.kernel.mapIso

added def CategoryTheory.Limits.kernel.ofCompIso

added def CategoryTheory.Limits.kernel.ofMono

added def CategoryTheory.Limits.kernel.zeroKernelFork

added theorem CategoryTheory.Limits.kernel.ι_of_mono

added theorem CategoryTheory.Limits.kernel.ι_of_zero

added def CategoryTheory.Limits.kernelCompMono

added def CategoryTheory.Limits.kernelComparison

added theorem CategoryTheory.Limits.kernelComparison_comp_kernel_map

added theorem CategoryTheory.Limits.kernelComparison_comp_ι

added def CategoryTheory.Limits.kernelIsIsoComp

added def CategoryTheory.Limits.kernelIsKernel

added def CategoryTheory.Limits.kernelIsoOfEq

added theorem CategoryTheory.Limits.kernelIsoOfEq_hom_comp_ι

added theorem CategoryTheory.Limits.kernelIsoOfEq_inv_comp_ι

added theorem CategoryTheory.Limits.kernelIsoOfEq_refl

added theorem CategoryTheory.Limits.kernelIsoOfEq_trans

added def CategoryTheory.Limits.kernelZeroIsoSource

added theorem CategoryTheory.Limits.kernelZeroIsoSource_hom

added theorem CategoryTheory.Limits.kernelZeroIsoSource_inv

added theorem CategoryTheory.Limits.kernel_not_epi_of_nonzero

added theorem CategoryTheory.Limits.kernel_not_iso_of_nonzero

added theorem CategoryTheory.Limits.lift_comp_kernelIsoOfEq_hom

added theorem CategoryTheory.Limits.lift_comp_kernelIsoOfEq_inv

added theorem CategoryTheory.Limits.map_lift_kernelComparison

added def CategoryTheory.Limits.ofιCongr

added def CategoryTheory.Limits.ofπCongr

added def CategoryTheory.Limits.zeroCokernelOfZeroCancel

added def CategoryTheory.Limits.zeroKernelOfCancelZero

added theorem CategoryTheory.Limits.π_comp_cokernelComparison

added theorem CategoryTheory.Limits.π_comp_cokernelIsoOfEq_hom

added theorem CategoryTheory.Limits.π_comp_cokernelIsoOfEq_inv