Basic

📁 Source: Mathlib/CategoryTheory/Generator/Basic.lean

Statistics

Metric	Count
Definitions HasCodetector, HasCoseparator, HasDetector, HasSeparator, IsCodetecting, IsCodetector, IsCoseparating, IsCoseparator, IsDetecting, IsDetector, IsSeparating, IsSeparator, IsCodetecting, IsCoseparating, IsDetecting, IsSeparating, coproductFrom, coproductFromFamily, productTo, productToFamily, ιCoproductFrom, πProductTo, codetector, coseparator, detector, separator	26
Theorems isSeparating_inverseImage_proj, isSeparating_proj_preimage, hasCodetector, hasCoseparator, hasDetector_of_hasCodetector_op, hasDetector_op, hasCodetector, hasCoseparator, hasSeparator_of_hasCoseparator_op, hasSeparator_op, of_equivalence, hasCodetector_of_hasDetector_op, hasCodetector_op, hasDetector, hasSeparator, wellPowered, hasCoseparator_of_hasSeparator_op, hasCoseparator_op, hasDetector, hasSeparator, of_equivalence, wellPowered, isCoseparating, isIso_iff_of_epi, mono, def, isCoseparator, isCodetecting, mono, of_equivalence, def, isCodetector, of_equivalence, isIso_iff_of_mono, isSeparating, mono, def, isSeparator, isDetecting, isSeparator_coproduct, mono, of_equivalence, def, isDetector, of_equivalence, isCoseparating, isIso_iff_of_epi, of_le, epi_iff, isCodetecting, mk_of_exists_limitsOfShape, mk_of_exists_mono, mono_productTo, of_equivalence, of_le, isIso_iff_of_mono, isSeparating, of_le, epi_coproductFrom, isDetecting, isSeparator_coproduct, mk_of_exists_colimitsOfShape, mk_of_exists_epi, mono_iff, of_equivalence, of_le, isCodetecting_bot_of_isGroupoid, isCodetecting_iff_isCoseparating, isCodetecting_op_iff, isCodetecting_unop_iff, isCoseparating_bot_of_isThin, isCoseparating_iff_mono, isCoseparating_op_iff, isCoseparating_unop_iff, isDetecting_bot_of_isGroupoid, isDetecting_iff_isSeparating, isDetecting_op_iff, isDetecting_unop_iff, isGroupoid_of_isCodetecting_bot, isGroupoid_of_isDetecting_bot, isSeparating_bot_of_isThin, isSeparating_iff_epi, isSeparating_op_iff, isSeparating_unop_iff, isThin_of_isCoseparating_bot, isThin_of_isSeparating_bot, isCoseparating_inverseImage_proj, isCoseparating_proj_preimage, eq_of_isDetecting, eq_of_le_of_isDetecting, inf_eq_of_isDetecting, groupoid_of_isCodetecting_empty, groupoid_of_isDetecting_empty, hasCodetector_op_iff, hasCoseparator_op_iff, hasDetector_op_iff, hasInitial_of_isCoseparating, hasSeparator_op_iff, hasTerminal_of_isSeparating, isCodetecting_empty_of_groupoid, isCodetecting_iff_isCoseparating, isCodetecting_op_iff, isCodetecting_unop_iff, isCodetector_codetector, isCodetector_coseparator, isCodetector_def, isCodetector_iff_reflectsIsomorphisms_yoneda_obj, isCodetector_op_iff, isCodetector_unop_iff, isCoseparating_empty_of_thin, isCoseparating_iff_mono, isCoseparating_op_iff, isCoseparating_unop_iff, isCoseparator_codetector, isCoseparator_coseparator, isCoseparator_def, isCoseparator_iff_faithful_yoneda_obj, isCoseparator_iff_mono, isCoseparator_iff_of_isLimit_fan, isCoseparator_of_isLimit_fan, isCoseparator_op_iff, isCoseparator_pi, isCoseparator_pi_of_isCoseparator, isCoseparator_prod, isCoseparator_prod_of_isCoseparator_left, isCoseparator_prod_of_isCoseparator_right, isCoseparator_unop_iff, isDetecting_empty_of_groupoid, isDetecting_iff_isSeparating, isDetecting_op_iff, isDetecting_unop_iff, isDetector_def, isDetector_detector, isDetector_iff_reflectsIsomorphisms_coyoneda_obj, isDetector_op_iff, isDetector_separator, isDetector_unop_iff, isSeparating_empty_of_thin, isSeparating_iff_epi, isSeparating_op_iff, isSeparating_unop_iff, isSeparator_coprod, isSeparator_coprod_of_isSeparator_left, isSeparator_coprod_of_isSeparator_right, isSeparator_def, isSeparator_detector, isSeparator_iff_epi, isSeparator_iff_faithful_coyoneda_obj, isSeparator_iff_of_isColimit_cofan, isSeparator_of_isColimit_cofan, isSeparator_op_iff, isSeparator_separator, isSeparator_sigma, isSeparator_sigma_of_isSeparator, isSeparator_unop_iff, thin_of_isCoseparating_empty, thin_of_isSeparating_empty, wellPowered_of_isDetecting, wellPowered_of_isDetector, wellPowered_of_isSeparator	160
Total	186

CategoryTheory

Definitions

