Documentation Verification Report

CommaMap

📁 Source: Mathlib/CategoryTheory/Comma/StructuredArrow/CommaMap.lean

Statistics

Metric	Count
Definitions `commaMapEquivalence`, `commaMapEquivalenceCounitIso`, `commaMapEquivalenceFunctor`, `commaMapEquivalenceInverse`, `commaMapEquivalenceUnitIso`	5
Theorems `commaMapEquivalenceCounitIso_hom_app_left_right`, `commaMapEquivalenceCounitIso_hom_app_right_right`, `commaMapEquivalenceCounitIso_inv_app_left_right`, `commaMapEquivalenceCounitIso_inv_app_right_right`, `commaMapEquivalenceFunctor_map_left`, `commaMapEquivalenceFunctor_map_right`, `commaMapEquivalenceFunctor_obj_hom`, `commaMapEquivalenceFunctor_obj_left`, `commaMapEquivalenceFunctor_obj_right`, `commaMapEquivalenceInverse_map`, `commaMapEquivalenceInverse_obj`, `commaMapEquivalenceUnitIso_hom_app_right_left`, `commaMapEquivalenceUnitIso_hom_app_right_right`, `commaMapEquivalenceUnitIso_inv_app_right_left`, `commaMapEquivalenceUnitIso_inv_app_right_right`	15
Total	20

CategoryTheory.StructuredArrow

Definitions

