Documentation Verification Report

FunctorHom

📁 Source: Mathlib/CategoryTheory/Functor/FunctorHom.lean

Statistics

Metric	Count
Definitions `instEnrichedCategoryFunctorType`, `HomObj`, `app`, `comp`, `id`, `map`, `ofNatTrans`, `functorHom`, `functorHomEquiv`, `homObjEquiv`, `homObjFunctor`, `natTransEquiv`	12
Theorems `associator_hom_apply`, `associator_inv_apply`, `functorHom_whiskerLeft_natTransEquiv_symm_app`, `natTransEquiv_symm_app_app_apply`, `natTransEquiv_symm_whiskerRight_functorHom_app`, `whiskerLeft_app_apply`, `whiskerRight_app_apply`, `comp_app`, `congr_app`, `ext`, `ext_iff`, `id_app`, `map_app`, `naturality`, `naturality_assoc`, `ofNatTrans_app`, `functorHomEquiv_apply_app`, `functorHomEquiv_symm_apply_app_app`, `functorHom_ext`, `functorHom_ext_iff`, `homObjEquiv_apply_app`, `homObjEquiv_symm_apply_app`, `homObjFunctor_map_app`, `homObjFunctor_obj`, `natTransEquiv_apply_app`, `natTransEquiv_symm_apply_app`	26
Total	38

CategoryTheory.Enriched.Functor

Definitions

