Documentation Verification Report

Pointed

📁 Source: Mathlib/CategoryTheory/Category/Pointed.lean

Statistics

Metric	Count
Definitions `comp`, `id`, `instInhabited`, `toFun`, `mk`, `X`, `hasForget`, `instCoeSortType`, `instFunLikeSubtypeForallXEqPoint`, `instInhabited`, `largeCategory`, `of`, `point`, `typeToPointed`, `typeToPointedForgetAdjunction`	15
Theorems `comp_toFun`, `comp_toFun'`, `ext`, `ext_iff`, `id_toFun`, `id_toFun'`, `map_point`, `mk_hom_toFun`, `mk_inv_toFun`, `coe_of`, `typeToPointed_map_toFun`, `typeToPointed_obj_X`, `typeToPointed_obj_point`	13
Total	28

Pointed

Definitions

Name	Category	Theorems
`X` 📖	CompOp	23 math math: `partialFunToPointed_map`, `pointedToTwoPFst_obj_toTwoPointing_toProd`, `partialFunEquivPointed_counitIso_inv_app_toFun`, `Hom.id_toFun'`, `pointedToPartialFun_map`, `Hom.comp_toFun`, `Hom.comp_toFun'`, `pointedToTwoPFst_obj_X`, `pointedToPartialFun_obj`, `pointedToTwoPFst_map_hom_toFun`, `Hom.id_toFun`, `pointedToTwoPSnd_obj_X`, `partialFunEquivPointed_inverse_obj`, `partialFunEquivPointed_functor_obj_X`, `bipointedToPointedSnd_comp_forget`, `partialFunEquivPointed_inverse_map_Dom`, `pointedToTwoPSnd_map_hom_toFun`, `partialFunEquivPointed_counitIso_hom_app_toFun`, `partialFunEquivPointed_inverse_map_get_coe`, `coe_of`, `typeToPointed_obj_X`, `pointedToTwoPSnd_obj_toTwoPointing_toProd`, `bipointedToPointedFst_comp_forget`
`hasForget` 📖	CompOp	2 math math: `bipointedToPointedSnd_comp_forget`, `bipointedToPointedFst_comp_forget`
`instCoeSortType` 📖	CompOp	—
`instFunLikeSubtypeForallXEqPoint` 📖	CompOp	2 math math: `bipointedToPointedSnd_comp_forget`, `bipointedToPointedFst_comp_forget`
`instInhabited` 📖	CompOp	—
`largeCategory` 📖	CompOp	43 math math: `partialFunToPointed_map`, `pointedToTwoPFst_obj_toTwoPointing_toProd`, `typeToPartialFunIsoPartialFunToPointed_inv_app_toFun`, `partialFunEquivPointed_counitIso_inv_app_toFun`, `pointedToBipointedFst_comp_swap`, `partialFunEquivPointed_unitIso_hom_app`, `Hom.id_toFun'`, `pointedToPartialFun_map`, `partialFunEquivPointed_unitIso_inv_app`, `swap_comp_bipointedToPointedFst`, `pointedToTwoPFst_comp_swap`, `typeToPointed_map_toFun`, `typeToPartialFunIsoPartialFunToPointed_hom_app_toFun`, `partialFunEquivPointed_functor_map_toFun`, `Hom.comp_toFun'`, `pointedToTwoPFst_obj_X`, `pointedToPartialFun_obj`, `pointedToTwoPFst_map_hom_toFun`, `pointedToTwoPFst_comp_forget_to_bipointed`, `pointedToBipointedCompBipointedToPointedSnd_hom_app_toFun`, `pointedToTwoPSnd_obj_X`, `partialFunEquivPointed_inverse_obj`, `pointedToBipointedCompBipointedToPointedSnd_inv_app_toFun`, `partialFunEquivPointed_functor_obj_X`, `pointedToBipointedCompBipointedToPointedFst_inv_app_toFun`, `pointedToBipointedCompBipointedToPointedFst_hom_app_toFun`, `Iso.mk_inv_toFun`, `bipointedToPointedSnd_comp_forget`, `partialFunToPointed_obj`, `swap_comp_bipointedToPointedSnd`, `pointedToTwoPSnd_comp_swap`, `partialFunEquivPointed_inverse_map_Dom`, `pointedToTwoPSnd_map_hom_toFun`, `partialFunEquivPointed_counitIso_hom_app_toFun`, `partialFunEquivPointed_inverse_map_get_coe`, `typeToPointed_obj_X`, `pointedToTwoPSnd_obj_toTwoPointing_toProd`, `partialFunEquivPointed_functor_obj_point`, `typeToPointed_obj_point`, `Iso.mk_hom_toFun`, `pointedToTwoPSnd_comp_forget_to_bipointed`, `pointedToBipointedSnd_comp_swap`, `bipointedToPointedFst_comp_forget`
`of` 📖	CompOp	1 math math: `coe_of`
`point` 📖	CompOp	16 math math: `pointedToTwoPFst_obj_toTwoPointing_toProd`, `partialFunEquivPointed_counitIso_inv_app_toFun`, `pointedToPartialFun_map`, `Hom.map_point`, `pointedToPartialFun_obj`, `pointedToTwoPFst_map_hom_toFun`, `partialFunEquivPointed_inverse_obj`, `bipointedToPointedSnd_comp_forget`, `partialFunEquivPointed_inverse_map_Dom`, `pointedToTwoPSnd_map_hom_toFun`, `partialFunEquivPointed_counitIso_hom_app_toFun`, `partialFunEquivPointed_inverse_map_get_coe`, `pointedToTwoPSnd_obj_toTwoPointing_toProd`, `partialFunEquivPointed_functor_obj_point`, `typeToPointed_obj_point`, `bipointedToPointedFst_comp_forget`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_of` 📖	mathematical	—	`X` `of`	—	—

Pointed.Hom

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	1 math math: `comp_toFun`
`id` 📖	CompOp	1 math math: `id_toFun`
`instInhabited` 📖	CompOp	—
`toFun` 📖	CompOp	23 math math: `typeToPartialFunIsoPartialFunToPointed_inv_app_toFun`, `partialFunEquivPointed_counitIso_inv_app_toFun`, `id_toFun'`, `pointedToPartialFun_map`, `comp_toFun`, `typeToPointed_map_toFun`, `typeToPartialFunIsoPartialFunToPointed_hom_app_toFun`, `partialFunEquivPointed_functor_map_toFun`, `comp_toFun'`, `map_point`, `pointedToTwoPFst_map_hom_toFun`, `id_toFun`, `pointedToBipointedCompBipointedToPointedSnd_hom_app_toFun`, `pointedToBipointedCompBipointedToPointedSnd_inv_app_toFun`, `pointedToBipointedCompBipointedToPointedFst_inv_app_toFun`, `pointedToBipointedCompBipointedToPointedFst_hom_app_toFun`, `Pointed.Iso.mk_inv_toFun`, `partialFunEquivPointed_inverse_map_Dom`, `pointedToTwoPSnd_map_hom_toFun`, `partialFunEquivPointed_counitIso_hom_app_toFun`, `partialFunEquivPointed_inverse_map_get_coe`, `Pointed.Iso.mk_hom_toFun`, `ext_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_toFun` 📖	mathematical	—	`toFun` `comp` `Pointed.X`	—	—
`comp_toFun'` 📖	mathematical	—	`toFun` `CategoryTheory.CategoryStruct.comp` `Pointed` `CategoryTheory.Category.toCategoryStruct` `Pointed.largeCategory` `Pointed.X`	—	—
`ext` 📖	—	`toFun`	—	—	—
`ext_iff` 📖	mathematical	—	`toFun`	—	`ext`
`id_toFun` 📖	mathematical	—	`toFun` `id` `Pointed.X`	—	—
`id_toFun'` 📖	mathematical	—	`toFun` `CategoryTheory.CategoryStruct.id` `Pointed` `CategoryTheory.Category.toCategoryStruct` `Pointed.largeCategory` `Pointed.X`	—	—
`map_point` 📖	mathematical	—	`toFun` `Pointed.point`	—	—

