Commit 2023-04-24 22:52 62dc4a1d

View on Github →

feat: port CategoryTheory.Generator (#3623)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Generator.lean

added theorem CategoryTheory.CostructuredArrow.isSeparating_proj_preimage

added theorem CategoryTheory.IsCodetecting.isCoseparating

added theorem CategoryTheory.IsCodetecting.mono

added def CategoryTheory.IsCodetecting

added theorem CategoryTheory.IsCodetector.def

added theorem CategoryTheory.IsCodetector.isCoseparator

added def CategoryTheory.IsCodetector

added theorem CategoryTheory.IsCoseparating.isCodetecting

added theorem CategoryTheory.IsCoseparating.mono

added def CategoryTheory.IsCoseparating

added theorem CategoryTheory.IsCoseparator.def

added def CategoryTheory.IsCoseparator

added theorem CategoryTheory.IsCospearator.isCodetector

added theorem CategoryTheory.IsDetecting.isSeparating

added theorem CategoryTheory.IsDetecting.mono

added def CategoryTheory.IsDetecting

added theorem CategoryTheory.IsDetector.def

added theorem CategoryTheory.IsDetector.isSeparator

added def CategoryTheory.IsDetector

added theorem CategoryTheory.IsSeparating.isDetecting

added theorem CategoryTheory.IsSeparating.mono

added def CategoryTheory.IsSeparating

added theorem CategoryTheory.IsSeparator.def

added theorem CategoryTheory.IsSeparator.isDetector

added def CategoryTheory.IsSeparator

added theorem CategoryTheory.StructuredArrow.isCoseparating_proj_preimage

added theorem CategoryTheory.Subobject.eq_of_isDetecting

added theorem CategoryTheory.Subobject.eq_of_le_of_isDetecting

added theorem CategoryTheory.Subobject.inf_eq_of_isDetecting

added theorem CategoryTheory.groupoid_of_isCodetecting_empty

added theorem CategoryTheory.groupoid_of_isDetecting_empty

added theorem CategoryTheory.hasInitial_of_isCoseparating

added theorem CategoryTheory.hasTerminal_of_isSeparating

added theorem CategoryTheory.isCodetecting_empty_of_groupoid

added theorem CategoryTheory.isCodetecting_iff_isCoseparating

added theorem CategoryTheory.isCodetecting_op_iff

added theorem CategoryTheory.isCodetecting_unop_iff

added theorem CategoryTheory.isCodetector_def

added theorem CategoryTheory.isCodetector_iff_reflectsIsomorphisms_yoneda_obj

added theorem CategoryTheory.isCodetector_op_iff

added theorem CategoryTheory.isCodetector_unop_iff

added theorem CategoryTheory.isCoseparating_empty_of_thin

added theorem CategoryTheory.isCoseparating_iff_mono

added theorem CategoryTheory.isCoseparating_op_iff

added theorem CategoryTheory.isCoseparating_unop_iff

added theorem CategoryTheory.isCoseparator_def

added theorem CategoryTheory.isCoseparator_iff_faithful_yoneda_obj

added theorem CategoryTheory.isCoseparator_iff_mono

added theorem CategoryTheory.isCoseparator_op_iff

added theorem CategoryTheory.isCoseparator_pi

added theorem CategoryTheory.isCoseparator_pi_of_isCoseparator

added theorem CategoryTheory.isCoseparator_prod

added theorem CategoryTheory.isCoseparator_prod_of_isCoseparator_left

added theorem CategoryTheory.isCoseparator_prod_of_isCoseparator_right

added theorem CategoryTheory.isCoseparator_unop_iff

added theorem CategoryTheory.isDetecting_empty_of_groupoid

added theorem CategoryTheory.isDetecting_iff_isSeparating

added theorem CategoryTheory.isDetecting_op_iff

added theorem CategoryTheory.isDetecting_unop_iff

added theorem CategoryTheory.isDetector_def

added theorem CategoryTheory.isDetector_iff_reflectsIsomorphisms_coyoneda_obj

added theorem CategoryTheory.isDetector_op_iff

added theorem CategoryTheory.isDetector_unop_iff

added theorem CategoryTheory.isSeparating_empty_of_thin

added theorem CategoryTheory.isSeparating_iff_epi

added theorem CategoryTheory.isSeparating_op_iff

added theorem CategoryTheory.isSeparating_unop_iff

added theorem CategoryTheory.isSeparator_coprod

added theorem CategoryTheory.isSeparator_coprod_of_isSeparator_left

added theorem CategoryTheory.isSeparator_coprod_of_isSeparator_right

added theorem CategoryTheory.isSeparator_def

added theorem CategoryTheory.isSeparator_iff_epi

added theorem CategoryTheory.isSeparator_iff_faithful_coyoneda_obj

added theorem CategoryTheory.isSeparator_op_iff

added theorem CategoryTheory.isSeparator_sigma

added theorem CategoryTheory.isSeparator_sigma_of_isSeparator

added theorem CategoryTheory.isSeparator_unop_iff

added theorem CategoryTheory.thin_of_isCoseparating_empty

added theorem CategoryTheory.thin_of_isSeparating_empty

added theorem CategoryTheory.wellPowered_of_isDetecting

added theorem CategoryTheory.wellPowered_of_isDetector