Name	Category	Theorems
`instEnrichedCategoryFunctorType` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`associator_hom_apply` 📖	mathematical	—	`CategoryTheory.Iso.hom` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.functorHom` `CategoryTheory.MonoidalCategoryStruct.associator` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct`	—	—
`associator_inv_apply` 📖	mathematical	—	`CategoryTheory.Iso.inv` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.functorHom` `CategoryTheory.MonoidalCategoryStruct.associator` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct`	—	—
`functorHom_whiskerLeft_natTransEquiv_symm_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `CategoryTheory.Functor.functorHom` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `CategoryTheory.Functor.natTransEquiv` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.HomObj` `Opposite.unop` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.rightOp` `CategoryTheory.coyoneda` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Functor.HomObj.ofNatTrans`	—	—
`natTransEquiv_symm_app_app_apply` 📖	mathematical	—	`CategoryTheory.Functor.HomObj.app` `Opposite.unop` `CategoryTheory.Functor` `CategoryTheory.types` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Functor.rightOp` `CategoryTheory.coyoneda` `CategoryTheory.NatTrans.app` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `CategoryTheory.Functor.functorHom` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `CategoryTheory.Functor.natTransEquiv`	—	—
`natTransEquiv_symm_whiskerRight_functorHom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Functor.functorHom` `CategoryTheory.MonoidalCategoryStruct.whiskerRight` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `CategoryTheory.Functor.natTransEquiv` `CategoryTheory.Functor.HomObj` `Opposite.unop` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.rightOp` `CategoryTheory.coyoneda` `CategoryTheory.Functor.HomObj.ofNatTrans` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct`	—	—
`whiskerLeft_app_apply` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `CategoryTheory.Functor.functorHom` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `CategoryTheory.Functor.obj`	—	—
`whiskerRight_app_apply` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `CategoryTheory.Functor.functorHom` `CategoryTheory.MonoidalCategoryStruct.whiskerRight` `CategoryTheory.Functor.obj`	—	—

CategoryTheory.Functor

Definitions

Name	Category	Theorems
`HomObj` 📖	CompData	8 math math: `functorHomEquiv_apply_app`, `homObjEquiv_apply_app`, `homObjEquiv_symm_apply_app`, `CategoryTheory.Enriched.Functor.functorHom_whiskerLeft_natTransEquiv_symm_app`, `CategoryTheory.Enriched.Functor.natTransEquiv_symm_whiskerRight_functorHom_app`, `CategoryTheory.FunctorToTypes.rightAdj_obj_obj`, `homObjFunctor_obj`, `functorHomEquiv_symm_apply_app_app`
`functorHom` 📖	CompOp	14 math math: `functorHomEquiv_apply_app`, `CategoryTheory.Enriched.Functor.associator_inv_apply`, `natTransEquiv_apply_app`, `CategoryTheory.FunctorToTypes.functorHomEquiv_symm_apply_app_app`, `CategoryTheory.Enriched.Functor.whiskerLeft_app_apply`, `natTransEquiv_symm_apply_app`, `CategoryTheory.Enriched.Functor.associator_hom_apply`, `CategoryTheory.FunctorToTypes.rightAdj_map_app_app`, `CategoryTheory.Enriched.Functor.whiskerRight_app_apply`, `CategoryTheory.Enriched.Functor.functorHom_whiskerLeft_natTransEquiv_symm_app`, `CategoryTheory.Enriched.Functor.natTransEquiv_symm_app_app_apply`, `CategoryTheory.FunctorToTypes.functorHomEquiv_apply_app`, `CategoryTheory.Enriched.Functor.natTransEquiv_symm_whiskerRight_functorHom_app`, `functorHomEquiv_symm_apply_app_app`
`functorHomEquiv` 📖	CompOp	2 math math: `functorHomEquiv_apply_app`, `functorHomEquiv_symm_apply_app_app`
`homObjEquiv` 📖	CompOp	2 math math: `homObjEquiv_apply_app`, `homObjEquiv_symm_apply_app`
`homObjFunctor` 📖	CompOp	2 math math: `homObjFunctor_map_app`, `homObjFunctor_obj`
`natTransEquiv` 📖	CompOp	5 math math: `natTransEquiv_apply_app`, `natTransEquiv_symm_apply_app`, `CategoryTheory.Enriched.Functor.functorHom_whiskerLeft_natTransEquiv_symm_app`, `CategoryTheory.Enriched.Functor.natTransEquiv_symm_app_app_apply`, `CategoryTheory.Enriched.Functor.natTransEquiv_symm_whiskerRight_functorHom_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`functorHomEquiv_apply_app` 📖	mathematical	—	`HomObj.app` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.Functor` `CategoryTheory.types` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `category` `functorHom` `HomObj` `EquivLike.toFunLike` `Equiv.instEquivLike` `functorHomEquiv` `Opposite.unop` `obj` `Opposite` `CategoryTheory.Category.opposite` `rightOp` `CategoryTheory.coyoneda` `CategoryTheory.NatTrans.app` `CategoryTheory.CategoryStruct.id` `Opposite.op`	—	—
`functorHomEquiv_symm_apply_app_app` 📖	mathematical	—	`HomObj.app` `Opposite.unop` `CategoryTheory.Functor` `CategoryTheory.types` `obj` `Opposite` `CategoryTheory.Category.opposite` `category` `rightOp` `CategoryTheory.coyoneda` `CategoryTheory.NatTrans.app` `functorHom` `DFunLike.coe` `Equiv` `HomObj` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `functorHomEquiv` `map` `Opposite.op`	—	—
`functorHom_ext` 📖	—	`HomObj.app` `Opposite.unop` `CategoryTheory.Functor` `CategoryTheory.types` `obj` `Opposite` `CategoryTheory.Category.opposite` `category` `rightOp` `CategoryTheory.coyoneda`	—	—	`HomObj.ext`
`functorHom_ext_iff` 📖	mathematical	—	`HomObj.app` `Opposite.unop` `CategoryTheory.Functor` `CategoryTheory.types` `obj` `Opposite` `CategoryTheory.Category.opposite` `category` `rightOp` `CategoryTheory.coyoneda`	—	`functorHom_ext`
`homObjEquiv_apply_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Functor` `category` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `DFunLike.coe` `Equiv` `HomObj` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `EquivLike.toFunLike` `Equiv.instEquivLike` `homObjEquiv` `obj` `HomObj.app`	—	—
`homObjEquiv_symm_apply_app` 📖	mathematical	—	`HomObj.app` `CategoryTheory.types` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.Functor` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `category` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `HomObj` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `homObjEquiv` `CategoryTheory.NatTrans.app` `obj`	—	—
`homObjFunctor_map_app` 📖	mathematical	—	`HomObj.app` `Opposite.unop` `CategoryTheory.Functor` `CategoryTheory.types` `map` `Opposite` `CategoryTheory.Category.opposite` `category` `homObjFunctor` `CategoryTheory.NatTrans.app` `Quiver.Hom.unop` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	—	—
`homObjFunctor_obj` 📖	mathematical	—	`obj` `Opposite` `CategoryTheory.Functor` `CategoryTheory.types` `CategoryTheory.Category.opposite` `category` `homObjFunctor` `HomObj` `Opposite.unop`	—	—
`natTransEquiv_apply_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.Functor` `CategoryTheory.types` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `category` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `functorHom` `EquivLike.toFunLike` `Equiv.instEquivLike` `natTransEquiv` `HomObj.app` `Opposite.unop` `obj` `Opposite` `CategoryTheory.Category.opposite` `rightOp` `CategoryTheory.coyoneda` `CategoryTheory.CategoryStruct.id` `Opposite.op`	—	—
`natTransEquiv_symm_apply_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Functor` `category` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `functorHom` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `natTransEquiv` `HomObj.ofNatTrans` `Opposite.unop` `obj` `Opposite` `CategoryTheory.Category.opposite` `rightOp` `CategoryTheory.coyoneda`	—	—

