Documentation Verification Report

WellPowered

📁 Source: Mathlib/CategoryTheory/Subobject/WellPowered.lean

Statistics

Metric	Count
Definitions `WellPowered`	1
Theorems `subobject_small`, `essentiallySmall_monoOver`, `essentiallySmall_monoOver_iff_small_subobject`, `instWellPoweredShrinkHoms`, `small_subobject`, `wellPowered_congr`, `wellPowered_of_equiv`, `wellPowered_of_essentiallySmall_monoOver`, `wellPowered_of_smallCategory`	9
Total	10

CategoryTheory

Definitions

Name	Category	Theorems
`WellPowered` 📖	CompData	18 math math: `wellPowered_of_isSeparator`, `instWellPoweredShrinkHoms`, `wellPowered_of_smallCategory`, `wellPowered_congr`, `wellPowered_of_isDetector`, `wellPowered_of_isDetecting`, `wellPowered_of_equiv`, `HasSeparator.wellPowered`, `ModuleCat.wellPowered_moduleCat`, `AddCommGrpCat.wellPowered_addCommGrp`, `IsGrothendieckAbelian.wellPowered`, `PresheafOfModules.wellPowered`, `StructuredArrow.wellPowered_structuredArrow`, `CostructuredArrow.well_copowered_costructuredArrow`, `HasDetector.wellPowered`, `instWellPoweredType`, `Abelian.wellPowered_opposite`, `wellPowered_of_essentiallySmall_monoOver`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`essentiallySmall_monoOver` 📖	mathematical	—	`EssentiallySmall` `MonoOver` `ObjectProperty.FullSubcategory.category` `Over` `instCategoryOver` `Over.isMono`	—	`essentiallySmall_monoOver_iff_small_subobject` `WellPowered.subobject_small`
`essentiallySmall_monoOver_iff_small_subobject` 📖	mathematical	—	`EssentiallySmall` `MonoOver` `ObjectProperty.FullSubcategory.category` `Over` `instCategoryOver` `Over.isMono` `Small` `Subobject`	—	`essentiallySmall_iff_of_thin` `MonoOver.isThin`
`instWellPoweredShrinkHoms` 📖	mathematical	—	`WellPowered` `ShrinkHoms` `ShrinkHoms.instCategory` `locallySmall_of_univLE` `UnivLE.self`	—	`wellPowered_of_equiv` `locallySmall_of_univLE` `UnivLE.self`
`small_subobject` 📖	mathematical	—	`Small` `Subobject`	—	`WellPowered.subobject_small`
`wellPowered_congr` 📖	mathematical	—	`WellPowered`	—	`wellPowered_of_equiv`
`wellPowered_of_equiv` 📖	mathematical	—	`WellPowered`	—	`wellPowered_of_essentiallySmall_monoOver` `essentiallySmall_congr` `essentiallySmall_monoOver`
`wellPowered_of_essentiallySmall_monoOver` 📖	mathematical	`EssentiallySmall` `MonoOver` `ObjectProperty.FullSubcategory.category` `Over` `instCategoryOver` `Over.isMono`	`WellPowered`	—	`essentiallySmall_monoOver_iff_small_subobject`
`wellPowered_of_smallCategory` 📖	mathematical	—	`WellPowered` `locallySmall_of_univLE` `UnivLE.self`	—	`locallySmall_of_univLE` `UnivLE.self` `UnivLE.small`

CategoryTheory.WellPowered

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`subobject_small` 📖	mathematical	—	`Small` `CategoryTheory.Subobject`	—	—

---

← Back to Index