Pointed.Iso

Definitions

Name	Category	Theorems
`mk` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mk_hom_toFun` 📖	mathematical	`DFunLike.coe` `Equiv` `Pointed.X` `EquivLike.toFunLike` `Equiv.instEquivLike` `Pointed.point`	`Pointed.Hom.toFun` `CategoryTheory.Iso.hom` `Pointed` `Pointed.largeCategory`	—	—
`mk_inv_toFun` 📖	mathematical	`DFunLike.coe` `Equiv` `Pointed.X` `EquivLike.toFunLike` `Equiv.instEquivLike` `Pointed.point`	`Pointed.Hom.toFun` `CategoryTheory.Iso.inv` `Pointed` `Pointed.largeCategory` `Equiv.symm`	—	—

(root)

Definitions

Name	Category	Theorems
`typeToPointed` 📖	CompOp	5 math math: `typeToPartialFunIsoPartialFunToPointed_inv_app_toFun`, `typeToPointed_map_toFun`, `typeToPartialFunIsoPartialFunToPointed_hom_app_toFun`, `typeToPointed_obj_X`, `typeToPointed_obj_point`
`typeToPointedForgetAdjunction` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`typeToPointed_map_toFun` 📖	mathematical	—	`Pointed.Hom.toFun` `CategoryTheory.Functor.map` `CategoryTheory.types` `Pointed` `Pointed.largeCategory` `typeToPointed`	—	—
`typeToPointed_obj_X` 📖	mathematical	—	`Pointed.X` `CategoryTheory.Functor.obj` `CategoryTheory.types` `Pointed` `Pointed.largeCategory` `typeToPointed`	—	—
`typeToPointed_obj_point` 📖	mathematical	—	`Pointed.point` `CategoryTheory.Functor.obj` `CategoryTheory.types` `Pointed` `Pointed.largeCategory` `typeToPointed`	—	—

---

← Back to Index