Name	Category	Theorems
HasCodetector 📖	CompData	5 math math: HasDetector.hasCodetector_of_hasDetector_op, HasCoseparator.hasCodetector, HasDetector.hasCodetector_op, hasDetector_op_iff, hasCodetector_op_iff
HasCoseparator 📖	CompData	7 math math: HasCoseparator.of_equivalence, IsGrothendieckAbelian.instHasCoseparator, HasSeparator.hasCoseparator_op, hasCoseparator_op_iff, HasCodetector.hasCoseparator, HasSeparator.hasCoseparator_of_hasSeparator_op, hasSeparator_op_iff
HasDetector 📖	CompData	5 math math: HasCodetector.hasDetector_of_hasCodetector_op, HasSeparator.hasDetector, hasDetector_op_iff, HasCodetector.hasDetector_op, hasCodetector_op_iff
HasSeparator 📖	CompData	11 math math: HasSeparator.of_equivalence, instHasSeparatorModuleCatOfSmall, HasDetector.hasSeparator, IsGrothendieckAbelian.hasSeparator, Sheaf.hasSeparator, Presheaf.hasSeparator, hasCoseparator_op_iff, HasCoseparator.hasSeparator_op, HomologicalComplex.instHasSeparator, HasCoseparator.hasSeparator_of_hasCoseparator_op, hasSeparator_op_iff
IsCodetecting 📖	MathDef	—
IsCodetector 📖	MathDef	10 math math: isCodetector_coseparator, isCodetector_unop_iff, IsCoseparator.isCodetector, isDetector_unop_iff, isCodetector_iff_reflectsIsomorphisms_yoneda_obj, HasCodetector.hasCodetector, isCodetector_op_iff, isCodetector_def, isDetector_op_iff, isCodetector_codetector
IsCoseparating 📖	MathDef	—
IsCoseparator 📖	MathDef	19 math math: isCoseparator_iff_mono, isCoseparator_iff_faithful_preadditiveYoneda, isCoseparator_of_isLimit_fan, isCoseparator_coseparator, isCoseparator_prod, isCoseparator_codetector, isCoseparator_def, isCoseparator_pi, isCoseparator_iff_faithful_yoneda_obj, isSeparator_op_iff, isCoseparator_iff_faithful_preadditiveYonedaObj, IsCodetector.isCoseparator, isCoseparator_iff_of_isLimit_fan, Preadditive.isCoseparator_iff, Abelian.has_injective_coseparator, isCoseparator_op_iff, HasCoseparator.hasCoseparator, isCoseparator_unop_iff, isSeparator_unop_iff
IsDetecting 📖	MathDef	—
IsDetector 📖	MathDef	10 math math: isCodetector_unop_iff, isDetector_detector, IsSeparator.isDetector, isDetector_iff_reflectsIsomorphisms_coyoneda_obj, isDetector_unop_iff, isCodetector_op_iff, isDetector_separator, HasDetector.hasDetector, isDetector_op_iff, isDetector_def
IsSeparating 📖	MathDef	—
IsSeparator 📖	MathDef	26 math math: isSeparator_iff_faithful_preadditiveCoyoneda, isSeparator_coprod, HasSeparator.hasSeparator, Preadditive.isSeparator_iff, IsSeparating.isSeparator_coproduct, isSeparator_sigma, isSeparator_iff_faithful_preadditiveCoyonedaObj, Ind.isSeparator_range_yoneda, isSeparator_iff_faithful_coyoneda_obj, Presheaf.isSeparator, isSeparator_iff_of_isColimit_cofan, isSeparator_iff_epi, isSeparator_def, Abelian.has_projective_separator, isSeparator_op_iff, isSeparator_detector, Types.isSeparator_punit, Sheaf.isSeparator, ObjectProperty.IsSeparating.isSeparator_coproduct, isCoseparator_op_iff, IsDetector.isSeparator, isSeparator_separator, isSeparator_of_isColimit_cofan, isCoseparator_unop_iff, isSeparator_unop_iff, ModuleCat.isSeparator
codetector 📖	CompOp	2 math math: isCoseparator_codetector, isCodetector_codetector
coseparator 📖	CompOp	2 math math: isCodetector_coseparator, isCoseparator_coseparator
detector 📖	CompOp	2 math math: isDetector_detector, isSeparator_detector
separator 📖	CompOp	2 math math: isDetector_separator, isSeparator_separator

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
groupoid_of_isCodetecting_empty 📖	mathematical	ObjectProperty.IsCodetecting Bot.bot ObjectProperty Category.toCategoryStruct Pi.instBotForall BooleanAlgebra.toBot Prop.instBooleanAlgebra	IsGroupoid	—	ObjectProperty.isGroupoid_of_isCodetecting_bot
groupoid_of_isDetecting_empty 📖	mathematical	ObjectProperty.IsDetecting Bot.bot ObjectProperty Category.toCategoryStruct Pi.instBotForall BooleanAlgebra.toBot Prop.instBooleanAlgebra	IsGroupoid	—	ObjectProperty.isGroupoid_of_isDetecting_bot
hasCodetector_op_iff 📖	mathematical	—	HasCodetector Opposite Category.opposite HasDetector	—	isDetector_unop_iff isCodetector_op_iff
hasCoseparator_op_iff 📖	mathematical	—	HasCoseparator Opposite Category.opposite HasSeparator	—	isSeparator_unop_iff isCoseparator_op_iff
hasDetector_op_iff 📖	mathematical	—	HasDetector Opposite Category.opposite HasCodetector	—	isCodetector_unop_iff isDetector_op_iff
hasInitial_of_isCoseparating 📖	mathematical	ObjectProperty.IsCoseparating	Limits.HasInitial	—	Limits.hasFiniteLimits_of_hasLimitsOfSize Limits.hasLimitOfHasLimitsOfShape Limits.hasProductsOfShape_of_small Limits.hasProductsOfShape_of_hasProducts Limits.hasLimitsOfShapeOfHasLimits ObjectProperty.IsCoseparating.mono_productTo StructuredArrow.instSmallOfLocallySmall ObjectProperty.instSmallFullSubcategoryOfSmall ObjectProperty.FullSubcategory.property Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype Limits.hasFiniteWidePullbacks_of_hasFiniteLimits Limits.pullback.fst_of_mono bot_le Limits.hasLimitsOfShape_of_hasFiniteLimits IsSplitEpi.mk' mono_comp Limits.equalizer.ι_mono Subobject.arrow_mono Subobject.eq_of_comp_arrow_eq Limits.Pi.hom_ext Category.assoc Subobject.ofLEMk_comp Category.id_comp Limits.eq_of_epi_equalizer IsSplitEpi.epi Limits.hasInitial_of_unique Unique.instSubsingleton
hasSeparator_op_iff 📖	mathematical	—	HasSeparator Opposite Category.opposite HasCoseparator	—	isCoseparator_unop_iff isSeparator_op_iff
hasTerminal_of_isSeparating 📖	mathematical	ObjectProperty.IsSeparating	Limits.HasTerminal	—	Limits.hasTerminal_of_hasInitial_op hasInitial_of_isCoseparating Limits.hasLimits_op_of_hasColimits ObjectProperty.instSmallOppositeOp_1 ObjectProperty.isCoseparating_op_iff
isCodetecting_empty_of_groupoid 📖	mathematical	—	ObjectProperty.IsCodetecting Bot.bot ObjectProperty Category.toCategoryStruct Pi.instBotForall BooleanAlgebra.toBot Prop.instBooleanAlgebra	—	ObjectProperty.isCodetecting_bot_of_isGroupoid
isCodetecting_iff_isCoseparating 📖	mathematical	—	ObjectProperty.IsCodetecting ObjectProperty.IsCoseparating	—	ObjectProperty.isCodetecting_iff_isCoseparating
isCodetecting_op_iff 📖	mathematical	—	ObjectProperty.IsCodetecting Opposite Category.opposite ObjectProperty.op Category.toCategoryStruct ObjectProperty.IsDetecting	—	ObjectProperty.isCodetecting_op_iff
isCodetecting_unop_iff 📖	mathematical	—	ObjectProperty.IsCodetecting Opposite Category.opposite ObjectProperty.op Category.toCategoryStruct ObjectProperty.IsDetecting	—	ObjectProperty.isCodetecting_op_iff
isCodetector_codetector 📖	mathematical	—	IsCodetector codetector	—	HasCodetector.hasCodetector
isCodetector_coseparator 📖	mathematical	—	IsCodetector coseparator	—	IsCoseparator.isCodetector isCoseparator_coseparator
isCodetector_def 📖	mathematical	—	IsCodetector IsIso	—	ObjectProperty.singleton_iff
isCodetector_iff_reflectsIsomorphisms_yoneda_obj 📖	mathematical	—	IsCodetector Functor.ReflectsIsomorphisms Opposite Category.opposite types Functor.obj Functor Functor.category yoneda	—	isIso_unop_iff IsCodetector.def Function.bijective_iff_existsUnique isIso_iff_bijective isCodetector_def isIso_op_iff isIso_of_reflects_iso
isCodetector_op_iff 📖	mathematical	—	IsCodetector Opposite Category.opposite Opposite.op IsDetector	—	IsDetector.eq_1 IsCodetector.eq_1 ObjectProperty.isCodetecting_op_iff ObjectProperty.op_singleton
isCodetector_unop_iff 📖	mathematical	—	IsCodetector Opposite.unop IsDetector Opposite Category.opposite	—	IsDetector.eq_1 IsCodetector.eq_1 ObjectProperty.isCodetecting_unop_iff ObjectProperty.unop_singleton
isCoseparating_empty_of_thin 📖	mathematical	Quiver.IsThin CategoryStruct.toQuiver Category.toCategoryStruct	ObjectProperty.IsCoseparating Bot.bot ObjectProperty Pi.instBotForall BooleanAlgebra.toBot Prop.instBooleanAlgebra	—	ObjectProperty.isCoseparating_bot_of_isThin
isCoseparating_iff_mono 📖	mathematical	Limits.HasProduct StructuredArrow ObjectProperty.FullSubcategory ObjectProperty.FullSubcategory.category ObjectProperty.ι ObjectProperty.productToFamily	ObjectProperty.IsCoseparating Mono Limits.piObj ObjectProperty.productTo	—	ObjectProperty.isCoseparating_iff_mono
isCoseparating_op_iff 📖	mathematical	—	ObjectProperty.IsCoseparating Opposite Category.opposite ObjectProperty.op Category.toCategoryStruct ObjectProperty.IsSeparating	—	ObjectProperty.isCoseparating_op_iff
isCoseparating_unop_iff 📖	mathematical	—	ObjectProperty.IsCoseparating Opposite Category.opposite ObjectProperty.op Category.toCategoryStruct ObjectProperty.IsSeparating	—	ObjectProperty.isCoseparating_op_iff
isCoseparator_codetector 📖	mathematical	—	IsCoseparator codetector	—	IsCodetector.isCoseparator isCodetector_codetector
isCoseparator_coseparator 📖	mathematical	—	IsCoseparator coseparator	—	HasCoseparator.hasCoseparator
isCoseparator_def 📖	mathematical	—	IsCoseparator	—	ObjectProperty.singleton_iff
isCoseparator_iff_faithful_yoneda_obj 📖	mathematical	—	IsCoseparator Functor.Faithful Opposite Category.opposite types Functor.obj Functor Functor.category yoneda	—	IsCoseparator.def isCoseparator_def Functor.map_injective
isCoseparator_iff_mono 📖	mathematical	Limits.HasProduct Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct	IsCoseparator Mono Limits.piObj Limits.Pi.lift	—	isCoseparator_def Category.assoc Limits.limit.lift_π eq_whisker cancel_mono Limits.limit.hom_ext
isCoseparator_iff_of_isLimit_fan 📖	mathematical	—	IsCoseparator Limits.Cone.pt Discrete discreteCategory Discrete.functor ObjectProperty.IsCoseparating ObjectProperty.ofObj Category.toCategoryStruct	—	IsCoseparator.def Limits.IsLimit.hom_ext Category.assoc isCoseparator_of_isLimit_fan
isCoseparator_of_isLimit_fan 📖	mathematical	ObjectProperty.IsCoseparating ObjectProperty.ofObj Category.toCategoryStruct	IsCoseparator Limits.Cone.pt Discrete discreteCategory Discrete.functor	—	isCoseparator_def Category.assoc Limits.Fan.IsLimit.lift_proj Pi.single_eq_same eq_whisker
isCoseparator_op_iff 📖	mathematical	—	IsCoseparator Opposite Category.opposite Opposite.op IsSeparator	—	IsSeparator.eq_1 IsCoseparator.eq_1 ObjectProperty.isCoseparating_op_iff ObjectProperty.op_singleton
isCoseparator_pi 📖	mathematical	—	IsCoseparator Limits.piObj ObjectProperty.IsCoseparating ObjectProperty.ofObj Category.toCategoryStruct	—	isCoseparator_iff_of_isLimit_fan
isCoseparator_pi_of_isCoseparator 📖	mathematical	IsCoseparator	Limits.piObj	—	isCoseparator_pi ObjectProperty.IsCoseparating.of_le
isCoseparator_prod 📖	mathematical	—	IsCoseparator Limits.prod ObjectProperty.IsCoseparating ObjectProperty.pair Category.toCategoryStruct	—	isCoseparator_iff_of_isLimit_fan
isCoseparator_prod_of_isCoseparator_left 📖	mathematical	IsCoseparator	Limits.prod	—	isCoseparator_prod ObjectProperty.IsCoseparating.of_le
isCoseparator_prod_of_isCoseparator_right 📖	mathematical	IsCoseparator	Limits.prod	—	isCoseparator_prod ObjectProperty.IsCoseparating.of_le
isCoseparator_unop_iff 📖	mathematical	—	IsCoseparator Opposite.unop IsSeparator Opposite Category.opposite	—	IsSeparator.eq_1 IsCoseparator.eq_1 ObjectProperty.isCoseparating_unop_iff ObjectProperty.unop_singleton
isDetecting_empty_of_groupoid 📖	mathematical	—	ObjectProperty.IsDetecting Bot.bot ObjectProperty Category.toCategoryStruct Pi.instBotForall BooleanAlgebra.toBot Prop.instBooleanAlgebra	—	ObjectProperty.isDetecting_bot_of_isGroupoid
isDetecting_iff_isSeparating 📖	mathematical	—	ObjectProperty.IsDetecting ObjectProperty.IsSeparating	—	ObjectProperty.isDetecting_iff_isSeparating
isDetecting_op_iff 📖	mathematical	—	ObjectProperty.IsDetecting Opposite Category.opposite ObjectProperty.op Category.toCategoryStruct ObjectProperty.IsCodetecting	—	ObjectProperty.isDetecting_op_iff
isDetecting_unop_iff 📖	mathematical	—	ObjectProperty.IsDetecting Opposite Category.opposite ObjectProperty.op Category.toCategoryStruct ObjectProperty.IsCodetecting	—	ObjectProperty.isDetecting_op_iff
isDetector_def 📖	mathematical	—	IsDetector IsIso	—	ObjectProperty.singleton_iff
isDetector_detector 📖	mathematical	—	IsDetector detector	—	HasDetector.hasDetector
isDetector_iff_reflectsIsomorphisms_coyoneda_obj 📖	mathematical	—	IsDetector Functor.ReflectsIsomorphisms types Functor.obj Opposite Category.opposite Functor Functor.category coyoneda Opposite.op	—	IsDetector.def Function.bijective_iff_existsUnique isIso_iff_bijective isDetector_def isIso_of_reflects_iso
isDetector_op_iff 📖	mathematical	—	IsDetector Opposite Category.opposite Opposite.op IsCodetector	—	IsDetector.eq_1 IsCodetector.eq_1 ObjectProperty.isDetecting_op_iff ObjectProperty.op_singleton
isDetector_separator 📖	mathematical	—	IsDetector separator	—	IsSeparator.isDetector isSeparator_separator
isDetector_unop_iff 📖	mathematical	—	IsDetector Opposite.unop IsCodetector Opposite Category.opposite	—	IsDetector.eq_1 IsCodetector.eq_1 ObjectProperty.isDetecting_unop_iff ObjectProperty.unop_singleton
isSeparating_empty_of_thin 📖	mathematical	Quiver.IsThin CategoryStruct.toQuiver Category.toCategoryStruct	ObjectProperty.IsSeparating Bot.bot ObjectProperty Pi.instBotForall BooleanAlgebra.toBot Prop.instBooleanAlgebra	—	ObjectProperty.isSeparating_bot_of_isThin
isSeparating_iff_epi 📖	mathematical	Limits.HasCoproduct CostructuredArrow ObjectProperty.FullSubcategory ObjectProperty.FullSubcategory.category ObjectProperty.ι ObjectProperty.coproductFromFamily	ObjectProperty.IsSeparating Epi Limits.sigmaObj ObjectProperty.coproductFrom	—	ObjectProperty.isSeparating_iff_epi
isSeparating_op_iff 📖	mathematical	—	ObjectProperty.IsSeparating Opposite Category.opposite ObjectProperty.op Category.toCategoryStruct ObjectProperty.IsCoseparating	—	ObjectProperty.isSeparating_op_iff
isSeparating_unop_iff 📖	mathematical	—	ObjectProperty.IsSeparating Opposite Category.opposite ObjectProperty.op Category.toCategoryStruct ObjectProperty.IsCoseparating	—	ObjectProperty.isSeparating_op_iff
isSeparator_coprod 📖	mathematical	—	IsSeparator Limits.coprod ObjectProperty.IsSeparating ObjectProperty.pair Category.toCategoryStruct	—	isSeparator_iff_of_isColimit_cofan
isSeparator_coprod_of_isSeparator_left 📖	mathematical	IsSeparator	Limits.coprod	—	isSeparator_coprod ObjectProperty.IsSeparating.of_le
isSeparator_coprod_of_isSeparator_right 📖	mathematical	IsSeparator	Limits.coprod	—	isSeparator_coprod ObjectProperty.IsSeparating.of_le
isSeparator_def 📖	mathematical	—	IsSeparator	—	ObjectProperty.singleton_iff
isSeparator_detector 📖	mathematical	—	IsSeparator detector	—	IsDetector.isSeparator isDetector_detector
isSeparator_iff_epi 📖	mathematical	Limits.HasCoproduct Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct	IsSeparator Epi Limits.sigmaObj Limits.Sigma.desc	—	isSeparator_def Limits.colimit.ι_desc_assoc whisker_eq cancel_epi Limits.colimit.hom_ext
isSeparator_iff_faithful_coyoneda_obj 📖	mathematical	—	IsSeparator Functor.Faithful types Functor.obj Opposite Category.opposite Functor Functor.category coyoneda Opposite.op	—	IsSeparator.def isSeparator_def Functor.map_injective
isSeparator_iff_of_isColimit_cofan 📖	mathematical	—	IsSeparator Limits.Cocone.pt Discrete discreteCategory Discrete.functor ObjectProperty.IsSeparating ObjectProperty.ofObj Category.toCategoryStruct	—	IsSeparator.def Limits.IsColimit.hom_ext Category.assoc isSeparator_of_isColimit_cofan
isSeparator_of_isColimit_cofan 📖	mathematical	ObjectProperty.IsSeparating ObjectProperty.ofObj Category.toCategoryStruct	IsSeparator Limits.Cocone.pt Discrete discreteCategory Discrete.functor	—	isSeparator_def Limits.Cofan.IsColimit.inj_desc_assoc Pi.single_eq_same whisker_eq
isSeparator_op_iff 📖	mathematical	—	IsSeparator Opposite Category.opposite Opposite.op IsCoseparator	—	IsSeparator.eq_1 IsCoseparator.eq_1 ObjectProperty.isSeparating_op_iff ObjectProperty.op_singleton
isSeparator_separator 📖	mathematical	—	IsSeparator separator	—	HasSeparator.hasSeparator
isSeparator_sigma 📖	mathematical	—	IsSeparator Limits.sigmaObj ObjectProperty.IsSeparating ObjectProperty.ofObj Category.toCategoryStruct	—	isSeparator_iff_of_isColimit_cofan
isSeparator_sigma_of_isSeparator 📖	mathematical	IsSeparator	Limits.sigmaObj	—	isSeparator_sigma ObjectProperty.IsSeparating.of_le
isSeparator_unop_iff 📖	mathematical	—	IsSeparator Opposite.unop IsCoseparator Opposite Category.opposite	—	IsSeparator.eq_1 IsCoseparator.eq_1 ObjectProperty.isSeparating_unop_iff ObjectProperty.unop_singleton
thin_of_isCoseparating_empty 📖	mathematical	ObjectProperty.IsCoseparating Bot.bot ObjectProperty Category.toCategoryStruct Pi.instBotForall BooleanAlgebra.toBot Prop.instBooleanAlgebra	Quiver.IsThin CategoryStruct.toQuiver	—	ObjectProperty.isThin_of_isCoseparating_bot
thin_of_isSeparating_empty 📖	mathematical	ObjectProperty.IsSeparating Bot.bot ObjectProperty Category.toCategoryStruct Pi.instBotForall BooleanAlgebra.toBot Prop.instBooleanAlgebra	Quiver.IsThin CategoryStruct.toQuiver	—	ObjectProperty.isThin_of_isSeparating_bot
wellPowered_of_isDetecting 📖	mathematical	ObjectProperty.IsDetecting	WellPowered	—	small_of_injective small_set small_sigma instSmallHomOfLocallySmall Subobject.eq_of_isDetecting
wellPowered_of_isDetector 📖	mathematical	IsDetector	WellPowered locallySmall_of_univLE UnivLE.self	—	wellPowered_of_isDetecting ObjectProperty.instSmallOfObjOfSmall UnivLE.small univLE_of_max UnivLE.self locallySmall_of_univLE
wellPowered_of_isSeparator 📖	mathematical	IsSeparator	WellPowered locallySmall_of_univLE UnivLE.self	—	wellPowered_of_isDetecting ObjectProperty.instSmallOfObjOfSmall UnivLE.small univLE_of_max UnivLE.self locallySmall_of_univLE IsSeparator.isDetector