Name	Category	Theorems
`commaMapEquivalence` 📖	CompOp	—
`commaMapEquivalenceCounitIso` 📖	CompOp	4 math math: `commaMapEquivalenceCounitIso_hom_app_left_right`, `commaMapEquivalenceCounitIso_hom_app_right_right`, `commaMapEquivalenceCounitIso_inv_app_left_right`, `commaMapEquivalenceCounitIso_inv_app_right_right`
`commaMapEquivalenceFunctor` 📖	CompOp	13 math math: `commaMapEquivalenceCounitIso_hom_app_left_right`, `commaMapEquivalenceUnitIso_inv_app_right_right`, `commaMapEquivalenceFunctor_obj_left`, `commaMapEquivalenceFunctor_map_left`, `commaMapEquivalenceFunctor_map_right`, `commaMapEquivalenceCounitIso_hom_app_right_right`, `commaMapEquivalenceUnitIso_hom_app_right_right`, `commaMapEquivalenceUnitIso_hom_app_right_left`, `commaMapEquivalenceUnitIso_inv_app_right_left`, `commaMapEquivalenceCounitIso_inv_app_left_right`, `commaMapEquivalenceFunctor_obj_right`, `commaMapEquivalenceCounitIso_inv_app_right_right`, `commaMapEquivalenceFunctor_obj_hom`
`commaMapEquivalenceInverse` 📖	CompOp	10 math math: `commaMapEquivalenceInverse_map`, `commaMapEquivalenceCounitIso_hom_app_left_right`, `commaMapEquivalenceUnitIso_inv_app_right_right`, `commaMapEquivalenceInverse_obj`, `commaMapEquivalenceCounitIso_hom_app_right_right`, `commaMapEquivalenceUnitIso_hom_app_right_right`, `commaMapEquivalenceUnitIso_hom_app_right_left`, `commaMapEquivalenceUnitIso_inv_app_right_left`, `commaMapEquivalenceCounitIso_inv_app_left_right`, `commaMapEquivalenceCounitIso_inv_app_right_right`
`commaMapEquivalenceUnitIso` 📖	CompOp	4 math math: `commaMapEquivalenceUnitIso_inv_app_right_right`, `commaMapEquivalenceUnitIso_hom_app_right_right`, `commaMapEquivalenceUnitIso_hom_app_right_left`, `commaMapEquivalenceUnitIso_inv_app_right_left`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commaMapEquivalenceCounitIso_hom_app_left_right` 📖	mathematical	—	`CategoryTheory.CommaMorphism.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Comma.left` `CategoryTheory.StructuredArrow` `CategoryTheory.instCategoryStructuredArrow` `CategoryTheory.Comma.right` `CategoryTheory.Functor.obj` `map₂` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.hom` `CategoryTheory.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.Comma` `CategoryTheory.commaCategory` `CategoryTheory.Comma.map` `commaMapEquivalenceInverse` `commaMapEquivalenceFunctor` `CategoryTheory.Functor.id` `CategoryTheory.CommaMorphism.left` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `commaMapEquivalenceCounitIso`	—	—
`commaMapEquivalenceCounitIso_hom_app_right_right` 📖	mathematical	—	`CategoryTheory.CommaMorphism.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Comma.right` `CategoryTheory.StructuredArrow` `CategoryTheory.Comma.left` `CategoryTheory.instCategoryStructuredArrow` `CategoryTheory.Functor.obj` `map₂` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.hom` `CategoryTheory.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.Comma` `CategoryTheory.commaCategory` `CategoryTheory.Comma.map` `commaMapEquivalenceInverse` `commaMapEquivalenceFunctor` `CategoryTheory.Functor.id` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `commaMapEquivalenceCounitIso`	—	—
`commaMapEquivalenceCounitIso_inv_app_left_right` 📖	mathematical	—	`CategoryTheory.CommaMorphism.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Comma.left` `CategoryTheory.StructuredArrow` `CategoryTheory.instCategoryStructuredArrow` `CategoryTheory.Comma.right` `CategoryTheory.Functor.obj` `map₂` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.hom` `CategoryTheory.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.Comma` `CategoryTheory.commaCategory` `CategoryTheory.Functor.id` `CategoryTheory.Comma.map` `commaMapEquivalenceInverse` `commaMapEquivalenceFunctor` `CategoryTheory.CommaMorphism.left` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.inv` `commaMapEquivalenceCounitIso`	—	—
`commaMapEquivalenceCounitIso_inv_app_right_right` 📖	mathematical	—	`CategoryTheory.CommaMorphism.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Comma.right` `CategoryTheory.StructuredArrow` `CategoryTheory.Comma.left` `CategoryTheory.instCategoryStructuredArrow` `CategoryTheory.Functor.obj` `map₂` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.hom` `CategoryTheory.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.Comma` `CategoryTheory.commaCategory` `CategoryTheory.Functor.id` `CategoryTheory.Comma.map` `commaMapEquivalenceInverse` `commaMapEquivalenceFunctor` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.inv` `commaMapEquivalenceCounitIso`	—	—
`commaMapEquivalenceFunctor_map_left` 📖	mathematical	—	`CategoryTheory.CommaMorphism.left` `CategoryTheory.StructuredArrow` `CategoryTheory.Comma.left` `CategoryTheory.instCategoryStructuredArrow` `CategoryTheory.Comma.right` `CategoryTheory.Functor.obj` `map₂` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.hom` `CategoryTheory.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Comma` `CategoryTheory.commaCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Comma.map` `CategoryTheory.CommaMorphism.right` `homMk` `CategoryTheory.Functor.map` `commaMapEquivalenceFunctor`	—	—
`commaMapEquivalenceFunctor_map_right` 📖	mathematical	—	`CategoryTheory.CommaMorphism.right` `CategoryTheory.StructuredArrow` `CategoryTheory.Comma.left` `CategoryTheory.instCategoryStructuredArrow` `CategoryTheory.Comma.right` `CategoryTheory.Functor.obj` `map₂` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.hom` `CategoryTheory.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Comma` `CategoryTheory.commaCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Comma.map` `CategoryTheory.CommaMorphism.left` `homMk` `CategoryTheory.Functor.map` `commaMapEquivalenceFunctor`	—	—
`commaMapEquivalenceFunctor_obj_hom` 📖	mathematical	—	`CategoryTheory.Comma.hom` `CategoryTheory.StructuredArrow` `CategoryTheory.Comma.left` `CategoryTheory.instCategoryStructuredArrow` `CategoryTheory.Comma.right` `CategoryTheory.Functor.obj` `map₂` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.Comma` `CategoryTheory.commaCategory` `CategoryTheory.Comma.map` `commaMapEquivalenceFunctor` `homMk` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.CommaMorphism.left` `CategoryTheory.CommaMorphism.right`	—	—
`commaMapEquivalenceFunctor_obj_left` 📖	mathematical	—	`CategoryTheory.Comma.left` `CategoryTheory.StructuredArrow` `CategoryTheory.instCategoryStructuredArrow` `CategoryTheory.Comma.right` `CategoryTheory.Functor.obj` `map₂` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.hom` `CategoryTheory.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.Comma` `CategoryTheory.commaCategory` `CategoryTheory.Comma.map` `commaMapEquivalenceFunctor` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.CommaMorphism.left`	—	—
`commaMapEquivalenceFunctor_obj_right` 📖	mathematical	—	`CategoryTheory.Comma.right` `CategoryTheory.StructuredArrow` `CategoryTheory.Comma.left` `CategoryTheory.instCategoryStructuredArrow` `CategoryTheory.Functor.obj` `map₂` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.hom` `CategoryTheory.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.Comma` `CategoryTheory.commaCategory` `CategoryTheory.Comma.map` `commaMapEquivalenceFunctor` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.CommaMorphism.right`	—	—
`commaMapEquivalenceInverse_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.Comma` `CategoryTheory.StructuredArrow` `CategoryTheory.Comma.left` `CategoryTheory.instCategoryStructuredArrow` `CategoryTheory.Comma.right` `CategoryTheory.Functor.obj` `map₂` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.hom` `CategoryTheory.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.commaCategory` `CategoryTheory.Comma.map` `commaMapEquivalenceInverse` `homMk` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.CommaMorphism.right` `CategoryTheory.CommaMorphism.left`	—	—
`commaMapEquivalenceInverse_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.Comma` `CategoryTheory.StructuredArrow` `CategoryTheory.Comma.left` `CategoryTheory.instCategoryStructuredArrow` `CategoryTheory.Comma.right` `map₂` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.hom` `CategoryTheory.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.commaCategory` `CategoryTheory.Comma.map` `commaMapEquivalenceInverse` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.CommaMorphism.right`	—	—
`commaMapEquivalenceUnitIso_hom_app_right_left` 📖	mathematical	—	`CategoryTheory.CommaMorphism.left` `CategoryTheory.Comma.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Comma` `CategoryTheory.commaCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Comma.map` `CategoryTheory.Functor.obj` `CategoryTheory.StructuredArrow` `CategoryTheory.instCategoryStructuredArrow` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Comma.left` `map₂` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.hom` `CategoryTheory.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `commaMapEquivalenceFunctor` `commaMapEquivalenceInverse` `CategoryTheory.CommaMorphism.right` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `commaMapEquivalenceUnitIso`	—	—
`commaMapEquivalenceUnitIso_hom_app_right_right` 📖	mathematical	—	`CategoryTheory.CommaMorphism.right` `CategoryTheory.Comma.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Comma` `CategoryTheory.commaCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Comma.map` `CategoryTheory.Functor.obj` `CategoryTheory.StructuredArrow` `CategoryTheory.instCategoryStructuredArrow` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Comma.left` `map₂` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.hom` `CategoryTheory.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `commaMapEquivalenceFunctor` `commaMapEquivalenceInverse` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `commaMapEquivalenceUnitIso`	—	—
`commaMapEquivalenceUnitIso_inv_app_right_left` 📖	mathematical	—	`CategoryTheory.CommaMorphism.left` `CategoryTheory.Comma.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Comma` `CategoryTheory.commaCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Comma.map` `CategoryTheory.Functor.obj` `CategoryTheory.StructuredArrow` `CategoryTheory.instCategoryStructuredArrow` `CategoryTheory.Functor.comp` `CategoryTheory.Comma.left` `map₂` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.hom` `CategoryTheory.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `commaMapEquivalenceFunctor` `commaMapEquivalenceInverse` `CategoryTheory.Functor.id` `CategoryTheory.CommaMorphism.right` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.inv` `commaMapEquivalenceUnitIso`	—	—
`commaMapEquivalenceUnitIso_inv_app_right_right` 📖	mathematical	—	`CategoryTheory.CommaMorphism.right` `CategoryTheory.Comma.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Comma` `CategoryTheory.commaCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Comma.map` `CategoryTheory.Functor.obj` `CategoryTheory.StructuredArrow` `CategoryTheory.instCategoryStructuredArrow` `CategoryTheory.Functor.comp` `CategoryTheory.Comma.left` `map₂` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.hom` `CategoryTheory.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `commaMapEquivalenceFunctor` `commaMapEquivalenceInverse` `CategoryTheory.Functor.id` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.inv` `commaMapEquivalenceUnitIso`	—	—

---

← Back to Index