Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-21 15:30 6db15773

View on Github →

feat(category_theory/preadditive): separators in preadditive categories (#11884)

Estimated changes

Modified src/category_theory/generator.lean

modified theorem category_theory.is_codetecting_op_iff

modified theorem category_theory.is_codetector_def

modified theorem category_theory.is_codetector_iff_reflects_isomorphisms_yoneda_obj

modified theorem category_theory.is_coseparator_def

modified theorem category_theory.is_coseparator_iff_faithful_yoneda_obj

modified theorem category_theory.is_detecting_iff_is_separating

modified theorem category_theory.is_detecting_op_iff

modified theorem category_theory.is_detecting_unop_iff

modified theorem category_theory.is_detector_def

modified theorem category_theory.is_detector_iff_reflects_isomorphisms_coyoneda_obj

modified theorem category_theory.is_separating_op_iff

modified theorem category_theory.is_separator_def

modified theorem category_theory.is_separator_iff_faithful_coyoneda_obj

Created src/category_theory/preadditive/generator.lean

added theorem category_theory.is_coseparator_iff_faithful_preadditive_yoneda

added theorem category_theory.is_coseparator_iff_faithful_preadditive_yoneda_obj

added theorem category_theory.is_separator_iff_faithful_preadditive_coyoneda

added theorem category_theory.is_separator_iff_faithful_preadditive_coyoneda_obj

added theorem category_theory.preadditive.is_coseparating_iff

added theorem category_theory.preadditive.is_coseparator_iff

added theorem category_theory.preadditive.is_separating_iff

added theorem category_theory.preadditive.is_separator_iff