CategoryTheory.CostructuredArrow

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSeparating_inverseImage_proj 📖	mathematical	CategoryTheory.ObjectProperty.IsSeparating	CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.ObjectProperty.inverseImage proj	—	ext
isSeparating_proj_preimage 📖	mathematical	CategoryTheory.ObjectProperty.IsSeparating	CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.ObjectProperty.inverseImage proj	—	isSeparating_inverseImage_proj

CategoryTheory.HasCodetector

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasCodetector 📖	mathematical	—	CategoryTheory.IsCodetector	—	—
hasCoseparator 📖	mathematical	—	CategoryTheory.HasCoseparator	—	CategoryTheory.isCoseparator_codetector
hasDetector_of_hasCodetector_op 📖	mathematical	—	CategoryTheory.HasDetector	—	—
hasDetector_op 📖	mathematical	—	CategoryTheory.HasDetector Opposite CategoryTheory.Category.opposite	—	—

CategoryTheory.HasCoseparator

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasCodetector 📖	mathematical	—	CategoryTheory.HasCodetector	—	CategoryTheory.isCodetector_coseparator
hasCoseparator 📖	mathematical	—	CategoryTheory.IsCoseparator	—	—
hasSeparator_of_hasCoseparator_op 📖	mathematical	—	CategoryTheory.HasSeparator	—	—
hasSeparator_op 📖	mathematical	—	CategoryTheory.HasSeparator Opposite CategoryTheory.Category.opposite	—	—
of_equivalence 📖	mathematical	—	CategoryTheory.HasCoseparator	—	CategoryTheory.IsCoseparator.of_equivalence CategoryTheory.isCoseparator_coseparator

