Documentation Verification Report

SmallRepresentatives

📁 Source: Mathlib/CategoryTheory/SmallRepresentatives.lean

Statistics

Metric	Count
Definitions `CoreSmallCategoryOfSet`, `arrowEquiv`, `equivalence`, `fullyFaithfulFunctor`, `functor`, `hom`, `homEquiv`, `obj`, `objEquiv`, `smallCategoryOfSet`, `SmallCategoryCardinalLT`, `categoryFamily`, `SmallCategoryOfSet`, `categoryFamily`, `comp`, `hom`, `id`, `instSmallCategoryElemObj`, `obj`	19
Theorems `functor_map`, `functor_obj`, `instIsEquivalenceElemObjSmallCategoryOfSetFunctor`, `smallCategoryOfSet_comp`, `smallCategoryOfSet_hom`, `smallCategoryOfSet_id`, `smallCategoryOfSet_obj`, `exists_equivalence`, `hasCardinalLT`, `assoc`, `comp_def`, `comp_id`, `exists_equivalence`, `id_comp`, `id_def`	15
Total	34

CategoryTheory

Definitions

Name	Category	Theorems
`CoreSmallCategoryOfSet` 📖	CompData	—
`SmallCategoryCardinalLT` 📖	CompOp	—
`SmallCategoryOfSet` 📖	CompData	3 math math: `ObjectProperty.instIsClosedUnderColimitsOfShapeColimitsCardinalClosureCategoryFamily`, `SmallCategoryCardinalLT.hasCardinalLT`, `SmallCategoryCardinalLT.exists_equivalence`

CategoryTheory.CoreSmallCategoryOfSet

Definitions

Name	Category	Theorems
`arrowEquiv` 📖	CompOp	—
`equivalence` 📖	CompOp	—
`fullyFaithfulFunctor` 📖	CompOp	—
`functor` 📖	CompOp	3 math math: `functor_obj`, `instIsEquivalenceElemObjSmallCategoryOfSetFunctor`, `functor_map`
`hom` 📖	CompOp	4 math math: `smallCategoryOfSet_id`, `smallCategoryOfSet_hom`, `functor_map`, `smallCategoryOfSet_comp`
`homEquiv` 📖	CompOp	3 math math: `smallCategoryOfSet_id`, `functor_map`, `smallCategoryOfSet_comp`
`obj` 📖	CompOp	5 math math: `functor_obj`, `smallCategoryOfSet_id`, `functor_map`, `smallCategoryOfSet_comp`, `smallCategoryOfSet_obj`
`objEquiv` 📖	CompOp	4 math math: `functor_obj`, `smallCategoryOfSet_id`, `functor_map`, `smallCategoryOfSet_comp`
`smallCategoryOfSet` 📖	CompOp	7 math math: `functor_obj`, `instIsEquivalenceElemObjSmallCategoryOfSetFunctor`, `smallCategoryOfSet_id`, `smallCategoryOfSet_hom`, `functor_map`, `smallCategoryOfSet_comp`, `smallCategoryOfSet_obj`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`functor_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `Set.Elem` `CategoryTheory.SmallCategoryOfSet.obj` `smallCategoryOfSet` `CategoryTheory.SmallCategoryOfSet.instSmallCategoryElemObj` `functor` `DFunLike.coe` `Equiv` `hom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `obj` `EquivLike.toFunLike` `Equiv.instEquivLike` `objEquiv` `homEquiv`	—	—
`functor_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Set.Elem` `CategoryTheory.SmallCategoryOfSet.obj` `smallCategoryOfSet` `CategoryTheory.SmallCategoryOfSet.instSmallCategoryElemObj` `functor` `DFunLike.coe` `Equiv` `obj` `EquivLike.toFunLike` `Equiv.instEquivLike` `objEquiv`	—	—
`instIsEquivalenceElemObjSmallCategoryOfSetFunctor` 📖	mathematical	—	`CategoryTheory.Functor.IsEquivalence` `Set.Elem` `CategoryTheory.SmallCategoryOfSet.obj` `smallCategoryOfSet` `CategoryTheory.SmallCategoryOfSet.instSmallCategoryElemObj` `functor`	—	`CategoryTheory.Functor.FullyFaithful.faithful` `CategoryTheory.Functor.FullyFaithful.full` `Equiv.surjective`
`smallCategoryOfSet_comp` 📖	mathematical	—	`CategoryTheory.SmallCategoryOfSet.comp` `smallCategoryOfSet` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Set.Elem` `obj` `EquivLike.toFunLike` `Equiv.instEquivLike` `objEquiv` `hom` `Equiv.symm` `homEquiv` `CategoryTheory.CategoryStruct.comp`	—	—
`smallCategoryOfSet_hom` 📖	mathematical	—	`CategoryTheory.SmallCategoryOfSet.hom` `smallCategoryOfSet` `hom`	—	—
`smallCategoryOfSet_id` 📖	mathematical	—	`CategoryTheory.SmallCategoryOfSet.id` `smallCategoryOfSet` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Set.Elem` `obj` `EquivLike.toFunLike` `Equiv.instEquivLike` `objEquiv` `hom` `Equiv.symm` `homEquiv` `CategoryTheory.CategoryStruct.id`	—	—
`smallCategoryOfSet_obj` 📖	mathematical	—	`CategoryTheory.SmallCategoryOfSet.obj` `smallCategoryOfSet` `obj`	—	—

