Documentation Verification Report

StrongGenerator

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

Statistics

Metric	Count
Definitions `IsStrongGenerator`	1
Theorems `exists_of_mono_not_isIso`, `exists_of_subobject_ne_top`, `extremalEpi_coproductFrom`, `isIso_of_mono`, `isSeparating`, `mk_of_exists_colimitsOfShape`, `mk_of_exists_extremalEpi`, `subobject_eq_top`, `isStrongGenerator_iff`, `isStrongGenerator_iff_exists_extremalEpi`	10
Total	11

CategoryTheory.ObjectProperty

Definitions

Name	Category	Theorems
`IsStrongGenerator` 📖	MathDef	7 math math: `CategoryTheory.IsCardinalLocallyPresentable.iff_exists_isStrongGenerator`, `IsStrongGenerator.mk_of_exists_extremalEpi`, `isStrongGenerator_iff_exists_extremalEpi`, `IsCardinalFilteredGenerator.isStrongGenerator`, `IsStrongGenerator.mk_of_exists_colimitsOfShape`, `isStrongGenerator_iff`, `CategoryTheory.Functor.isStrongGenerator_of_isDense`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isStrongGenerator_iff` 📖	mathematical	—	`IsStrongGenerator` `IsSeparating` `CategoryTheory.IsIso`	—	`CategoryTheory.Subobject.isIso_iff_mk_eq_top` `CategoryTheory.Subobject.mk_factors_iff` `CategoryTheory.Subobject.isIso_arrow_iff_eq_top` `CategoryTheory.Subobject.arrow_mono` `CategoryTheory.Subobject.factorThru_arrow`
`isStrongGenerator_iff_exists_extremalEpi` 📖	mathematical	`CategoryTheory.Limits.HasCoproducts`	`IsStrongGenerator` `CategoryTheory.ExtremalEpi` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor`	—	`CategoryTheory.Limits.hasCoproductsOfShape_of_small` `CategoryTheory.CostructuredArrow.instSmallOfLocallySmall` `instSmallFullSubcategoryOfSmall` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `FullSubcategory.property` `IsStrongGenerator.extremalEpi_coproductFrom` `IsStrongGenerator.mk_of_exists_extremalEpi`

CategoryTheory.ObjectProperty.IsStrongGenerator

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_of_mono_not_isIso` 📖	—	`CategoryTheory.ObjectProperty.IsStrongGenerator` `CategoryTheory.IsIso`	—	—	`isIso_of_mono` `Mathlib.Tactic.Push.not_forall_eq`
`exists_of_subobject_ne_top` 📖	mathematical	`CategoryTheory.ObjectProperty.IsStrongGenerator`	`CategoryTheory.Subobject.Factors`	—	`subobject_eq_top`
`extremalEpi_coproductFrom` 📖	mathematical	`CategoryTheory.ObjectProperty.IsStrongGenerator`	`CategoryTheory.ExtremalEpi` `CategoryTheory.Limits.sigmaObj` `CategoryTheory.CostructuredArrow` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.ObjectProperty.ι` `CategoryTheory.ObjectProperty.coproductFromFamily` `CategoryTheory.ObjectProperty.coproductFrom`	—	`CategoryTheory.ObjectProperty.IsSeparating.epi_coproductFrom` `isSeparating` `isIso_of_mono` `CategoryTheory.Category.assoc` `CategoryTheory.Limits.colimit.ι_desc`
`isIso_of_mono` 📖	mathematical	`CategoryTheory.ObjectProperty.IsStrongGenerator` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.CategoryStruct.comp`	`CategoryTheory.IsIso`	—	`CategoryTheory.ObjectProperty.isStrongGenerator_iff`
`isSeparating` 📖	mathematical	`CategoryTheory.ObjectProperty.IsStrongGenerator`	`CategoryTheory.ObjectProperty.IsSeparating`	—	—
`mk_of_exists_colimitsOfShape` 📖	mathematical	`CategoryTheory.ObjectProperty.colimitsOfShape`	`CategoryTheory.ObjectProperty.IsStrongGenerator`	—	`CategoryTheory.ObjectProperty.isStrongGenerator_iff` `CategoryTheory.ObjectProperty.IsSeparating.mk_of_exists_colimitsOfShape` `CategoryTheory.Category.comp_id` `CategoryTheory.cancel_mono` `CategoryTheory.Category.assoc` `CategoryTheory.NatTrans.naturality` `CategoryTheory.Limits.IsColimit.hom_ext` `CategoryTheory.Limits.IsColimit.fac_assoc` `CategoryTheory.ObjectProperty.ColimitOfShape.prop_diag_obj` `CategoryTheory.Category.id_comp`
`mk_of_exists_extremalEpi` 📖	mathematical	`CategoryTheory.ExtremalEpi` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor`	`CategoryTheory.ObjectProperty.IsStrongGenerator`	—	`CategoryTheory.ObjectProperty.isStrongGenerator_iff` `CategoryTheory.ObjectProperty.IsSeparating.mk_of_exists_epi` `CategoryTheory.ExtremalEpi.toEpi` `CategoryTheory.ExtremalEpi.isIso` `CategoryTheory.Limits.Cofan.IsColimit.hom_ext` `CategoryTheory.Limits.Cofan.IsColimit.fac_assoc`
`subobject_eq_top` 📖	mathematical	`CategoryTheory.ObjectProperty.IsStrongGenerator` `CategoryTheory.Subobject.Factors`	`Top.top` `CategoryTheory.Subobject` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubobject` `CategoryTheory.Subobject.orderTop`	—	—

---

← Back to Index