CategoryTheory.HasDetector

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasCodetector_of_hasDetector_op 📖	mathematical	—	CategoryTheory.HasCodetector	—	—
hasCodetector_op 📖	mathematical	—	CategoryTheory.HasCodetector Opposite CategoryTheory.Category.opposite	—	—
hasDetector 📖	mathematical	—	CategoryTheory.IsDetector	—	—
hasSeparator 📖	mathematical	—	CategoryTheory.HasSeparator	—	CategoryTheory.isSeparator_detector
wellPowered 📖	mathematical	—	CategoryTheory.WellPowered CategoryTheory.locallySmall_of_univLE UnivLE.self	—	CategoryTheory.wellPowered_of_isDetector CategoryTheory.isDetector_detector

CategoryTheory.HasSeparator

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasCoseparator_of_hasSeparator_op 📖	mathematical	—	CategoryTheory.HasCoseparator	—	—
hasCoseparator_op 📖	mathematical	—	CategoryTheory.HasCoseparator Opposite CategoryTheory.Category.opposite	—	—
hasDetector 📖	mathematical	—	CategoryTheory.HasDetector	—	CategoryTheory.isDetector_separator
hasSeparator 📖	mathematical	—	CategoryTheory.IsSeparator	—	—
of_equivalence 📖	mathematical	—	CategoryTheory.HasSeparator	—	CategoryTheory.IsSeparator.of_equivalence CategoryTheory.isSeparator_separator
wellPowered 📖	mathematical	—	CategoryTheory.WellPowered CategoryTheory.locallySmall_of_univLE UnivLE.self	—	CategoryTheory.HasDetector.wellPowered hasDetector