CategoryTheory.Functor.HomObj

Definitions

Name	Category	Theorems
`app` 📖	CompOp	21 math math: `CategoryTheory.Functor.functorHomEquiv_apply_app`, `CategoryTheory.Functor.natTransEquiv_apply_app`, `CategoryTheory.Functor.homObjEquiv_apply_app`, `comp_app`, `CategoryTheory.FunctorToTypes.functorHomEquiv_symm_apply_app_app`, `CategoryTheory.Functor.homObjEquiv_symm_apply_app`, `CategoryTheory.FunctorToTypes.rightAdj_map_app`, `CategoryTheory.Functor.homObjFunctor_map_app`, `CategoryTheory.FunctorToTypes.rightAdj_map_app_app`, `CategoryTheory.Functor.functorHom_ext_iff`, `CategoryTheory.Enriched.Functor.natTransEquiv_symm_app_app_apply`, `map_app`, `CategoryTheory.FunctorToTypes.functorHomEquiv_apply_app`, `CategoryTheory.FunctorToTypes.rightAdj_obj_map_app`, `ofNatTrans_app`, `naturality_assoc`, `ext_iff`, `congr_app`, `naturality`, `id_app`, `CategoryTheory.Functor.functorHomEquiv_symm_apply_app_app`
`comp` 📖	CompOp	1 math math: `comp_app`
`id` 📖	CompOp	1 math math: `id_app`
`map` 📖	CompOp	1 math math: `map_app`
`ofNatTrans` 📖	CompOp	4 math math: `CategoryTheory.Functor.natTransEquiv_symm_apply_app`, `CategoryTheory.Enriched.Functor.functorHom_whiskerLeft_natTransEquiv_symm_app`, `CategoryTheory.Enriched.Functor.natTransEquiv_symm_whiskerRight_functorHom_app`, `ofNatTrans_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_app` 📖	mathematical	—	`app` `comp` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj`	—	—
`congr_app` 📖	mathematical	—	`app`	—	—
`ext` 📖	—	`app`	—	—	—
`ext_iff` 📖	mathematical	—	`app`	—	`ext`
`id_app` 📖	mathematical	—	`app` `id` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj`	—	—
`map_app` 📖	mathematical	—	`app` `map` `CategoryTheory.NatTrans.app` `CategoryTheory.types`	—	—
`naturality` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `app` `CategoryTheory.types`	—	—
`naturality_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `app` `CategoryTheory.types`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `naturality`
`ofNatTrans_app` 📖	mathematical	—	`app` `ofNatTrans` `CategoryTheory.NatTrans.app`	—	—

---

← Back to Index