Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-05 21:22 6787a8d9

View on Github →

feat(category_theory): a hierarchy of balanced categories (#11856)

Estimated changes

Modified src/algebra/category/Group/abelian.lean

Modified src/algebra/category/Module/abelian.lean

Modified src/category_theory/abelian/basic.lean

deleted theorem category_theory.abelian.is_iso_of_mono_of_epi

deleted theorem category_theory.abelian.strong_epi_of_epi

deleted theorem category_theory.abelian.strong_mono_of_mono

Modified src/category_theory/abelian/non_preadditive.lean

deleted theorem category_theory.non_preadditive_abelian.is_iso_of_mono_of_epi

deleted theorem category_theory.non_preadditive_abelian.strong_epi_of_epi

Modified src/category_theory/abelian/opposite.lean

Created src/category_theory/balanced.lean

added theorem category_theory.is_iso_iff_mono_and_epi

added theorem category_theory.is_iso_of_mono_of_epi

Modified src/category_theory/epi_mono.lean

added def category_theory.split_epi_of_epi

added def category_theory.split_mono_of_mono

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

added def category_theory.normal_epi_of_epi

added def category_theory.normal_mono_of_mono

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

added def category_theory.regular_epi_of_epi

added def category_theory.regular_mono_of_mono

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

added theorem category_theory.strong_epi_of_epi

added theorem category_theory.strong_mono_of_mono

Modified src/category_theory/simple.lean

Modified src/category_theory/types.lean

added theorem category_theory.injective_of_mono

added theorem category_theory.surjective_of_epi