Documentation Verification Report

Skeleton

📁 Source: Mathlib/CategoryTheory/Monoidal/Skeleton.lean

Statistics

Metric	Count
Definitions `monoidHom`, `mulEquiv`, `Skeleton`, `instBraidedCategory`, `instCommMonoid`, `instMonoid`, `instMonoidalCategory`, `monoidHom`, `mulEquiv`, `commMonoidOfSkeletalBraided`, `instLaxMonoidalSkeletonMapSkeleton`, `instMonoidalSkeletonFunctorSkeletonEquivalence`, `instMonoidalSkeletonInverseSkeletonEquivalence`, `instMonoidalSkeletonMapSkeleton`, `instOplaxMonoidalSkeletonMapSkeleton`, `monoidOfSkeletalMonoidal`, `Skeleton`	17
Theorems `mul_eq`, `one_eq`, `toSkeleton_tensorObj`	3
Total	20

CategoryTheory

Definitions

Name	Category	Theorems
`Skeleton` 📖	CompOp	45 math math: `Limits.hasColimitsOfShape_skeleton`, `Limits.hasLimitsOfSize_skeleton`, `instSmallUnitsSkeletonModuleCat`, `CommRing.Pic.mul_eq_tensor`, `Skeleton.toSkeleton_tensorObj`, `fromSkeleton.isEquivalence`, `skeletonEquivalence_unitIso`, `instInvertibleCarrierOutSemimoduleCatValSkeleton`, `essentiallySmall_iff`, `CommRing.Pic.inv_eq_dual`, `skeletonEquivalence_inverse`, `toSkeleton_eq_iff`, `CommRing.Pic.mk_eq_iff`, `CommRing.Pic.mk_eq_self`, `Skeleton.one_eq`, `CommRing.Pic.mapAlgebra_apply`, `CommRing.Pic.ext_iff`, `CommRing.Pic.instFreeAsModuleOfNat`, `Functor.mapSkeleton_obj_toSkeleton`, `Functor.instFaithfulSkeletonMapSkeleton`, `toSkeleton_fromSkeleton_obj`, `instEssSurjSkeletonFromSkeleton`, `skeleton_skeletal`, `skeletonEquivalence_counitIso`, `fromSkeleton_obj`, `small_skeleton_of_essentiallySmall`, `Limits.hasLimitsOfShape_skeleton`, `fromSkeleton_map`, `instFaithfulSkeletonFromSkeleton`, `instFullSkeletonFromSkeleton`, `Functor.instFullSkeletonMapSkeleton`, `Skeleton.comp_hom`, `toSkeletonFunctor_map_hom`, `Functor.instEssSurjSkeletonMapSkeleton`, `toSkeletonFunctor_obj`, `skeleton_isSkeleton`, `Skeleton.mul_eq`, `skeletonEquivalence_functor`, `Functor.mapSkeleton_injective`, `instInvertibleCarrierOutModuleCatValSkeleton`, `Limits.hasColimitsOfSize_skeleton`, `Functor.mapSkeleton_surjective`, `Skeleton.comp_hom_assoc`, `instSmallUnitsSkeletonSemimoduleCat`, `essentiallySmall_iff_of_thin`
`commMonoidOfSkeletalBraided` 📖	CompOp	—
`instLaxMonoidalSkeletonMapSkeleton` 📖	CompOp	—
`instMonoidalSkeletonFunctorSkeletonEquivalence` 📖	CompOp	—
`instMonoidalSkeletonInverseSkeletonEquivalence` 📖	CompOp	—
`instMonoidalSkeletonMapSkeleton` 📖	CompOp	—
`instOplaxMonoidalSkeletonMapSkeleton` 📖	CompOp	—
`monoidOfSkeletalMonoidal` 📖	CompOp	—

CategoryTheory.Skeletal

Definitions

Name	Category	Theorems
`monoidHom` 📖	CompOp	—
`mulEquiv` 📖	CompOp	—

CategoryTheory.Skeleton

Definitions

Name	Category	Theorems
`instBraidedCategory` 📖	CompOp	—
`instCommMonoid` 📖	CompOp	—
`instMonoid` 📖	CompOp	14 math math: `instSmallUnitsSkeletonModuleCat`, `CommRing.Pic.mul_eq_tensor`, `toSkeleton_tensorObj`, `instInvertibleCarrierOutSemimoduleCatValSkeleton`, `CommRing.Pic.inv_eq_dual`, `CommRing.Pic.mk_eq_iff`, `CommRing.Pic.mk_eq_self`, `one_eq`, `CommRing.Pic.mapAlgebra_apply`, `CommRing.Pic.ext_iff`, `CommRing.Pic.instFreeAsModuleOfNat`, `mul_eq`, `instInvertibleCarrierOutModuleCatValSkeleton`, `instSmallUnitsSkeletonSemimoduleCat`
`instMonoidalCategory` 📖	CompOp	—
`monoidHom` 📖	CompOp	—
`mulEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mul_eq` 📖	mathematical	—	`CategoryTheory.Skeleton` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid` `CategoryTheory.toSkeleton` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `Quotient.out` `CategoryTheory.isIsomorphicSetoid`	—	—
`one_eq` 📖	mathematical	—	`CategoryTheory.Skeleton` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid` `CategoryTheory.toSkeleton` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct`	—	—
`toSkeleton_tensorObj` 📖	mathematical	—	`CategoryTheory.toSkeleton` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Skeleton` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid`	—	—

FintypeCat

Definitions

Name	Category	Theorems
`Skeleton` 📖	CompOp	7 math math: `Skeleton.instIsEquivalenceIncl`, `isSkeleton`, `Skeleton.is_skeletal`, `Skeleton.instEssSurjIncl`, `Skeleton.instFullIncl`, `Skeleton.incl_mk_nat_card`, `Skeleton.instFaithfulIncl`

---

← Back to Index