Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-15 19:34 d76ac2e0

View on Github →

feat(category_theory): separators and detectors (#11880)

Estimated changes

Modified src/category_theory/balanced.lean

added theorem category_theory.balanced_opposite

Created src/category_theory/generator.lean

added theorem category_theory.groupoid_of_is_codetecting_empty

added theorem category_theory.groupoid_of_is_detecting_empty

added theorem category_theory.is_codetecting.is_coseparating

added theorem category_theory.is_codetecting.mono

added def category_theory.is_codetecting

added theorem category_theory.is_codetecting_empty_of_groupoid

added theorem category_theory.is_codetecting_iff_is_coseparating

added theorem category_theory.is_codetecting_op_iff

added theorem category_theory.is_codetecting_unop_iff

added theorem category_theory.is_codetector.def

added theorem category_theory.is_codetector.is_coseparator

added def category_theory.is_codetector

added theorem category_theory.is_codetector_def

added theorem category_theory.is_codetector_iff_reflects_isomorphisms_yoneda_obj

added theorem category_theory.is_codetector_op_iff

added theorem category_theory.is_codetector_unop_iff

added theorem category_theory.is_coseparating.is_codetecting

added theorem category_theory.is_coseparating.mono

added def category_theory.is_coseparating

added theorem category_theory.is_coseparating_empty_of_thin

added theorem category_theory.is_coseparating_op_iff

added theorem category_theory.is_coseparating_unop_iff

added theorem category_theory.is_coseparator.def

added def category_theory.is_coseparator

added theorem category_theory.is_coseparator_def

added theorem category_theory.is_coseparator_iff_faithful_yoneda_obj

added theorem category_theory.is_coseparator_op_iff

added theorem category_theory.is_coseparator_unop_iff

added theorem category_theory.is_cospearator.is_codetector

added theorem category_theory.is_detecting.is_separating

added theorem category_theory.is_detecting.mono

added def category_theory.is_detecting

added theorem category_theory.is_detecting_empty_of_groupoid

added theorem category_theory.is_detecting_iff_is_separating

added theorem category_theory.is_detecting_op_iff

added theorem category_theory.is_detecting_unop_iff

added theorem category_theory.is_detector.def

added theorem category_theory.is_detector.is_separator

added def category_theory.is_detector

added theorem category_theory.is_detector_def

added theorem category_theory.is_detector_iff_reflects_isomorphisms_coyoneda_obj

added theorem category_theory.is_detector_op_iff

added theorem category_theory.is_detector_unop_iff

added theorem category_theory.is_separating.is_detecting

added theorem category_theory.is_separating.mono

added def category_theory.is_separating

added theorem category_theory.is_separating_empty_of_thin

added theorem category_theory.is_separating_op_iff

added theorem category_theory.is_separating_unop_iff

added theorem category_theory.is_separator.def

added theorem category_theory.is_separator.is_detector

added def category_theory.is_separator

added theorem category_theory.is_separator_def

added theorem category_theory.is_separator_iff_faithful_coyoneda_obj

added theorem category_theory.is_separator_op_iff

added theorem category_theory.is_separator_unop_iff

added theorem category_theory.thin_of_is_coseparating_empty

added theorem category_theory.thin_of_is_separating_empty

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

Modified src/category_theory/opposites.lean

added theorem category_theory.is_iso_op_iff

added theorem category_theory.is_iso_unop_iff

modified theorem category_theory.op_inv

added theorem category_theory.unop_inv