Documentation Verification Report

EndoFunctor

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

Statistics

Metric	Count
Definitions `algebraPreadditive`, `coalgebraPreadditive`	2
Theorems `forget_additive`, `forget_additive`, `algebraPreadditive_homGroup_add_f`, `algebraPreadditive_homGroup_neg_f`, `algebraPreadditive_homGroup_nsmul_f`, `algebraPreadditive_homGroup_sub_f`, `algebraPreadditive_homGroup_zero_f`, `algebraPreadditive_homGroup_zsmul_f`, `coalgebraPreadditive_homGroup_add_f`, `coalgebraPreadditive_homGroup_neg_f`, `coalgebraPreadditive_homGroup_nsmul_f`, `coalgebraPreadditive_homGroup_sub_f`, `coalgebraPreadditive_homGroup_zero_f`, `coalgebraPreadditive_homGroup_zsmul_f`	14
Total	16

CategoryTheory.Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`forget_additive` 📖	mathematical	—	`CategoryTheory.Functor.Additive` `CategoryTheory.Endofunctor.Algebra` `CategoryTheory.Endofunctor.Algebra.instCategory` `CategoryTheory.Endofunctor.algebraPreadditive` `CategoryTheory.Endofunctor.Algebra.forget`	—	—

CategoryTheory.Coalgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`forget_additive` 📖	mathematical	—	`CategoryTheory.Functor.Additive` `CategoryTheory.Endofunctor.Coalgebra` `CategoryTheory.Endofunctor.Coalgebra.instCategory` `CategoryTheory.Endofunctor.coalgebraPreadditive` `CategoryTheory.Endofunctor.Coalgebra.forget`	—	—

CategoryTheory.Endofunctor

Definitions

Name	Category	Theorems
`algebraPreadditive` 📖	CompOp	7 math math: `algebraPreadditive_homGroup_neg_f`, `algebraPreadditive_homGroup_zsmul_f`, `algebraPreadditive_homGroup_sub_f`, `CategoryTheory.Algebra.forget_additive`, `algebraPreadditive_homGroup_zero_f`, `algebraPreadditive_homGroup_add_f`, `algebraPreadditive_homGroup_nsmul_f`
`coalgebraPreadditive` 📖	CompOp	7 math math: `coalgebraPreadditive_homGroup_sub_f`, `coalgebraPreadditive_homGroup_zero_f`, `coalgebraPreadditive_homGroup_neg_f`, `coalgebraPreadditive_homGroup_zsmul_f`, `CategoryTheory.Coalgebra.forget_additive`, `coalgebraPreadditive_homGroup_add_f`, `coalgebraPreadditive_homGroup_nsmul_f`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraPreadditive_homGroup_add_f` 📖	mathematical	—	`Algebra.Hom.f` `Quiver.Hom` `Algebra` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Algebra.instCategory` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `CategoryTheory.Preadditive.homGroup` `algebraPreadditive` `Algebra.a`	—	—
`algebraPreadditive_homGroup_neg_f` 📖	mathematical	—	`Algebra.Hom.f` `Quiver.Hom` `Algebra` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Algebra.instCategory` `SubNegMonoid.toNeg` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup` `algebraPreadditive` `Algebra.a` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—
`algebraPreadditive_homGroup_nsmul_f` 📖	mathematical	—	`Algebra.Hom.f` `Quiver.Hom` `Algebra` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Algebra.instCategory` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup` `algebraPreadditive` `Algebra.a`	—	—
`algebraPreadditive_homGroup_sub_f` 📖	mathematical	—	`Algebra.Hom.f` `Quiver.Hom` `Algebra` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Algebra.instCategory` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup` `algebraPreadditive` `Algebra.a`	—	—
`algebraPreadditive_homGroup_zero_f` 📖	mathematical	—	`Algebra.Hom.f` `Quiver.Hom` `Algebra` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Algebra.instCategory` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup` `algebraPreadditive` `Algebra.a` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms`	—	—
`algebraPreadditive_homGroup_zsmul_f` 📖	mathematical	—	`Algebra.Hom.f` `Quiver.Hom` `Algebra` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Algebra.instCategory` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup` `algebraPreadditive` `Algebra.a`	—	—
`coalgebraPreadditive_homGroup_add_f` 📖	mathematical	—	`Coalgebra.Hom.f` `Quiver.Hom` `Coalgebra` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Coalgebra.instCategory` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `CategoryTheory.Preadditive.homGroup` `coalgebraPreadditive` `Coalgebra.V`	—	—
`coalgebraPreadditive_homGroup_neg_f` 📖	mathematical	—	`Coalgebra.Hom.f` `Quiver.Hom` `Coalgebra` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Coalgebra.instCategory` `SubNegMonoid.toNeg` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup` `coalgebraPreadditive` `Coalgebra.V` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—
`coalgebraPreadditive_homGroup_nsmul_f` 📖	mathematical	—	`Coalgebra.Hom.f` `Quiver.Hom` `Coalgebra` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Coalgebra.instCategory` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup` `coalgebraPreadditive` `Coalgebra.V`	—	—
`coalgebraPreadditive_homGroup_sub_f` 📖	mathematical	—	`Coalgebra.Hom.f` `Quiver.Hom` `Coalgebra` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Coalgebra.instCategory` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup` `coalgebraPreadditive` `Coalgebra.V`	—	—
`coalgebraPreadditive_homGroup_zero_f` 📖	mathematical	—	`Coalgebra.Hom.f` `Quiver.Hom` `Coalgebra` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Coalgebra.instCategory` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup` `coalgebraPreadditive` `Coalgebra.V` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms`	—	—
`coalgebraPreadditive_homGroup_zsmul_f` 📖	mathematical	—	`Coalgebra.Hom.f` `Quiver.Hom` `Coalgebra` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Coalgebra.instCategory` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup` `coalgebraPreadditive` `Coalgebra.V`	—	—

---

← Back to Index