EilenbergMoore

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

Statistics

Metric	Count
Definitions coalgebraPreadditive, algebraPreadditive	2
Theorems coalgebraPreadditive_homGroup_add_f, coalgebraPreadditive_homGroup_neg_f, coalgebraPreadditive_homGroup_nsmul_f, coalgebraPreadditive_homGroup_sub_f, coalgebraPreadditive_homGroup_zero_f, coalgebraPreadditive_homGroup_zsmul_f, 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, forget_additive	14
Total	16

CategoryTheory.Comonad

Definitions

Name	Category	Theorems
coalgebraPreadditive 📖	CompOp	7 math math: coalgebraPreadditive_homGroup_neg_f, coalgebraPreadditive_homGroup_nsmul_f, coalgebraPreadditive_homGroup_zsmul_f, forget_additive, coalgebraPreadditive_homGroup_add_f, coalgebraPreadditive_homGroup_sub_f, coalgebraPreadditive_homGroup_zero_f

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coalgebraPreadditive_homGroup_add_f 📖	mathematical	—	Coalgebra.Hom.f Quiver.Hom Coalgebra CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Coalgebra.eilenbergMoore AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup coalgebraPreadditive Coalgebra.A	—	—
coalgebraPreadditive_homGroup_neg_f 📖	mathematical	—	Coalgebra.Hom.f Quiver.Hom Coalgebra CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Coalgebra.eilenbergMoore SubNegMonoid.toNeg AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup coalgebraPreadditive Coalgebra.A 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.eilenbergMoore AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup coalgebraPreadditive Coalgebra.A	—	—
coalgebraPreadditive_homGroup_sub_f 📖	mathematical	—	Coalgebra.Hom.f Quiver.Hom Coalgebra CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Coalgebra.eilenbergMoore SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup coalgebraPreadditive Coalgebra.A	—	—
coalgebraPreadditive_homGroup_zero_f 📖	mathematical	—	Coalgebra.Hom.f Quiver.Hom Coalgebra CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Coalgebra.eilenbergMoore AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup coalgebraPreadditive Coalgebra.A 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.eilenbergMoore SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup coalgebraPreadditive Coalgebra.A	—	—
forget_additive 📖	mathematical	—	CategoryTheory.Functor.Additive Coalgebra Coalgebra.eilenbergMoore coalgebraPreadditive forget	—	—

CategoryTheory.Monad

Definitions

Name	Category	Theorems
algebraPreadditive 📖	CompOp	7 math math: algebraPreadditive_homGroup_sub_f, algebraPreadditive_homGroup_add_f, algebraPreadditive_homGroup_zsmul_f, algebraPreadditive_homGroup_zero_f, algebraPreadditive_homGroup_nsmul_f, forget_additive, algebraPreadditive_homGroup_neg_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.eilenbergMoore 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.eilenbergMoore 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.eilenbergMoore 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.eilenbergMoore 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.eilenbergMoore 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.eilenbergMoore SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup algebraPreadditive Algebra.A	—	—
forget_additive 📖	mathematical	—	CategoryTheory.Functor.Additive Algebra Algebra.eilenbergMoore algebraPreadditive forget	—	—

---

← Back to Index