Documentation Verification Report

Enrichment

📁 Source: Mathlib/CategoryTheory/Monoidal/Closed/Enrichment.lean

Statistics

Metric	Count
Definitions `enrichedCategorySelf`, `enrichedOrdinaryCategorySelf`	2
Theorems `enrichedCategorySelf_comp`, `enrichedCategorySelf_hom`, `enrichedCategorySelf_id`, `enrichedOrdinaryCategorySelf_eHomWhiskerLeft`, `enrichedOrdinaryCategorySelf_eHomWhiskerRight`, `enrichedOrdinaryCategorySelf_homEquiv`, `enrichedOrdinaryCategorySelf_homEquiv_symm`	7
Total	9

CategoryTheory.MonoidalClosed

Definitions

Name	Category	Theorems
`enrichedCategorySelf` 📖	CompOp	3 math math: `enrichedCategorySelf_comp`, `enrichedCategorySelf_id`, `enrichedCategorySelf_hom`
`enrichedOrdinaryCategorySelf` 📖	CompOp	8 math math: `enrichedOrdinaryCategorySelf_homEquiv_symm`, `enrichedOrdinaryCategorySelf_eHomWhiskerRight`, `CategoryTheory.Presheaf.functorEnrichedHomCoyonedaObjEquiv_naturality`, `enrichedOrdinaryCategorySelf_homEquiv`, `CategoryTheory.Presheaf.isSheaf_functorEnrichedHom`, `FunctorCategory.homEquiv_naturality_two_symm`, `enrichedOrdinaryCategorySelf_eHomWhiskerLeft`, `FunctorCategory.homEquiv_naturality_three`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`enrichedCategorySelf_comp` 📖	mathematical	—	`CategoryTheory.eComp` `enrichedCategorySelf` `comp` `closed`	—	—
`enrichedCategorySelf_hom` 📖	mathematical	—	`CategoryTheory.EnrichedCategory.Hom` `enrichedCategorySelf` `CategoryTheory.Functor.obj` `CategoryTheory.ihom` `closed`	—	—
`enrichedCategorySelf_id` 📖	mathematical	—	`CategoryTheory.eId` `enrichedCategorySelf` `id` `closed`	—	—
`enrichedOrdinaryCategorySelf_eHomWhiskerLeft` 📖	mathematical	—	`CategoryTheory.eHomWhiskerLeft` `enrichedOrdinaryCategorySelf` `CategoryTheory.Functor.map` `CategoryTheory.ihom` `closed`	—	`whiskerLeft_curry'_comp` `CategoryTheory.Iso.inv_hom_id_assoc`
`enrichedOrdinaryCategorySelf_eHomWhiskerRight` 📖	mathematical	—	`CategoryTheory.eHomWhiskerRight` `enrichedOrdinaryCategorySelf` `CategoryTheory.NatTrans.app` `CategoryTheory.ihom` `closed` `pre`	—	`curry'_whiskerRight_comp` `CategoryTheory.Iso.inv_hom_id_assoc`
`enrichedOrdinaryCategorySelf_homEquiv` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.EnrichedCategory.Hom` `CategoryTheory.EnrichedOrdinaryCategory.toEnrichedCategory` `enrichedOrdinaryCategorySelf` `EquivLike.toFunLike` `Equiv.instEquivLike` `CategoryTheory.eHomEquiv` `curry'` `closed`	—	—
`enrichedOrdinaryCategorySelf_homEquiv_symm` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.EnrichedCategory.Hom` `CategoryTheory.EnrichedOrdinaryCategory.toEnrichedCategory` `enrichedOrdinaryCategorySelf` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `CategoryTheory.eHomEquiv` `uncurry'` `closed`	—	—

---

← Back to Index