Widesubcategory

📁 Source: Mathlib/CategoryTheory/Widesubcategory.lean

Statistics

Metric	Count
Definitions InducedWideCategory, category, hasCoeToSort, WideSubcategory, category, obj, wideInducedFunctor, wideSubcategoryInclusion	8
Theorems category_comp_coe, category_id_coe, faithful, comp_def, ext, ext_iff, id_def, wideInducedFunctor_map, wideInducedFunctor_obj, faithful, map, obj	12
Total	20

CategoryTheory

Definitions

Name	Category	Theorems
InducedWideCategory 📖	CompOp	5 math math: InducedWideCategory.faithful, wideInducedFunctor_obj, InducedWideCategory.category_comp_coe, wideInducedFunctor_map, InducedWideCategory.category_id_coe
WideSubcategory 📖	CompData	5 math math: wideSubcategoryInclusion.obj, WideSubcategory.id_def, wideSubcategory.faithful, WideSubcategory.comp_def, wideSubcategoryInclusion.map
wideInducedFunctor 📖	CompOp	3 math math: InducedWideCategory.faithful, wideInducedFunctor_obj, wideInducedFunctor_map
wideSubcategoryInclusion 📖	CompOp	3 math math: wideSubcategoryInclusion.obj, wideSubcategory.faithful, wideSubcategoryInclusion.map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
wideInducedFunctor_map 📖	mathematical	—	Functor.map InducedWideCategory InducedWideCategory.category wideInducedFunctor Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Set Set.instMembership setOf	—	—
wideInducedFunctor_obj 📖	mathematical	—	Functor.obj InducedWideCategory InducedWideCategory.category wideInducedFunctor	—	—

CategoryTheory.InducedWideCategory

Definitions

Name	Category	Theorems
category 📖	CompOp	5 math math: faithful, CategoryTheory.wideInducedFunctor_obj, category_comp_coe, CategoryTheory.wideInducedFunctor_map, category_id_coe
hasCoeToSort 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
category_comp_coe 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Set Set.instMembership setOf CategoryTheory.CategoryStruct.comp CategoryTheory.InducedWideCategory category	—	—
category_id_coe 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Set Set.instMembership setOf CategoryTheory.CategoryStruct.id CategoryTheory.InducedWideCategory category	—	—
faithful 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.InducedWideCategory category CategoryTheory.wideInducedFunctor	—	—

CategoryTheory.WideSubcategory

Definitions

Name	Category	Theorems
category 📖	CompOp	5 math math: CategoryTheory.wideSubcategoryInclusion.obj, id_def, CategoryTheory.wideSubcategory.faithful, comp_def, CategoryTheory.wideSubcategoryInclusion.map
obj 📖	CompOp	5 math math: CategoryTheory.wideSubcategoryInclusion.obj, id_def, comp_def, CategoryTheory.wideSubcategoryInclusion.map, ext_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_def 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj Set Set.instMembership setOf CategoryTheory.CategoryStruct.comp CategoryTheory.WideSubcategory category	—	—
ext 📖	—	obj	—	—	—
ext_iff 📖	mathematical	—	obj	—	ext
id_def 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj Set Set.instMembership setOf CategoryTheory.CategoryStruct.id CategoryTheory.WideSubcategory category	—	—

CategoryTheory.wideSubcategory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
faithful 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.WideSubcategory CategoryTheory.WideSubcategory.category CategoryTheory.wideSubcategoryInclusion	—	CategoryTheory.InducedWideCategory.faithful

CategoryTheory.wideSubcategoryInclusion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.WideSubcategory CategoryTheory.WideSubcategory.category CategoryTheory.wideSubcategoryInclusion Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.WideSubcategory.obj Set Set.instMembership setOf	—	—
obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.WideSubcategory CategoryTheory.WideSubcategory.category CategoryTheory.wideSubcategoryInclusion CategoryTheory.WideSubcategory.obj	—	—

---

← Back to Index