CategoryTheory.SmallCategoryCardinalLT

Definitions

Name	Category	Theorems
`categoryFamily` 📖	CompOp	3 math math: `CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeColimitsCardinalClosureCategoryFamily`, `hasCardinalLT`, `exists_equivalence`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_equivalence` 📖	mathematical	`HasCardinalLT` `CategoryTheory.Arrow`	`CategoryTheory.Equivalence` `categoryFamily` `CategoryTheory.SmallCategoryOfSet.instSmallCategoryElemObj` `Ordinal.ToType` `Cardinal.ord` `CategoryTheory.SmallCategoryOfSet` `Set.Elem` `CategoryTheory.SmallCategoryOfSet.obj`	—	`Cardinal.lift_mk_le'` `Cardinal.mk_toType` `Cardinal.card_ord` `LT.lt.le` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `Function.Embedding.injective` `hasCardinalLT_iff_of_equiv`
`hasCardinalLT` 📖	mathematical	—	`HasCardinalLT` `CategoryTheory.Arrow` `categoryFamily` `CategoryTheory.SmallCategoryOfSet.instSmallCategoryElemObj` `Ordinal.ToType` `Cardinal.ord` `CategoryTheory.SmallCategoryOfSet` `Set.Elem` `CategoryTheory.SmallCategoryOfSet.obj`	—	—

CategoryTheory.SmallCategoryOfSet

Definitions

Name	Category	Theorems
`categoryFamily` 📖	CompOp	1 math math: `exists_equivalence`
`comp` 📖	CompOp	5 math math: `assoc`, `id_comp`, `comp_def`, `comp_id`, `CategoryTheory.CoreSmallCategoryOfSet.smallCategoryOfSet_comp`
`hom` 📖	CompOp	1 math math: `CategoryTheory.CoreSmallCategoryOfSet.smallCategoryOfSet_hom`
`id` 📖	CompOp	4 math math: `id_def`, `CategoryTheory.CoreSmallCategoryOfSet.smallCategoryOfSet_id`, `id_comp`, `comp_id`
`instSmallCategoryElemObj` 📖	CompOp	9 math math: `CategoryTheory.CoreSmallCategoryOfSet.functor_obj`, `CategoryTheory.CoreSmallCategoryOfSet.instIsEquivalenceElemObjSmallCategoryOfSetFunctor`, `id_def`, `CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeColimitsCardinalClosureCategoryFamily`, `CategoryTheory.SmallCategoryCardinalLT.hasCardinalLT`, `comp_def`, `CategoryTheory.CoreSmallCategoryOfSet.functor_map`, `CategoryTheory.SmallCategoryCardinalLT.exists_equivalence`, `exists_equivalence`
`obj` 📖	CompOp	9 math math: `CategoryTheory.CoreSmallCategoryOfSet.functor_obj`, `CategoryTheory.CoreSmallCategoryOfSet.instIsEquivalenceElemObjSmallCategoryOfSetFunctor`, `id_def`, `CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeColimitsCardinalClosureCategoryFamily`, `CategoryTheory.SmallCategoryCardinalLT.hasCardinalLT`, `comp_def`, `CategoryTheory.CoreSmallCategoryOfSet.functor_map`, `CategoryTheory.SmallCategoryCardinalLT.exists_equivalence`, `CategoryTheory.CoreSmallCategoryOfSet.smallCategoryOfSet_obj`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`assoc` 📖	mathematical	—	`comp`	—	—
`comp_def` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Set.Elem` `obj` `CategoryTheory.Category.toCategoryStruct` `instSmallCategoryElemObj` `comp`	—	—
`comp_id` 📖	mathematical	—	`comp` `id`	—	—
`exists_equivalence` 📖	mathematical	`Cardinal` `Cardinal.instLE` `Cardinal.lift` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	`CategoryTheory.Equivalence` `categoryFamily` `instSmallCategoryElemObj`	—	`Cardinal.lift_mk_le'` `Function.Embedding.injective`
`id_comp` 📖	mathematical	—	`comp` `id`	—	—
`id_def` 📖	mathematical	—	`CategoryTheory.CategoryStruct.id` `Set.Elem` `obj` `CategoryTheory.Category.toCategoryStruct` `instSmallCategoryElemObj` `id`	—	—

---

← Back to Index