Documentation Verification Report

Basic

📁 Source: Mathlib/CategoryTheory/Groupoid/Grpd/Basic.lean

Statistics

Metric	Count
Definitions `category`, `forgetToCat`, `instCoeSortType`, `instGroupoidαCategoryObjCatForgetToCat`, `instInhabited`, `objects`, `of`, `piIsoPi`, `piLimitFan`, `piLimitFanIsLimit`, `str'`	11
Theorems `coe_of`, `comp_eq_comp`, `forgetToCat_faithful`, `forgetToCat_full`, `has_pi`, `hom_to_functor`, `id_eq_id`, `id_to_functor`, `piIsoPi_hom_π`	9
Total	20

CategoryTheory.Grpd

Definitions

Name	Category	Theorems
`category` 📖	CompOp	35 math math: `forgetToCat_full`, `FundamentalGroupoidFunctor.piIso_hom`, `ContinuousMap.Homotopy.apply_zero_path`, `piIsoPi_hom_π`, `free_obj`, `free_map`, `ContinuousMap.Homotopy.evalAt_eq`, `id_to_functor`, `ContinuousMap.Homotopy.heq_path_of_eq_image`, `ContinuousMap.Homotopy.eq_path_of_eq_image`, `FundamentalGroupoidFunctor.prodToProdTop_obj`, `FundamentalGroupoidFunctor.prodIso_hom`, `FundamentalGroupoidFunctor.piToPiTop_map`, `ContinuousMap.Homotopy.apply_one_path`, `FundamentalGroupoidFunctor.projLeft_map`, `FundamentalGroupoidFunctor.instIsIsoFanGrpdObjTopCatFundamentalGroupoidFunctorPiTopToPiCone`, `freeForgetAdjunction_homEquiv_symm_apply`, `forgetToCat_faithful`, `has_pi`, `freeForgetAdjunction_counit_app`, `FundamentalGroupoid.map_eq`, `id_eq_id`, `FundamentalGroupoidFunctor.preservesProduct`, `freeForgetAdjunction_homEquiv_apply`, `FundamentalGroupoidFunctor.piToPiTop_obj_as`, `FundamentalGroupoidFunctor.piIso_inv`, `FundamentalGroupoidFunctor.prodIso_inv`, `FundamentalGroupoidFunctor.projRight_map`, `comp_eq_comp`, `freeForgetAdjunction_unit_app`, `hom_to_functor`, `FundamentalGroupoidFunctor.prodToProdTop_map`, `FundamentalGroupoidFunctor.proj_map`, `FundamentalGroupoidFunctor.coneDiscreteComp_obj_mapCone`, `ContinuousMap.Homotopy.eq_diag_path`
`forgetToCat` 📖	CompOp	6 math math: `forgetToCat_full`, `freeForgetAdjunction_homEquiv_symm_apply`, `forgetToCat_faithful`, `freeForgetAdjunction_counit_app`, `freeForgetAdjunction_homEquiv_apply`, `freeForgetAdjunction_unit_app`
`instCoeSortType` 📖	CompOp	—
`instGroupoidαCategoryObjCatForgetToCat` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`objects` 📖	CompOp	—
`of` 📖	CompOp	9 math math: `FundamentalGroupoidFunctor.piIso_hom`, `piIsoPi_hom_π`, `FundamentalGroupoidFunctor.prodIso_hom`, `freeForgetAdjunction_homEquiv_symm_apply`, `freeForgetAdjunction_counit_app`, `coe_of`, `freeForgetAdjunction_homEquiv_apply`, `FundamentalGroupoidFunctor.piIso_inv`, `FundamentalGroupoidFunctor.prodIso_inv`
`piIsoPi` 📖	CompOp	1 math math: `piIsoPi_hom_π`
`piLimitFan` 📖	CompOp	1 math math: `FundamentalGroupoidFunctor.instIsIsoFanGrpdObjTopCatFundamentalGroupoidFunctorPiTopToPiCone`
`piLimitFanIsLimit` 📖	CompOp	—
`str'` 📖	CompOp	23 math math: `FundamentalGroupoidFunctor.piIso_hom`, `ContinuousMap.Homotopy.apply_zero_path`, `piIsoPi_hom_π`, `ContinuousMap.Homotopy.evalAt_eq`, `id_to_functor`, `ContinuousMap.Homotopy.heq_path_of_eq_image`, `ContinuousMap.Homotopy.eq_path_of_eq_image`, `FundamentalGroupoidFunctor.prodToProdTop_obj`, `FundamentalGroupoidFunctor.prodIso_hom`, `FundamentalGroupoidFunctor.piToPiTop_map`, `ContinuousMap.Homotopy.apply_one_path`, `FundamentalGroupoidFunctor.projLeft_map`, `FundamentalGroupoid.map_eq`, `id_eq_id`, `FundamentalGroupoidFunctor.piToPiTop_obj_as`, `FundamentalGroupoidFunctor.piIso_inv`, `FundamentalGroupoidFunctor.prodIso_inv`, `FundamentalGroupoidFunctor.projRight_map`, `comp_eq_comp`, `hom_to_functor`, `FundamentalGroupoidFunctor.prodToProdTop_map`, `FundamentalGroupoidFunctor.proj_map`, `ContinuousMap.Homotopy.eq_diag_path`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_of` 📖	mathematical	—	`CategoryTheory.Bundled.α` `CategoryTheory.Groupoid` `of`	—	—
`comp_eq_comp` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Grpd` `CategoryTheory.Category.toCategoryStruct` `category` `CategoryTheory.Functor.comp` `CategoryTheory.Bundled.α` `CategoryTheory.Groupoid` `CategoryTheory.Groupoid.toCategory` `str'`	—	—
`forgetToCat_faithful` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `CategoryTheory.Grpd` `category` `CategoryTheory.Cat` `CategoryTheory.Cat.category` `forgetToCat`	—	—
`forgetToCat_full` 📖	mathematical	—	`CategoryTheory.Functor.Full` `CategoryTheory.Grpd` `category` `CategoryTheory.Cat` `CategoryTheory.Cat.category` `forgetToCat`	—	—
`has_pi` 📖	mathematical	—	`CategoryTheory.Limits.HasProducts` `CategoryTheory.Grpd` `category`	—	`CategoryTheory.Limits.hasProducts_of_limit_fans`
`hom_to_functor` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Grpd` `CategoryTheory.Category.toCategoryStruct` `category` `CategoryTheory.Functor.comp` `CategoryTheory.Bundled.α` `CategoryTheory.Groupoid` `CategoryTheory.Groupoid.toCategory` `str'`	—	`comp_eq_comp`
`id_eq_id` 📖	mathematical	—	`CategoryTheory.CategoryStruct.id` `CategoryTheory.Grpd` `CategoryTheory.Category.toCategoryStruct` `category` `CategoryTheory.Functor.id` `CategoryTheory.Bundled.α` `CategoryTheory.Groupoid` `CategoryTheory.Groupoid.toCategory` `str'`	—	—
`id_to_functor` 📖	mathematical	—	`CategoryTheory.Functor.id` `CategoryTheory.Bundled.α` `CategoryTheory.Groupoid` `CategoryTheory.Groupoid.toCategory` `str'` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Grpd` `CategoryTheory.Category.toCategoryStruct` `category`	—	—
`piIsoPi_hom_π` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Grpd` `CategoryTheory.Category.toCategoryStruct` `category` `of` `CategoryTheory.groupoidPi` `CategoryTheory.Bundled.α` `CategoryTheory.Groupoid` `str'` `CategoryTheory.Limits.piObj` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `has_pi` `CategoryTheory.Discrete.functor` `CategoryTheory.Iso.hom` `piIsoPi` `CategoryTheory.Limits.Pi.π` `CategoryTheory.Pi.eval` `CategoryTheory.Groupoid.toCategory`	—	`CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `has_pi` `CategoryTheory.Limits.limit.conePointUniqueUpToIso_hom_comp`

---

← Back to Index