Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-04 07:50 d537897a

View on Github →

feat(category_theory/simple): simple objects are indecomposable (#13882) Remarkably tedious.

Estimated changes

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

added def category_theory.indecomposable

added theorem category_theory.limits.biprod.is_iso_inl_iff_id_eq_fst_comp_inl

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

added theorem category_theory.limits.is_zero.eq_zero_of_src

added theorem category_theory.limits.is_zero.eq_zero_of_tgt

added theorem category_theory.limits.is_zero.iff_id_eq_zero

added theorem category_theory.limits.is_zero.iff_split_epi_eq_zero

added theorem category_theory.limits.is_zero.iff_split_mono_eq_zero

added theorem category_theory.limits.is_zero.of_epi

added theorem category_theory.limits.is_zero.of_epi_eq_zero

added theorem category_theory.limits.is_zero.of_epi_zero

added theorem category_theory.limits.is_zero.of_mono

added theorem category_theory.limits.is_zero.of_mono_eq_zero

added theorem category_theory.limits.is_zero.of_mono_zero

Modified src/category_theory/simple.lean

added theorem category_theory.biprod.is_iso_inl_iff_is_zero

added theorem category_theory.indecomposable_of_simple

added theorem category_theory.simple.not_is_zero

added theorem category_theory.simple.of_iso