CategoryTheory.IsCodetecting

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCoseparating 📖	mathematical	CategoryTheory.ObjectProperty.IsCodetecting	CategoryTheory.ObjectProperty.IsCoseparating	—	CategoryTheory.ObjectProperty.IsCodetecting.isCoseparating
isIso_iff_of_epi 📖	mathematical	CategoryTheory.ObjectProperty.IsCodetecting	CategoryTheory.IsIso CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda Opposite.op CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.ObjectProperty.IsCodetecting.isIso_iff_of_epi
mono 📖	—	CategoryTheory.ObjectProperty.IsCodetecting CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le	—	—	CategoryTheory.ObjectProperty.IsCodetecting.of_le

CategoryTheory.IsCodetector

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
def 📖	mathematical	CategoryTheory.IsCodetector ExistsUnique Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp	CategoryTheory.IsIso	—	CategoryTheory.isCodetector_def
isCoseparator 📖	mathematical	CategoryTheory.IsCodetector	CategoryTheory.IsCoseparator	—	CategoryTheory.ObjectProperty.IsCodetecting.isCoseparating

CategoryTheory.IsCoseparating

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCodetecting 📖	mathematical	CategoryTheory.ObjectProperty.IsCoseparating	CategoryTheory.ObjectProperty.IsCodetecting	—	CategoryTheory.ObjectProperty.IsCoseparating.isCodetecting
mono 📖	—	CategoryTheory.ObjectProperty.IsCoseparating CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le	—	—	CategoryTheory.ObjectProperty.IsCoseparating.of_le
of_equivalence 📖	mathematical	CategoryTheory.ObjectProperty.IsCoseparating	CategoryTheory.ObjectProperty.strictMap CategoryTheory.Equivalence.functor	—	CategoryTheory.ObjectProperty.IsCoseparating.of_equivalence

CategoryTheory.IsCoseparator

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
def 📖	—	CategoryTheory.IsCoseparator CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—	CategoryTheory.isCoseparator_def
isCodetector 📖	mathematical	CategoryTheory.IsCoseparator	CategoryTheory.IsCodetector	—	CategoryTheory.ObjectProperty.IsCoseparating.isCodetecting
of_equivalence 📖	mathematical	CategoryTheory.IsCoseparator	CategoryTheory.Functor.obj CategoryTheory.Equivalence.functor	—	CategoryTheory.ObjectProperty.strictMap_singleton CategoryTheory.ObjectProperty.IsCoseparating.of_equivalence

