Commit 2020-06-01 17:01 17296e9c

View on Github →

feat(category_theory/abelian): Schur's lemma (#2838) I wrote this mostly to gain some familiarity with @TwoFX's work on abelian categories from #2817. That all looked great, and Schur's lemma was pleasantly straightforward.

Estimated changes

Modified src/category_theory/limits/shapes/images.lean

added theorem category_theory.limits.epi_of_epi_image

Modified src/category_theory/limits/shapes/kernels.lean

modified def category_theory.limits.cokernel.cokernel_iso

modified def category_theory.limits.cokernel.of_epi

modified def category_theory.limits.cokernel.of_iso_comp

modified theorem category_theory.limits.cokernel.π_of_epi

modified def category_theory.limits.cokernel.π_of_zero

added def category_theory.limits.cokernel.π_zero_is_iso

added theorem category_theory.limits.cokernel_not_iso_of_nonzero

added theorem category_theory.limits.cokernel_not_mono_of_nonzero

added theorem category_theory.limits.eq_zero_of_epi_kernel

added theorem category_theory.limits.eq_zero_of_mono_cokernel

added def category_theory.limits.has_cokernel

added def category_theory.limits.has_kernel

modified def category_theory.limits.kernel.iso_kernel

modified def category_theory.limits.kernel.of_comp_iso

modified def category_theory.limits.kernel.of_mono

modified theorem category_theory.limits.kernel.ι_of_mono

modified def category_theory.limits.kernel.ι_of_zero

modified def category_theory.limits.kernel.ι_zero_is_iso

added theorem category_theory.limits.kernel_not_epi_of_nonzero

added theorem category_theory.limits.kernel_not_iso_of_nonzero

Modified src/category_theory/limits/shapes/zero.lean

added theorem category_theory.limits.eq_zero_of_image_eq_zero

added theorem category_theory.limits.has_zero_object.from_zero_ext

added theorem category_theory.limits.has_zero_object.to_zero_ext

added theorem category_theory.limits.nonzero_image_of_nonzero

Modified src/category_theory/preadditive.lean

added theorem category_theory.preadditive.epi_of_cokernel_zero

modified def category_theory.preadditive.has_colimit_parallel_pair

modified def category_theory.preadditive.has_limit_parallel_pair

added theorem category_theory.preadditive.mono_of_kernel_zero

Created src/category_theory/schur.lean

added def category_theory.is_iso_of_hom_simple

Created src/category_theory/simple.lean

added theorem category_theory.cokernel_zero_of_nonzero_to_simple

added theorem category_theory.epi_from_simple_zero_of_not_iso

added def category_theory.is_iso_of_epi_of_nonzero

added def category_theory.is_iso_of_mono_of_nonzero

added theorem category_theory.kernel_zero_of_nonzero_from_simple

added theorem category_theory.mono_to_simple_zero_of_not_iso

added theorem category_theory.simple.ext

added def category_theory.simple_of_cosimple

added theorem category_theory.zero_not_simple