Monoidal

📁 Source: Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean

Statistics

Metric	Count
Definitions tensorHom, tensorObj, tensorObjMap, monoidalCategory, monoidalCategoryStruct, instCommRingCarrierObjOppositeRingCatCompCommRingCatForget₂RingHomCarrier	6
Theorems tensorHom_app, tensorObj_map_tmul, tensorObj_obj	3
Total	9

PresheafOfModules

Definitions

Name	Category	Theorems
monoidalCategory 📖	CompOp	—
monoidalCategoryStruct 📖	CompOp	—

PresheafOfModules.Monoidal

Definitions

Name	Category	Theorems
tensorHom 📖	CompOp	1 math math: tensorHom_app
tensorObj 📖	CompOp	3 math math: tensorObj_obj, tensorObj_map_tmul, tensorHom_app
tensorObjMap 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tensorHom_app 📖	mathematical	—	PresheafOfModules.Hom.app CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CommRingCat CommRingCat.instCategory RingCat RingCat.instCategory CategoryTheory.forget₂ RingHom CommRingCat.carrier Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier RingCat.carrier Ring.toSemiring RingCat.ring RingCat.instConcreteCategoryRingHomCarrier CommRingCat.hasForgetToRingCat tensorObj tensorHom CategoryTheory.MonoidalCategoryStruct.tensorHom ModuleCat CategoryTheory.Functor.obj ModuleCat.moduleCategory CommRing.toRing instCommRingCarrierObjOppositeRingCatCompCommRingCatForget₂RingHomCarrier ModuleCat.MonoidalCategory.instMonoidalCategoryStruct PresheafOfModules.obj	—	—
tensorObj_map_tmul 📖	mathematical	—	DFunLike.coe LinearMap CommRingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CommRingCat CommRingCat.instCategory Ring.toSemiring CommRing.toRing CommRingCat.commRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier PresheafOfModules.obj CategoryTheory.Functor.comp RingCat RingCat.instCategory CategoryTheory.forget₂ RingHom CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier RingCat.carrier RingCat.ring RingCat.instConcreteCategoryRingHomCarrier CommRingCat.hasForgetToRingCat tensorObj ModuleCat ModuleCat.moduleCategory ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.Functor.map AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule CategoryTheory.MonoidalCategoryStruct.tensorObj instCommRingCarrierObjOppositeRingCatCompCommRingCatForget₂RingHomCarrier ModuleCat.MonoidalCategory.instMonoidalCategoryStruct CommRingCat.Hom.hom LinearMap.instFunLike ModuleCat.Hom.hom PresheafOfModules.map TensorProduct.tmul ModuleCat.instModuleCarrierObjRestrictScalars CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier	—	—
tensorObj_obj 📖	mathematical	—	PresheafOfModules.obj CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CommRingCat CommRingCat.instCategory RingCat RingCat.instCategory CategoryTheory.forget₂ RingHom CommRingCat.carrier Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier RingCat.carrier Ring.toSemiring RingCat.ring RingCat.instConcreteCategoryRingHomCarrier CommRingCat.hasForgetToRingCat tensorObj CategoryTheory.MonoidalCategoryStruct.tensorObj ModuleCat CategoryTheory.Functor.obj ModuleCat.moduleCategory CommRing.toRing instCommRingCarrierObjOppositeRingCatCompCommRingCatForget₂RingHomCarrier ModuleCat.MonoidalCategory.instMonoidalCategoryStruct	—	—

(root)

Definitions

Name	Category	Theorems
instCommRingCarrierObjOppositeRingCatCompCommRingCatForget₂RingHomCarrier 📖	CompOp	3 math math: PresheafOfModules.Monoidal.tensorObj_obj, PresheafOfModules.Monoidal.tensorObj_map_tmul, PresheafOfModules.Monoidal.tensorHom_app

---

← Back to Index