CategoryTheory.IsDetecting

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIso_iff_of_mono 📖	mathematical	CategoryTheory.ObjectProperty.IsDetecting	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.types Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.coyoneda Opposite.op CategoryTheory.Functor.map	—	CategoryTheory.ObjectProperty.IsDetecting.isIso_iff_of_mono
isSeparating 📖	mathematical	CategoryTheory.ObjectProperty.IsDetecting	CategoryTheory.ObjectProperty.IsSeparating	—	CategoryTheory.ObjectProperty.IsDetecting.isSeparating
mono 📖	—	CategoryTheory.ObjectProperty.IsDetecting CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le	—	—	CategoryTheory.ObjectProperty.IsDetecting.of_le

CategoryTheory.IsDetector

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
def 📖	mathematical	CategoryTheory.IsDetector ExistsUnique Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp	CategoryTheory.IsIso	—	CategoryTheory.isDetector_def
isSeparator 📖	mathematical	CategoryTheory.IsDetector	CategoryTheory.IsSeparator	—	CategoryTheory.ObjectProperty.IsDetecting.isSeparating

CategoryTheory.IsSeparating

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isDetecting 📖	mathematical	CategoryTheory.ObjectProperty.IsSeparating	CategoryTheory.ObjectProperty.IsDetecting	—	CategoryTheory.ObjectProperty.IsSeparating.isDetecting
isSeparator_coproduct 📖	mathematical	CategoryTheory.ObjectProperty.IsSeparating CategoryTheory.ObjectProperty.ofObj CategoryTheory.Category.toCategoryStruct	CategoryTheory.IsSeparator CategoryTheory.Limits.sigmaObj	—	CategoryTheory.ObjectProperty.IsSeparating.isSeparator_coproduct
mono 📖	—	CategoryTheory.ObjectProperty.IsSeparating CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le	—	—	CategoryTheory.ObjectProperty.IsSeparating.of_le
of_equivalence 📖	mathematical	CategoryTheory.ObjectProperty.IsSeparating	CategoryTheory.ObjectProperty.strictMap CategoryTheory.Equivalence.functor	—	CategoryTheory.ObjectProperty.IsSeparating.of_equivalence

CategoryTheory.IsSeparator

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
def 📖	—	CategoryTheory.IsSeparator CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—	CategoryTheory.isSeparator_def
isDetector 📖	mathematical	CategoryTheory.IsSeparator	CategoryTheory.IsDetector	—	CategoryTheory.ObjectProperty.IsSeparating.isDetecting
of_equivalence 📖	mathematical	CategoryTheory.IsSeparator	CategoryTheory.Functor.obj CategoryTheory.Equivalence.functor	—	CategoryTheory.ObjectProperty.strictMap_singleton CategoryTheory.ObjectProperty.IsSeparating.of_equivalence

CategoryTheory.ObjectProperty

Definitions

