Commit 2024-11-10 09:06 f00a79ed

View on Github →

feat(CategoryTheory/Generator): introduce classes HasDetector and HasSeparator (#18577) This change defines the typeclasses HasDetector and HasSeparator for categories with detectors/separators. Several results for IsDetector and IsSeparator are also proved for the new typeclasses. Convenience theorems for proving the well-poweredness of categories with separators are added, too. Two typos are fixed: "separating" is corrected to "coseparating" in the module docstring and IsCospearator.isCodetector is renamed to IsCoseparator.isCodetector.

Estimated changes

Modified Mathlib/CategoryTheory/Generator.lean

added theorem CategoryTheory.HasCodetector.hasCoseparator

added theorem CategoryTheory.HasCodetector.hasDetector_of_hasCodetector_op

added theorem CategoryTheory.HasCoseparator.hasCodetector

added theorem CategoryTheory.HasCoseparator.hasSeparator_of_hasCoseparator_op

added theorem CategoryTheory.HasDetector.hasCodetector_of_hasDetector_op

added theorem CategoryTheory.HasDetector.hasSeparator

added theorem CategoryTheory.HasSeparator.hasCoseparator_of_hasSeparator_op

added theorem CategoryTheory.HasSeparator.hasDetector

added theorem CategoryTheory.IsCoseparator.isCodetector

deleted theorem CategoryTheory.IsCospearator.isCodetector

added theorem CategoryTheory.hasCodetector_op_iff

added theorem CategoryTheory.hasCoseparator_op_iff

added theorem CategoryTheory.hasDetector_op_iff

added theorem CategoryTheory.hasSeparator_op_iff

added theorem CategoryTheory.isCodetector_codetector

added theorem CategoryTheory.isCodetector_coseparator

added theorem CategoryTheory.isCoseparator_codetector

added theorem CategoryTheory.isCoseparator_coseparator

added theorem CategoryTheory.isDetector_detector

added theorem CategoryTheory.isDetector_separator

added theorem CategoryTheory.isSeparator_detector

added theorem CategoryTheory.isSeparator_separator

added theorem CategoryTheory.wellPowered_of_isSeparator