Documentation Verification Report

FunctorCategory

📁 Source: Mathlib/CategoryTheory/Preadditive/FunctorCategory.lean

Statistics

Metric	Count
Definitions `appHom`, `functorCategoryPreadditive`, `instAddHomFunctor`, `instNegHomFunctor`, `instZeroHomFunctor`	5
Theorems `appHom_apply`, `app_add`, `app_neg`, `app_nsmul`, `app_sub`, `app_sum`, `app_units_zsmul`, `app_zero`, `app_zsmul`	9
Total	14

CategoryTheory

Definitions

Name	Category	Theorems
`functorCategoryPreadditive` 📖	CompOp	34 math math: `CatCenter.app_sub`, `Linear.smulOfRingMorphism_smul_eq'`, `NatTrans.app_nsmul`, `Linear.smulOfRingMorphism_smul_eq`, `CatCenter.app_add`, `ModuleCat.smulNatTrans_apply_app`, `HomologicalComplex.tensor_unit_d₂`, `NatTrans.app_sum`, `NatTrans.appHom_apply`, `Abelian.instAdditiveOppositeFunctorAddCommGrpCatExtFunctor`, `presheafToSheaf_additive`, `CatCenter.app_neg_one_zpow`, `CatCenter.localization_zero`, `NatTrans.appLinearMap_apply`, `instPreservesHomologyFunctorAddCommGrpCatColim`, `CochainComplex.mapBifunctorHomologicalComplexShift₁Iso_hom_f_f`, `Functor.instAdditiveObjEvaluation`, `NatTrans.app_smul`, `CochainComplex.mapBifunctorHomologicalComplexShift₁Iso_inv_f_f`, `NatTrans.app_units_zsmul`, `HomologicalComplex.unit_tensor_d₁`, `instAdditiveAdditiveFunctorFunctorForget`, `Action.functorCategoryEquivalence_linear`, `NatTrans.app_zsmul`, `ContinuousCohomology.MultiInd.d_succ`, `Linear.toCatCenter_apply_app`, `CatCenter.app_neg`, `CommShift₂Setup.int_ε`, `Action.functorCategoryEquivalence_additive`, `NatTrans.app_sub`, `PresheafOfModules.instAdditiveFunctorOppositeAbToPresheaf`, `CatCenter.localization_add`, `instAdditiveFunctorColim`, `CommShift₂Setup.int_z`
`instAddHomFunctor` 📖	CompOp	2 math math: `Localization.liftNatTrans_add`, `NatTrans.app_add`
`instNegHomFunctor` 📖	CompOp	1 math math: `NatTrans.app_neg`
`instZeroHomFunctor` 📖	CompOp	5 math math: `ContinuousCohomology.MultiInd.d_comp_d_assoc`, `NatTrans.app_zero`, `ContinuousCohomology.MultiInd.d_comp_d`, `GrothendieckTopology.diagramNatTrans_zero`, `GrothendieckTopology.plusMap_zero`

CategoryTheory.NatTrans

Definitions

Name	Category	Theorems
`appHom` 📖	CompOp	1 math math: `appHom_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`appHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Quiver.Hom` `CategoryTheory.Functor` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.obj` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup` `CategoryTheory.functorCategoryPreadditive` `AddMonoidHom.instFunLike` `appHom` `app`	—	—
`app_add` 📖	mathematical	—	`app` `Quiver.Hom` `CategoryTheory.Functor` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.instAddHomFunctor` `CategoryTheory.Functor.obj` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `CategoryTheory.Preadditive.homGroup`	—	—
`app_neg` 📖	mathematical	—	`app` `Quiver.Hom` `CategoryTheory.Functor` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.instNegHomFunctor` `CategoryTheory.Functor.obj` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `CategoryTheory.Preadditive.homGroup`	—	—
`app_nsmul` 📖	mathematical	—	`app` `Quiver.Hom` `CategoryTheory.Functor` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup` `CategoryTheory.functorCategoryPreadditive` `CategoryTheory.Functor.obj`	—	`AddMonoidHom.map_nsmul`
`app_sub` 📖	mathematical	—	`app` `Quiver.Hom` `CategoryTheory.Functor` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup` `CategoryTheory.functorCategoryPreadditive` `CategoryTheory.Functor.obj`	—	—
`app_sum` 📖	mathematical	—	`app` `Finset.sum` `Quiver.Hom` `CategoryTheory.Functor` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `AddCommGroup.toAddCommMonoid` `CategoryTheory.Preadditive.homGroup` `CategoryTheory.functorCategoryPreadditive` `CategoryTheory.Functor.obj`	—	`map_sum` `AddMonoidHom.instAddMonoidHomClass` `Finset.sum_congr`
`app_units_zsmul` 📖	mathematical	—	`app` `Units` `Int.instMonoid` `Quiver.Hom` `CategoryTheory.Functor` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Units.instSMul` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup` `CategoryTheory.functorCategoryPreadditive` `CategoryTheory.Functor.obj`	—	`app_zsmul`
`app_zero` 📖	mathematical	—	`app` `Quiver.Hom` `CategoryTheory.Functor` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.instZeroHomFunctor` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms`	—	—
`app_zsmul` 📖	mathematical	—	`app` `Quiver.Hom` `CategoryTheory.Functor` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup` `CategoryTheory.functorCategoryPreadditive` `CategoryTheory.Functor.obj`	—	`AddMonoidHom.map_zsmul`

---

← Back to Index