Name	Category	Theorems
IsCodetecting 📖	MathDef	14 math math: isDetecting_op_iff, CategoryTheory.isCodetecting_empty_of_groupoid, isCodetecting_bot_of_isGroupoid, CategoryTheory.isCodetecting_iff_isCoseparating, CategoryTheory.IsCoseparating.isCodetecting, IsCoseparating.isCodetecting, isDetecting_unop_iff, CategoryTheory.isCodetecting_op_iff, isCodetecting_unop_iff, CategoryTheory.isDetecting_op_iff, isCodetecting_op_iff, CategoryTheory.isDetecting_unop_iff, CategoryTheory.isCodetecting_unop_iff, isCodetecting_iff_isCoseparating
IsCoseparating 📖	MathDef	22 math math: CategoryTheory.isSeparating_unop_iff, CategoryTheory.isCoseparating_empty_of_thin, IsCodetecting.isCoseparating, isCoseparating_iff_mono, CategoryTheory.isCodetecting_iff_isCoseparating, isCoseparating_op_iff, CategoryTheory.isSeparating_op_iff, isSeparating_unop_iff, CategoryTheory.isCoseparating_op_iff, CategoryTheory.isCoseparating_iff_mono, CategoryTheory.isCoseparator_prod, CategoryTheory.Preadditive.isCoseparating_iff, CategoryTheory.isCoseparator_pi, isCoseparating_unop_iff, CategoryTheory.isCoseparating_unop_iff, CategoryTheory.isCoseparator_iff_of_isLimit_fan, isSeparating_op_iff, IsCoseparating.mk_of_exists_limitsOfShape, CategoryTheory.IsCodetecting.isCoseparating, isCoseparating_bot_of_isThin, isCodetecting_iff_isCoseparating, IsCoseparating.mk_of_exists_mono
IsDetecting 📖	MathDef	15 math math: CategoryTheory.isDetecting_iff_isSeparating, isDetecting_op_iff, isDetecting_bot_of_isGroupoid, CategoryTheory.IsSeparating.isDetecting, isDetecting_unop_iff, PresheafOfModules.freeYoneda.isDetecting, IsSeparating.isDetecting, CategoryTheory.isCodetecting_op_iff, isCodetecting_unop_iff, CategoryTheory.isDetecting_op_iff, isCodetecting_op_iff, CategoryTheory.isDetecting_unop_iff, CategoryTheory.isDetecting_empty_of_groupoid, isDetecting_iff_isSeparating, CategoryTheory.isCodetecting_unop_iff
IsSeparating 📖	MathDef	26 math math: CategoryTheory.isDetecting_iff_isSeparating, CategoryTheory.isSeparating_iff_epi, CategoryTheory.isSeparating_unop_iff, CategoryTheory.isSeparator_coprod, isCoseparating_op_iff, CategoryTheory.Preadditive.isSeparating_iff, CategoryTheory.isSeparating_op_iff, CategoryTheory.isSeparator_sigma, PresheafOfModules.freeYoneda.isSeparating, isSeparating_unop_iff, CategoryTheory.isCoseparating_op_iff, IsDetecting.isSeparating, CategoryTheory.isSeparating_empty_of_thin, isSeparating_iff_epi, IsSeparating.mk_of_exists_epi, CategoryTheory.isSeparator_iff_of_isColimit_cofan, isStrongGenerator_iff, IsSeparating.mk_of_exists_colimitsOfShape, isSeparating_bot_of_isThin, isCoseparating_unop_iff, CategoryTheory.isCoseparating_unop_iff, CategoryTheory.IsDetecting.isSeparating, CategoryTheory.Ind.isSeparating_range_yoneda, IsStrongGenerator.isSeparating, isSeparating_op_iff, isDetecting_iff_isSeparating
coproductFrom 📖	CompOp	4 math math: CategoryTheory.isSeparating_iff_epi, isSeparating_iff_epi, IsStrongGenerator.extremalEpi_coproductFrom, IsSeparating.epi_coproductFrom
coproductFromFamily 📖	CompOp	2 math math: IsStrongGenerator.extremalEpi_coproductFrom, IsSeparating.epi_coproductFrom
productTo 📖	CompOp	3 math math: isCoseparating_iff_mono, CategoryTheory.isCoseparating_iff_mono, IsCoseparating.mono_productTo
productToFamily 📖	CompOp	1 math math: IsCoseparating.mono_productTo
ιCoproductFrom 📖	CompOp	—
πProductTo 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCodetecting_bot_of_isGroupoid 📖	mathematical	—	IsCodetecting Bot.bot CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.instBotForall BooleanAlgebra.toBot Prop.instBooleanAlgebra	—	CategoryTheory.IsGroupoid.all_isIso
isCodetecting_iff_isCoseparating 📖	mathematical	—	IsCodetecting IsCoseparating	—	IsCodetecting.isCoseparating IsCoseparating.isCodetecting
isCodetecting_op_iff 📖	mathematical	—	IsCodetecting Opposite CategoryTheory.Category.opposite op CategoryTheory.Category.toCategoryStruct IsDetecting	—	CategoryTheory.isIso_op_iff CategoryTheory.isIso_unop_iff
isCodetecting_unop_iff 📖	mathematical	—	IsCodetecting unop CategoryTheory.Category.toCategoryStruct IsDetecting Opposite CategoryTheory.Category.opposite	—	isDetecting_op_iff
isCoseparating_bot_of_isThin 📖	mathematical	Quiver.IsThin CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	IsCoseparating Bot.bot CategoryTheory.ObjectProperty Pi.instBotForall BooleanAlgebra.toBot Prop.instBooleanAlgebra	—	—
isCoseparating_iff_mono 📖	mathematical	CategoryTheory.Limits.HasProduct CategoryTheory.StructuredArrow FullSubcategory FullSubcategory.category ι productToFamily	IsCoseparating CategoryTheory.Mono CategoryTheory.Limits.piObj productTo	—	IsCoseparating.mono_productTo IsCoseparating.mk_of_exists_mono FullSubcategory.property
isCoseparating_op_iff 📖	mathematical	—	IsCoseparating Opposite CategoryTheory.Category.opposite op CategoryTheory.Category.toCategoryStruct IsSeparating	—	—
isCoseparating_unop_iff 📖	mathematical	—	IsCoseparating unop CategoryTheory.Category.toCategoryStruct IsSeparating Opposite CategoryTheory.Category.opposite	—	isSeparating_op_iff
isDetecting_bot_of_isGroupoid 📖	mathematical	—	IsDetecting Bot.bot CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.instBotForall BooleanAlgebra.toBot Prop.instBooleanAlgebra	—	CategoryTheory.IsGroupoid.all_isIso
isDetecting_iff_isSeparating 📖	mathematical	—	IsDetecting IsSeparating	—	IsDetecting.isSeparating IsSeparating.isDetecting
isDetecting_op_iff 📖	mathematical	—	IsDetecting Opposite CategoryTheory.Category.opposite op CategoryTheory.Category.toCategoryStruct IsCodetecting	—	CategoryTheory.isIso_op_iff CategoryTheory.isIso_unop_iff
isDetecting_unop_iff 📖	mathematical	—	IsDetecting unop CategoryTheory.Category.toCategoryStruct IsCodetecting Opposite CategoryTheory.Category.opposite	—	isCodetecting_op_iff
isGroupoid_of_isCodetecting_bot 📖	mathematical	IsCodetecting Bot.bot CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.instBotForall BooleanAlgebra.toBot Prop.instBooleanAlgebra	CategoryTheory.IsGroupoid	—	instIsEmptyFalse
isGroupoid_of_isDetecting_bot 📖	mathematical	IsDetecting Bot.bot CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.instBotForall BooleanAlgebra.toBot Prop.instBooleanAlgebra	CategoryTheory.IsGroupoid	—	instIsEmptyFalse
isSeparating_bot_of_isThin 📖	mathematical	Quiver.IsThin CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	IsSeparating Bot.bot CategoryTheory.ObjectProperty Pi.instBotForall BooleanAlgebra.toBot Prop.instBooleanAlgebra	—	—
isSeparating_iff_epi 📖	mathematical	CategoryTheory.Limits.HasCoproduct CategoryTheory.CostructuredArrow FullSubcategory FullSubcategory.category ι coproductFromFamily	IsSeparating CategoryTheory.Epi CategoryTheory.Limits.sigmaObj coproductFrom	—	IsSeparating.epi_coproductFrom IsSeparating.mk_of_exists_epi FullSubcategory.property
isSeparating_op_iff 📖	mathematical	—	IsSeparating Opposite CategoryTheory.Category.opposite op CategoryTheory.Category.toCategoryStruct IsCoseparating	—	—
isSeparating_unop_iff 📖	mathematical	—	IsSeparating unop CategoryTheory.Category.toCategoryStruct IsCoseparating Opposite CategoryTheory.Category.opposite	—	isCoseparating_op_iff
isThin_of_isCoseparating_bot 📖	mathematical	IsCoseparating Bot.bot CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.instBotForall BooleanAlgebra.toBot Prop.instBooleanAlgebra	Quiver.IsThin CategoryTheory.CategoryStruct.toQuiver	—	instIsEmptyFalse
isThin_of_isSeparating_bot 📖	mathematical	IsSeparating Bot.bot CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.instBotForall BooleanAlgebra.toBot Prop.instBooleanAlgebra	Quiver.IsThin CategoryTheory.CategoryStruct.toQuiver	—	instIsEmptyFalse

CategoryTheory.ObjectProperty.IsCodetecting

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCoseparating 📖	mathematical	CategoryTheory.ObjectProperty.IsCodetecting	CategoryTheory.ObjectProperty.IsCoseparating	—	CategoryTheory.ObjectProperty.IsDetecting.isSeparating CategoryTheory.Limits.hasEqualizers_opposite
isIso_iff_of_epi 📖	mathematical	CategoryTheory.ObjectProperty.IsCodetecting	CategoryTheory.IsIso CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda Opposite.op CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.isIso_iff_coyoneda_map_bijective existsUnique_of_exists_of_unique CategoryTheory.cancel_epi
of_le 📖	—	CategoryTheory.ObjectProperty.IsCodetecting CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le	—	—	—

