FunctorCategory

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

Statistics

Metric	Count
Definitions appLinearMap, functorCategoryLinear	2
Theorems appLinearMap_apply, app_smul	2
Total	4

CategoryTheory

Definitions

Name	Category	Theorems
functorCategoryLinear 📖	CompOp	3 math math: NatTrans.appLinearMap_apply, NatTrans.app_smul, Action.functorCategoryEquivalence_linear

CategoryTheory.NatTrans

Definitions

Name	Category	Theorems
appLinearMap 📖	CompOp	1 math math: appLinearMap_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
appLinearMap_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.functorCategoryPreadditive CategoryTheory.Linear.homModule CategoryTheory.functorCategoryLinear LinearMap.instFunLike appLinearMap app	—	—
app_smul 📖	mathematical	—	app Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup CategoryTheory.functorCategoryPreadditive DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid CategoryTheory.Linear.homModule CategoryTheory.functorCategoryLinear CategoryTheory.Functor.obj	—	—

---

← Back to Index