CategoryTheory.ObjectProperty.IsCoseparating

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
epi_iff 📖	mathematical	CategoryTheory.ObjectProperty.IsCoseparating	CategoryTheory.Epi	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker'
isCodetecting 📖	mathematical	CategoryTheory.ObjectProperty.IsCoseparating	CategoryTheory.ObjectProperty.IsCodetecting	—	CategoryTheory.ObjectProperty.IsSeparating.isDetecting CategoryTheory.balanced_opposite
mk_of_exists_limitsOfShape 📖	mathematical	CategoryTheory.ObjectProperty.limitsOfShape	CategoryTheory.ObjectProperty.IsCoseparating	—	CategoryTheory.Limits.IsLimit.hom_ext CategoryTheory.ObjectProperty.LimitOfShape.prop_diag_obj
mk_of_exists_mono 📖	mathematical	CategoryTheory.Mono CategoryTheory.Limits.Cone.pt CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor	CategoryTheory.ObjectProperty.IsCoseparating	—	CategoryTheory.cancel_mono CategoryTheory.Limits.Fan.IsLimit.hom_ext CategoryTheory.Category.assoc
mono_productTo 📖	mathematical	CategoryTheory.ObjectProperty.IsCoseparating	CategoryTheory.Mono CategoryTheory.Limits.piObj CategoryTheory.StructuredArrow CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.ObjectProperty.ι CategoryTheory.ObjectProperty.productToFamily CategoryTheory.ObjectProperty.productTo	—	CategoryTheory.Category.assoc CategoryTheory.Limits.limit.lift_π CategoryTheory.eq_whisker
of_equivalence 📖	mathematical	CategoryTheory.ObjectProperty.IsCoseparating	CategoryTheory.ObjectProperty.strictMap CategoryTheory.Equivalence.functor	—	CategoryTheory.Functor.map_injective CategoryTheory.Equivalence.faithful_inverse Equiv.surjective CategoryTheory.Adjunction.homEquiv_counit CategoryTheory.ObjectProperty.strictMap_obj
of_le 📖	—	CategoryTheory.ObjectProperty.IsCoseparating CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le	—	—	—

CategoryTheory.ObjectProperty.IsDetecting

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIso_iff_of_mono 📖	mathematical	CategoryTheory.ObjectProperty.IsDetecting	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.types Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.coyoneda Opposite.op CategoryTheory.Functor.map	—	CategoryTheory.isIso_iff_yoneda_map_bijective existsUnique_of_exists_of_unique CategoryTheory.cancel_mono
isSeparating 📖	mathematical	CategoryTheory.ObjectProperty.IsDetecting	CategoryTheory.ObjectProperty.IsSeparating	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.equalizer.existsUnique CategoryTheory.Limits.eq_of_epi_equalizer CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso
of_le 📖	—	CategoryTheory.ObjectProperty.IsDetecting CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le	—	—	—

CategoryTheory.ObjectProperty.IsSeparating

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
epi_coproductFrom 📖	mathematical	CategoryTheory.ObjectProperty.IsSeparating	CategoryTheory.Epi CategoryTheory.Limits.sigmaObj CategoryTheory.CostructuredArrow CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.ObjectProperty.ι CategoryTheory.ObjectProperty.coproductFromFamily CategoryTheory.ObjectProperty.coproductFrom	—	CategoryTheory.Limits.colimit.ι_desc_assoc CategoryTheory.whisker_eq
isDetecting 📖	mathematical	CategoryTheory.ObjectProperty.IsSeparating	CategoryTheory.ObjectProperty.IsDetecting	—	CategoryTheory.isIso_iff_mono_and_epi CategoryTheory.Category.assoc
isSeparator_coproduct 📖	mathematical	CategoryTheory.ObjectProperty.IsSeparating CategoryTheory.ObjectProperty.ofObj CategoryTheory.Category.toCategoryStruct	CategoryTheory.IsSeparator CategoryTheory.Limits.sigmaObj	—	CategoryTheory.isSeparator_sigma
mk_of_exists_colimitsOfShape 📖	mathematical	CategoryTheory.ObjectProperty.colimitsOfShape	CategoryTheory.ObjectProperty.IsSeparating	—	CategoryTheory.Limits.IsColimit.hom_ext CategoryTheory.ObjectProperty.ColimitOfShape.prop_diag_obj
mk_of_exists_epi 📖	mathematical	CategoryTheory.Epi CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor	CategoryTheory.ObjectProperty.IsSeparating	—	CategoryTheory.cancel_epi CategoryTheory.Limits.Cofan.IsColimit.hom_ext CategoryTheory.Category.assoc
mono_iff 📖	mathematical	CategoryTheory.ObjectProperty.IsSeparating	CategoryTheory.Mono	—	CategoryTheory.Category.assoc
of_equivalence 📖	mathematical	CategoryTheory.ObjectProperty.IsSeparating	CategoryTheory.ObjectProperty.strictMap CategoryTheory.Equivalence.functor	—	CategoryTheory.Functor.map_injective CategoryTheory.Equivalence.faithful_inverse Equiv.surjective CategoryTheory.Adjunction.homEquiv_unit CategoryTheory.Category.assoc CategoryTheory.ObjectProperty.strictMap_obj
of_le 📖	—	CategoryTheory.ObjectProperty.IsSeparating CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le	—	—	—

CategoryTheory.StructuredArrow

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCoseparating_inverseImage_proj 📖	mathematical	CategoryTheory.ObjectProperty.IsCoseparating	CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.ObjectProperty.inverseImage proj	—	ext
isCoseparating_proj_preimage 📖	mathematical	CategoryTheory.ObjectProperty.IsCoseparating	CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.ObjectProperty.inverseImage proj	—	isCoseparating_inverseImage_proj

CategoryTheory.Subobject

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_of_isDetecting 📖	—	CategoryTheory.ObjectProperty.IsDetecting Factors	—	—	inf_eq_of_isDetecting inf_comm
eq_of_le_of_isDetecting 📖	—	CategoryTheory.ObjectProperty.IsDetecting CategoryTheory.Subobject Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject Factors	—	—	factors_iff CategoryTheory.cancel_mono arrow_mono CategoryTheory.Category.assoc ofLE_arrow factorThru_arrow instMonoOfLE le_antisymm le_of_comm
inf_eq_of_isDetecting 📖	mathematical	CategoryTheory.ObjectProperty.IsDetecting Factors	CategoryTheory.Subobject SemilatticeInf.toMin semilatticeInf	—	eq_of_le_of_isDetecting inf_le_left inf_factors

---

← Back to Index