Basic

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

Statistics

Metric	Count
Definitions `instMonoidalCategoryStruct`, `tensorLift`, `instCommRingCarrierTensorUnit`, `monoidalCategory`, `associator`, `instMonoidalCategoryStruct`, `leftUnitor`, `rightUnitor`, `tensorHom`, `tensorLift`, `tensorObj`, `whiskerLeft`, `whiskerRight`, `instCommSemiringCarrierTensorUnit`, `monoidalCategory`	15
Theorems `associator_def`, `associator_hom_apply`, `associator_inv_apply`, `leftUnitor_def`, `leftUnitor_hom_apply`, `leftUnitor_inv_apply`, `rightUnitor_def`, `rightUnitor_hom_apply`, `rightUnitor_inv_apply`, `tensorHom_def`, `tensorHom_tmul`, `tensorLift_tmul`, `tensorObj`, `tensorObj_carrier`, `tensorObj_def`, `tensorObj_isAddCommGroup`, `tensorObj_isModule`, `tensorUnit_carrier`, `tensorUnit_isAddCommGroup`, `tensorUnit_isModule`, `tensor_ext`, `tensor_ext₃`, `tensor_ext₃'`, `whiskerLeft_apply`, `whiskerLeft_def`, `whiskerRight_apply`, `whiskerRight_def`, `hom_hom_associator`, `hom_hom_leftUnitor`, `hom_hom_rightUnitor`, `hom_inv_associator`, `hom_inv_leftUnitor`, `hom_inv_rightUnitor`, `hom_tensorHom`, `hom_whiskerLeft`, `hom_whiskerRight`, `instMonoidalLinear`, `instMonoidalPreadditive`, `ofHom₂_compr₂`, `associator_def`, `associator_hom_apply`, `associator_inv_apply`, `associator_naturality`, `id_tensorHom_id`, `leftUnitor_def`, `leftUnitor_hom_apply`, `leftUnitor_inv_apply`, `leftUnitor_naturality`, `pentagon`, `rightUnitor_def`, `rightUnitor_hom_apply`, `rightUnitor_inv_apply`, `rightUnitor_naturality`, `tensorHom_comp_tensorHom`, `tensorHom_def`, `tensorHom_tmul`, `tensorLift_tmul`, `tensorObj_def`, `tensorUnit_carrier`, `tensorUnit_isAddCommMonoid`, `tensorUnit_isModule`, `tensor_ext`, `tensor_ext₃`, `tensor_ext₃'`, `triangle`, `whiskerLeft_apply`, `whiskerLeft_def`, `whiskerRight_apply`, `whiskerRight_def`, `hom_hom_associator`, `hom_hom_leftUnitor`, `hom_hom_rightUnitor`, `hom_inv_associator`, `hom_inv_leftUnitor`, `hom_inv_rightUnitor`, `hom_tensorHom`, `hom_whiskerLeft`, `hom_whiskerRight`	78
Total	93

ModuleCat

Definitions

Name	Category	Theorems
`instCommRingCarrierTensorUnit` 📖	CompOp	3 math math: `free_ε_one`, `free_η_freeMk`, `FGModuleCat.FGModuleCatEvaluation_apply'`
`monoidalCategory` 📖	CompOp	99 math math: `Representation.repOfTprodIso_inv_apply`, `MonoidalCategory.braiding_hom_apply`, `Rep.MonoidalClosed.linearHomEquiv_symm_hom`, `TannakaDuality.FiniteGroup.toRightFDRepComp_in_rightRegular`, `FDRep.char_tensor`, `Representation.repOfTprodIso_apply`, `instSmallUnitsSkeletonModuleCat`, `Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_left`, `monoidalClosed_uncurry`, `TannakaDuality.FiniteGroup.forget_obj`, `Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_right`, `Rep.coinvariantsTensorFreeLEquiv_symm_apply`, `Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_single`, `CoalgCat.comonEquivalence_inverse`, `Rep.homEquiv_apply_hom`, `CoalgCat.comonEquivalence_counitIso`, `Module.Flat.lTensor_shortComplex_exact`, `Rep.ihom_ev_app_hom`, `Rep.MonoidalClosed.linearHomEquivComm_hom`, `Rep.homEquiv_def`, `FGModuleCat.FGModuleCatEvaluation_apply`, `monoidalClosed_curry`, `Module.Flat.iff_rTensor_preserves_shortComplex_exact`, `CoalgCat.toComonObj_X`, `FGModuleCat.instIsMonoidalClosedModuleCatIsFG`, `Rep.coinvariantsTensorFreeLEquiv_apply`, `Module.Flat.iff_lTensor_preserves_shortComplex_exact`, `CoalgCat.comul_def`, `CoalgCat.MonoidalCategory.inducingFunctorData_μIso`, `CoalgCat.MonoidalCategory.inducingFunctorData_εIso`, `FGModuleCat.FGModuleCatCoevaluation_apply_one`, `MonModuleEquivalenceAlgebra.functor_map_hom_apply`, `Rep.finsuppTensorRight_hom_hom`, `free_ε_one`, `TannakaDuality.FiniteGroup.forget_map`, `MonModuleEquivalenceAlgebra.functor_obj_carrier`, `Rep.tensor_ρ`, `Rep.linearization_η_hom_apply`, `FGModuleCat.ihom_obj`, `CoalgCat.comonEquivalence_functor`, `CoalgCat.ofComonObjCoalgebraStruct_comul`, `MonoidalCategory.tensorμ_eq_tensorTensorTensorComm`, `free_η_freeMk`, `MonModuleEquivalenceAlgebra.inverse_obj_mon`, `CoalgCat.comonEquivalence_unitIso`, `free_μ_freeMk_tmul_freeMk`, `Rep.diagonalSuccIsoTensorTrivial_hom_hom_single`, `CoalgCat.counit_def`, `MonModuleEquivalenceAlgebra.algebraMap`, `MonoidalCategory.tensorμ_apply`, `ihom_map_apply`, `MonModuleEquivalenceAlgebra.inverseObj_mul`, `ihom_coev_app`, `Rep.finsuppTensorRight_inv_hom`, `instMonoidalLinear`, `Rep.finsuppTensorLeft_inv_hom`, `free_δ_freeMk`, `Rep.leftRegularTensorTrivialIsoFree_inv_hom`, `FGModuleCat.tensorObj_obj`, `FGModuleCat.tensorUnit_obj`, `Rep.linearization_δ_hom`, `MonModuleEquivalenceAlgebra.inverse_obj_X_isAddCommGroup`, `Rep.MonoidalClosed.linearHomEquiv_hom`, `Module.Flat.iff_preservesFiniteLimits_tensorLeft`, `Rep.finsuppTensorLeft_hom_hom`, `Rep.coinvariantsTensorMk_apply`, `Rep.homEquiv_symm_apply_hom`, `CoalgCat.toComon_map_hom`, `preservesFiniteLimits_tensorLeft_of_ringHomFlat`, `Rep.ihom_coev_app_hom`, `FGModuleCat.FGModuleCatEvaluation_apply'`, `Module.Flat.instPreservesFiniteLimitsModuleCatTensorLeftOfCarrier`, `MonModuleEquivalenceAlgebra.inverse_obj_X_carrier`, `CoalgCat.ofComonObjCoalgebraStruct_counit`, `Rep.leftRegularTensorTrivialIsoFree_hom_hom_single_tmul_single`, `instMonoidalPreadditive`, `groupHomology.inhomogeneousChains.d_eq`, `Rep.MonoidalClosed.linearHomEquivComm_symm_hom`, `TannakaDuality.FiniteGroup.map_mul_toRightFDRepComp`, `MonModuleEquivalenceAlgebra.inverse_map_hom`, `MonModuleEquivalenceAlgebra.inverse_obj_X_isModule`, `MonoidalCategory.braiding_inv_apply`, `instInvertibleCarrierOutModuleCatValSkeleton`, `monoidalClosed_pre_app`, `Rep.ihom_obj_ρ_def`, `TannakaDuality.FiniteGroup.equivHom_surjective`, `Rep.leftRegularTensorTrivialIsoFree_hom_hom`, `TannakaDuality.FiniteGroup.equivHom_injective`, `FDRep.dualTensorIsoLinHom_hom_hom`, `Rep.linearization_ε_hom`, `CoalgCat.toComon_obj`, `MonModuleEquivalenceAlgebra.inverseObj_one`, `Module.Flat.rTensor_shortComplex_exact`, `TannakaDuality.FiniteGroup.equivHom_apply`, `ihom_ev_app`, `LightCondensed.instIsMonoidalFunctorOppositeLightProfiniteModuleCatWCoherentTopology`, `FGModuleCat.instIsMonoidalModuleCatIsFG`, `Rep.leftRegularTensorTrivialIsoFree_inv_hom_single_single`, `Rep.linearization_μ_hom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hom_hom_associator` 📖	mathematical	—	`Hom.hom` `CommRing.toRing` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `ModuleCat` `moduleCategory` `MonoidalCategory.instMonoidalCategoryStruct` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.associator` `LinearEquiv.toLinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `carrier` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `TensorProduct.assoc`	—	—
`hom_hom_leftUnitor` 📖	mathematical	—	`Hom.hom` `CommRing.toRing` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `ModuleCat` `moduleCategory` `MonoidalCategory.instMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.leftUnitor` `LinearEquiv.toLinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `carrier` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `Semiring.toModule` `isModule` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `TensorProduct.lid`	—	—
`hom_hom_rightUnitor` 📖	mathematical	—	`Hom.hom` `CommRing.toRing` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `ModuleCat` `moduleCategory` `MonoidalCategory.instMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.rightUnitor` `LinearEquiv.toLinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `carrier` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `isModule` `Semiring.toModule` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `TensorProduct.rid`	—	—
`hom_inv_associator` 📖	mathematical	—	`Hom.hom` `CommRing.toRing` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `ModuleCat` `moduleCategory` `MonoidalCategory.instMonoidalCategoryStruct` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategoryStruct.associator` `LinearEquiv.toLinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `carrier` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearEquiv.symm` `TensorProduct.assoc`	—	—
`hom_inv_leftUnitor` 📖	mathematical	—	`Hom.hom` `CommRing.toRing` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `ModuleCat` `moduleCategory` `MonoidalCategory.instMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategoryStruct.leftUnitor` `LinearEquiv.toLinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `carrier` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `Semiring.toModule` `isModule` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearEquiv.symm` `TensorProduct.lid`	—	—
`hom_inv_rightUnitor` 📖	mathematical	—	`Hom.hom` `CommRing.toRing` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `ModuleCat` `moduleCategory` `MonoidalCategory.instMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategoryStruct.rightUnitor` `LinearEquiv.toLinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `carrier` `TensorProduct` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `isModule` `Semiring.toModule` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearEquiv.symm` `TensorProduct.rid`	—	—
`hom_tensorHom` 📖	mathematical	—	`Hom.hom` `CommRing.toRing` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `ModuleCat` `moduleCategory` `MonoidalCategory.instMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorHom` `TensorProduct.map` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `carrier` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule`	—	—
`hom_whiskerLeft` 📖	mathematical	—	`Hom.hom` `CommRing.toRing` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `ModuleCat` `moduleCategory` `MonoidalCategory.instMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `LinearMap.lTensor` `CommRing.toCommSemiring` `carrier` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule`	—	—
`hom_whiskerRight` 📖	mathematical	—	`Hom.hom` `CommRing.toRing` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `ModuleCat` `moduleCategory` `MonoidalCategory.instMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.whiskerRight` `LinearMap.rTensor` `CommRing.toCommSemiring` `carrier` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule`	—	—
`instMonoidalLinear` 📖	mathematical	—	`CategoryTheory.MonoidalLinear` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ModuleCat` `CommRing.toRing` `moduleCategory` `instPreadditive` `instLinear` `monoidalCategory` `instMonoidalPreadditive`	—	`instMonoidalPreadditive` `hom_ext` `TensorProduct.ext` `LinearMap.ext` `smulCommClass_self` `RingHomCompTriple.ids` `MonoidalCategory.whiskerLeft_apply` `TensorProduct.tmul_smul` `TensorProduct.CompatibleSMul.isScalarTower` `IsScalarTower.left` `MonoidalCategory.whiskerRight_apply` `TensorProduct.smul_tmul`
`instMonoidalPreadditive` 📖	mathematical	—	`CategoryTheory.MonoidalPreadditive` `ModuleCat` `CommRing.toRing` `moduleCategory` `instPreadditive` `monoidalCategory`	—	`hom_ext` `TensorProduct.ext` `LinearMap.ext` `smulCommClass_self` `RingHomCompTriple.ids` `MonoidalCategory.whiskerLeft_apply` `TensorProduct.tmul_zero` `MonoidalCategory.whiskerRight_apply` `TensorProduct.zero_tmul` `TensorProduct.tmul_add` `TensorProduct.add_tmul`
`ofHom₂_compr₂` 📖	mathematical	—	`ofHom₂` `LinearMap.compr₂` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `carrier` `CommRing.toRing` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CategoryTheory.CategoryStruct.comp` `ModuleCat` `CategoryTheory.Category.toCategoryStruct` `moduleCategory` `of` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `instAddCommGroupHom` `Hom.instModule` `CategoryTheory.Preadditive.homGroup` `instPreadditive` `CategoryTheory.Linear.homModule` `instLinear` `ofHom` `CategoryTheory.Linear.rightComp`	—	`smulCommClass_self` `IsScalarTower.left`

ModuleCat.MonoidalCategory

Definitions

Name	Category	Theorems
`instMonoidalCategoryStruct` 📖	CompOp	50 math math: `PresheafOfModules.Monoidal.tensorObj_obj`, `QuadraticModuleCat.forget₂_map_associator_inv`, `ModuleCat.hom_tensorHom`, `associator_hom_apply`, `tensorHom_tmul`, `whiskerLeft_def`, `tensorHom_def`, `PresheafOfModules.Monoidal.tensorObj_map_tmul`, `ModuleCat.monoidalClosed_curry`, `leftUnitor_hom_apply`, `ModuleCat.hom_whiskerRight`, `ModuleCat.hom_inv_associator`, `rightUnitor_def`, `associator_def`, `ModuleCat.hom_whiskerLeft`, `tensorUnit_carrier`, `rightUnitor_hom_apply`, `tensorLift_tmul`, `ModuleCat.hom_hom_leftUnitor`, `ModuleCat.hom_hom_rightUnitor`, `QuadraticModuleCat.forget₂_map_associator_hom`, `ModuleCat.FreeMonoidal.εIso_inv_freeMk`, `ModuleCat.hom_inv_rightUnitor`, `QuadraticModuleCat.toModuleCat_tensor`, `Rep.diagonalSuccIsoTensorTrivial_hom_hom_single`, `tensorObj`, `ModuleCat.FreeMonoidal.μIso_hom_freeMk_tmul_freeMk`, `rightUnitor_inv_apply`, `leftUnitor_inv_apply`, `tensorObj_isModule`, `tensorObj_isAddCommGroup`, `ModuleCat.hom_hom_associator`, `PresheafOfModules.Monoidal.tensorHom_app`, `whiskerRight_apply`, `tensorUnit_isModule`, `FGModuleCat.tensorObj_obj`, `FGModuleCat.tensorUnit_obj`, `ModuleCat.FreeMonoidal.μIso_inv_freeMk`, `leftUnitor_def`, `tensorObj_def`, `FGModuleCat.FGModuleCatEvaluation_apply'`, `ModuleCat.hom_inv_leftUnitor`, `ModuleCat.FreeMonoidal.εIso_hom_one`, `Rep.leftRegularTensorTrivialIsoFree_hom_hom_single_tmul_single`, `whiskerLeft_apply`, `whiskerRight_def`, `tensorObj_carrier`, `tensorUnit_isAddCommGroup`, `associator_inv_apply`, `Rep.leftRegularTensorTrivialIsoFree_inv_hom_single_single`
`tensorLift` 📖	CompOp	1 math math: `tensorLift_tmul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`associator_def` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.associator` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `instMonoidalCategoryStruct` `LinearEquiv.toModuleIso` `TensorProduct` `CommRing.toCommSemiring` `ModuleCat.carrier` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `TensorProduct.addCommGroup` `TensorProduct.assoc`	—	—
`associator_hom_apply` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `instMonoidalCategoryStruct` `ModuleCat.carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.associator` `TensorProduct.tmul` `CommRing.toCommSemiring` `TensorProduct` `TensorProduct.addCommMonoid`	—	—
`associator_inv_apply` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `instMonoidalCategoryStruct` `ModuleCat.carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategoryStruct.associator` `TensorProduct.tmul` `CommRing.toCommSemiring` `TensorProduct` `TensorProduct.addCommMonoid`	—	—
`leftUnitor_def` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.leftUnitor` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `instMonoidalCategoryStruct` `LinearEquiv.toModuleIso` `TensorProduct` `CommRing.toCommSemiring` `ModuleCat.carrier` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `Semiring.toModule` `ModuleCat.isModule` `TensorProduct.addCommGroup` `Ring.toAddCommGroup` `TensorProduct.instModule` `TensorProduct.lid`	—	—
`leftUnitor_hom_apply` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `instMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `ModuleCat.carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.leftUnitor` `TensorProduct.tmul` `CommRing.toCommSemiring` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Module.toDistribMulAction`	—	`TensorProduct.lid_tmul`
`leftUnitor_inv_apply` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `instMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `ModuleCat.carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategoryStruct.leftUnitor` `TensorProduct.tmul` `CommRing.toCommSemiring` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`TensorProduct.lid_symm_apply`
`rightUnitor_def` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.rightUnitor` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `instMonoidalCategoryStruct` `LinearEquiv.toModuleIso` `TensorProduct` `CommRing.toCommSemiring` `ModuleCat.carrier` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ModuleCat.isModule` `Semiring.toModule` `TensorProduct.addCommGroup` `TensorProduct.instModule` `TensorProduct.rid`	—	—
`rightUnitor_hom_apply` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `instMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `ModuleCat.carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.rightUnitor` `TensorProduct.tmul` `CommRing.toCommSemiring` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Module.toDistribMulAction`	—	`TensorProduct.rid_tmul`
`rightUnitor_inv_apply` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `instMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `ModuleCat.carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategoryStruct.rightUnitor` `TensorProduct.tmul` `CommRing.toCommSemiring` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`TensorProduct.rid_symm_apply`
`tensorHom_def` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.tensorHom` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `instMonoidalCategoryStruct` `ModuleCat.ofHom` `TensorProduct` `CommRing.toCommSemiring` `ModuleCat.carrier` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `TensorProduct.addCommGroup` `TensorProduct.instModule` `TensorProduct.map` `RingHom.id` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `ModuleCat.Hom.hom`	—	—
`tensorHom_tmul` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `instMonoidalCategoryStruct` `ModuleCat.carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.MonoidalCategoryStruct.tensorHom` `TensorProduct.tmul` `CommRing.toCommSemiring`	—	—
`tensorLift_tmul` 📖	mathematical	`ModuleCat.carrier` `CommRing.toRing` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `ModuleCat.isModule`	`DFunLike.coe` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `ModuleCat` `ModuleCat.moduleCategory` `instMonoidalCategoryStruct` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `tensorLift` `TensorProduct.tmul`	—	—
`tensorObj` 📖	mathematical	—	`ModuleCat.carrier` `CommRing.toRing` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `ModuleCat` `ModuleCat.moduleCategory` `instMonoidalCategoryStruct` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule`	—	`tensorObj_carrier`
`tensorObj_carrier` 📖	mathematical	—	`ModuleCat.carrier` `CommRing.toRing` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `ModuleCat` `ModuleCat.moduleCategory` `instMonoidalCategoryStruct` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule`	—	—
`tensorObj_def` 📖	mathematical	—	`ModuleCat.carrier` `CommRing.toRing` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `ModuleCat` `ModuleCat.moduleCategory` `instMonoidalCategoryStruct` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule`	—	`tensorObj_carrier`
`tensorObj_isAddCommGroup` 📖	mathematical	—	`ModuleCat.isAddCommGroup` `CommRing.toRing` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `ModuleCat` `ModuleCat.moduleCategory` `instMonoidalCategoryStruct` `TensorProduct.addCommGroup` `CommRing.toCommSemiring` `ModuleCat.carrier` `AddCommGroup.toAddCommMonoid` `ModuleCat.isModule`	—	—
`tensorObj_isModule` 📖	mathematical	—	`ModuleCat.isModule` `CommRing.toRing` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `ModuleCat` `ModuleCat.moduleCategory` `instMonoidalCategoryStruct` `TensorProduct.instModule` `CommRing.toCommSemiring` `ModuleCat.carrier` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup`	—	—
`tensorUnit_carrier` 📖	mathematical	—	`ModuleCat.carrier` `CommRing.toRing` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `ModuleCat` `ModuleCat.moduleCategory` `instMonoidalCategoryStruct`	—	—
`tensorUnit_isAddCommGroup` 📖	mathematical	—	`ModuleCat.isAddCommGroup` `CommRing.toRing` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `ModuleCat` `ModuleCat.moduleCategory` `instMonoidalCategoryStruct` `Ring.toAddCommGroup`	—	—
`tensorUnit_isModule` 📖	mathematical	—	`ModuleCat.isModule` `CommRing.toRing` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `ModuleCat` `ModuleCat.moduleCategory` `instMonoidalCategoryStruct` `Semiring.toModule` `Ring.toSemiring`	—	—
`tensor_ext` 📖	—	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `CommRing.toRing` `RingHom.id` `Semiring.toNonAssocSemiring` `ModuleCat.carrier` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `ModuleCat` `ModuleCat.moduleCategory` `instMonoidalCategoryStruct` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.Hom.hom` `TensorProduct.tmul` `CommRing.toCommSemiring`	—	—	`ModuleCat.hom_ext` `TensorProduct.ext` `LinearMap.ext` `smulCommClass_self` `RingHomCompTriple.ids`
`tensor_ext₃` 📖	—	`DFunLike.coe` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `instMonoidalCategoryStruct` `ModuleCat.carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `TensorProduct.tmul` `CommRing.toCommSemiring`	—	—	`CategoryTheory.cancel_epi` `CategoryTheory.epi_of_strongEpi` `CategoryTheory.strongEpi_of_isIso` `CategoryTheory.Iso.isIso_hom` `tensor_ext₃'`
`tensor_ext₃'` 📖	—	`DFunLike.coe` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `instMonoidalCategoryStruct` `ModuleCat.carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `TensorProduct.tmul` `CommRing.toCommSemiring`	—	—	`ModuleCat.hom_ext` `TensorProduct.ext_threefold`
`whiskerLeft_apply` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `instMonoidalCategoryStruct` `ModuleCat.carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `TensorProduct.tmul` `CommRing.toCommSemiring`	—	—
`whiskerLeft_def` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `instMonoidalCategoryStruct` `ModuleCat.ofHom` `TensorProduct` `CommRing.toCommSemiring` `ModuleCat.carrier` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `TensorProduct.addCommGroup` `TensorProduct.instModule` `LinearMap.lTensor` `ModuleCat.Hom.hom`	—	—
`whiskerRight_apply` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `instMonoidalCategoryStruct` `ModuleCat.carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.MonoidalCategoryStruct.whiskerRight` `TensorProduct.tmul` `CommRing.toCommSemiring`	—	—
`whiskerRight_def` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.whiskerRight` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `instMonoidalCategoryStruct` `ModuleCat.ofHom` `TensorProduct` `CommRing.toCommSemiring` `ModuleCat.carrier` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `TensorProduct.addCommGroup` `TensorProduct.instModule` `LinearMap.rTensor` `ModuleCat.Hom.hom`	—	—

SemimoduleCat

Definitions

Name	Category	Theorems
`instCommSemiringCarrierTensorUnit` 📖	CompOp	—
`monoidalCategory` 📖	CompOp	13 math math: `CommRing.Pic.mul_eq_tensor`, `instInvertibleCarrierOutSemimoduleCatValSkeleton`, `CommRing.Pic.inv_eq_dual`, `CommRing.Pic.mk_eq_iff`, `CommRing.Pic.mk_eq_self`, `CommRing.Pic.mapAlgebra_apply`, `CommRing.Pic.ext_iff`, `CommRing.Pic.instFreeAsModuleOfNat`, `MonoidalCategory.tensorμ_apply`, `MonoidalCategory.braiding_hom_apply`, `MonoidalCategory.braiding_inv_apply`, `MonoidalCategory.tensorμ_eq_tensorTensorTensorComm`, `instSmallUnitsSkeletonSemimoduleCat`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hom_hom_associator` 📖	mathematical	—	`Hom.hom` `CommSemiring.toSemiring` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SemimoduleCat` `moduleCategory` `MonoidalCategory.instMonoidalCategoryStruct` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.associator` `LinearEquiv.toLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `carrier` `isAddCommMonoid` `isModule` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `TensorProduct.assoc`	—	—
`hom_hom_leftUnitor` 📖	mathematical	—	`Hom.hom` `CommSemiring.toSemiring` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SemimoduleCat` `moduleCategory` `MonoidalCategory.instMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.leftUnitor` `LinearEquiv.toLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `carrier` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `isAddCommMonoid` `Semiring.toModule` `isModule` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `TensorProduct.lid`	—	—
`hom_hom_rightUnitor` 📖	mathematical	—	`Hom.hom` `CommSemiring.toSemiring` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SemimoduleCat` `moduleCategory` `MonoidalCategory.instMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.rightUnitor` `LinearEquiv.toLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `carrier` `isAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `isModule` `Semiring.toModule` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `TensorProduct.rid`	—	—
`hom_inv_associator` 📖	mathematical	—	`Hom.hom` `CommSemiring.toSemiring` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SemimoduleCat` `moduleCategory` `MonoidalCategory.instMonoidalCategoryStruct` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategoryStruct.associator` `LinearEquiv.toLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `carrier` `isAddCommMonoid` `isModule` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearEquiv.symm` `TensorProduct.assoc`	—	—
`hom_inv_leftUnitor` 📖	mathematical	—	`Hom.hom` `CommSemiring.toSemiring` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SemimoduleCat` `moduleCategory` `MonoidalCategory.instMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategoryStruct.leftUnitor` `LinearEquiv.toLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `carrier` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `isAddCommMonoid` `Semiring.toModule` `isModule` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearEquiv.symm` `TensorProduct.lid`	—	—
`hom_inv_rightUnitor` 📖	mathematical	—	`Hom.hom` `CommSemiring.toSemiring` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SemimoduleCat` `moduleCategory` `MonoidalCategory.instMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategoryStruct.rightUnitor` `LinearEquiv.toLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `carrier` `TensorProduct` `isAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `isModule` `Semiring.toModule` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearEquiv.symm` `TensorProduct.rid`	—	—
`hom_tensorHom` 📖	mathematical	—	`Hom.hom` `CommSemiring.toSemiring` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SemimoduleCat` `moduleCategory` `MonoidalCategory.instMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorHom` `TensorProduct.map` `RingHom.id` `Semiring.toNonAssocSemiring` `carrier` `isAddCommMonoid` `isModule`	—	—
`hom_whiskerLeft` 📖	mathematical	—	`Hom.hom` `CommSemiring.toSemiring` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SemimoduleCat` `moduleCategory` `MonoidalCategory.instMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `LinearMap.lTensor` `carrier` `isAddCommMonoid` `isModule`	—	—
`hom_whiskerRight` 📖	mathematical	—	`Hom.hom` `CommSemiring.toSemiring` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SemimoduleCat` `moduleCategory` `MonoidalCategory.instMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.whiskerRight` `LinearMap.rTensor` `carrier` `isAddCommMonoid` `isModule`	—	—

SemimoduleCat.MonoidalCategory

Definitions

Name	Category	Theorems
`associator` 📖	CompOp	4 math math: `triangle`, `associator_naturality`, `associator_def`, `pentagon`
`instMonoidalCategoryStruct` 📖	CompOp	34 math math: `rightUnitor_hom_apply`, `SemimoduleCat.hom_inv_rightUnitor`, `tensorHom_tmul`, `whiskerRight_apply`, `braiding_naturality_right`, `rightUnitor_inv_apply`, `SemimoduleCat.hom_hom_rightUnitor`, `tensorLift_tmul`, `tensorUnit_isAddCommMonoid`, `whiskerLeft_def`, `SemimoduleCat.hom_inv_leftUnitor`, `tensorObj_def`, `SemimoduleCat.hom_tensorHom`, `SemimoduleCat.hom_inv_associator`, `associator_def`, `SemimoduleCat.hom_whiskerLeft`, `leftUnitor_def`, `hexagon_forward`, `rightUnitor_def`, `associator_inv_apply`, `whiskerLeft_apply`, `SemimoduleCat.hom_whiskerRight`, `SemimoduleCat.hom_hom_associator`, `leftUnitor_inv_apply`, `tensorHom_def`, `braiding_naturality`, `hexagon_reverse`, `SemimoduleCat.hom_hom_leftUnitor`, `tensorUnit_isModule`, `leftUnitor_hom_apply`, `whiskerRight_def`, `braiding_naturality_left`, `associator_hom_apply`, `tensorUnit_carrier`
`leftUnitor` 📖	CompOp	3 math math: `triangle`, `leftUnitor_def`, `leftUnitor_naturality`
`rightUnitor` 📖	CompOp	3 math math: `triangle`, `rightUnitor_def`, `rightUnitor_naturality`
`tensorHom` 📖	CompOp	7 math math: `triangle`, `associator_naturality`, `tensorHom_comp_tensorHom`, `leftUnitor_naturality`, `tensorHom_def`, `rightUnitor_naturality`, `id_tensorHom_id`
`tensorLift` 📖	CompOp	1 math math: `tensorLift_tmul`
`tensorObj` 📖	CompOp	7 math math: `triangle`, `associator_naturality`, `tensorObj_def`, `tensorHom_comp_tensorHom`, `leftUnitor_naturality`, `rightUnitor_naturality`, `pentagon`
`whiskerLeft` 📖	CompOp	2 math math: `whiskerLeft_def`, `pentagon`
`whiskerRight` 📖	CompOp	2 math math: `whiskerRight_def`, `pentagon`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`associator_def` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.associator` `SemimoduleCat` `CommSemiring.toSemiring` `SemimoduleCat.moduleCategory` `instMonoidalCategoryStruct` `associator`	—	—
`associator_hom_apply` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SemimoduleCat` `CommSemiring.toSemiring` `SemimoduleCat.moduleCategory` `instMonoidalCategoryStruct` `SemimoduleCat.carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SemimoduleCat.isAddCommMonoid` `SemimoduleCat.isModule` `LinearMap.instFunLike` `SemimoduleCat.instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.associator` `TensorProduct.tmul` `TensorProduct` `TensorProduct.addCommMonoid`	—	—
`associator_inv_apply` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SemimoduleCat` `CommSemiring.toSemiring` `SemimoduleCat.moduleCategory` `instMonoidalCategoryStruct` `SemimoduleCat.carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SemimoduleCat.isAddCommMonoid` `SemimoduleCat.isModule` `LinearMap.instFunLike` `SemimoduleCat.instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategoryStruct.associator` `TensorProduct.tmul` `TensorProduct` `TensorProduct.addCommMonoid`	—	—
`associator_naturality` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SemimoduleCat` `CommSemiring.toSemiring` `CategoryTheory.Category.toCategoryStruct` `SemimoduleCat.moduleCategory` `tensorObj` `tensorHom` `CategoryTheory.Iso.hom` `associator`	—	`SemimoduleCat.hom_ext` `TensorProduct.ext_threefold`
`id_tensorHom_id` 📖	mathematical	—	`tensorHom` `CategoryTheory.CategoryStruct.id` `SemimoduleCat` `CommSemiring.toSemiring` `CategoryTheory.Category.toCategoryStruct` `SemimoduleCat.moduleCategory` `SemimoduleCat.of` `TensorProduct` `SemimoduleCat.carrier` `SemimoduleCat.isAddCommMonoid` `SemimoduleCat.isModule` `TensorProduct.addCommMonoid` `TensorProduct.instModule`	—	`SemimoduleCat.hom_ext` `TensorProduct.ext` `smulCommClass_self` `RingHomCompTriple.ids`
`leftUnitor_def` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.leftUnitor` `SemimoduleCat` `CommSemiring.toSemiring` `SemimoduleCat.moduleCategory` `instMonoidalCategoryStruct` `leftUnitor`	—	—
`leftUnitor_hom_apply` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SemimoduleCat` `CommSemiring.toSemiring` `SemimoduleCat.moduleCategory` `instMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `SemimoduleCat.carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SemimoduleCat.isAddCommMonoid` `SemimoduleCat.isModule` `LinearMap.instFunLike` `SemimoduleCat.instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.leftUnitor` `TensorProduct.tmul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`TensorProduct.lid_tmul`
`leftUnitor_inv_apply` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SemimoduleCat` `CommSemiring.toSemiring` `SemimoduleCat.moduleCategory` `instMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `SemimoduleCat.carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SemimoduleCat.isAddCommMonoid` `SemimoduleCat.isModule` `LinearMap.instFunLike` `SemimoduleCat.instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategoryStruct.leftUnitor` `TensorProduct.tmul` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`TensorProduct.lid_symm_apply`
`leftUnitor_naturality` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SemimoduleCat` `CommSemiring.toSemiring` `CategoryTheory.Category.toCategoryStruct` `SemimoduleCat.moduleCategory` `tensorObj` `SemimoduleCat.of` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `tensorHom` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Iso.hom` `TensorProduct` `SemimoduleCat.carrier` `SemimoduleCat.isAddCommMonoid` `SemimoduleCat.isModule` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `leftUnitor`	—	`SemimoduleCat.hom_ext` `TensorProduct.ext` `LinearMap.ext_ring` `smulCommClass_self` `RingHomCompTriple.ids` `LinearMap.ext` `one_smul` `RingHomInvPair.ids`
`pentagon` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SemimoduleCat` `CommSemiring.toSemiring` `CategoryTheory.Category.toCategoryStruct` `SemimoduleCat.moduleCategory` `tensorObj` `whiskerRight` `CategoryTheory.Iso.hom` `associator` `whiskerLeft`	—	`SemimoduleCat.hom_ext` `TensorProduct.ext_fourfold`
`rightUnitor_def` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.rightUnitor` `SemimoduleCat` `CommSemiring.toSemiring` `SemimoduleCat.moduleCategory` `instMonoidalCategoryStruct` `rightUnitor`	—	—
`rightUnitor_hom_apply` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SemimoduleCat` `CommSemiring.toSemiring` `SemimoduleCat.moduleCategory` `instMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `SemimoduleCat.carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SemimoduleCat.isAddCommMonoid` `SemimoduleCat.isModule` `LinearMap.instFunLike` `SemimoduleCat.instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.rightUnitor` `TensorProduct.tmul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`TensorProduct.rid_tmul`
`rightUnitor_inv_apply` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SemimoduleCat` `CommSemiring.toSemiring` `SemimoduleCat.moduleCategory` `instMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `SemimoduleCat.carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SemimoduleCat.isAddCommMonoid` `SemimoduleCat.isModule` `LinearMap.instFunLike` `SemimoduleCat.instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategoryStruct.rightUnitor` `TensorProduct.tmul` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`TensorProduct.rid_symm_apply`
`rightUnitor_naturality` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SemimoduleCat` `CommSemiring.toSemiring` `CategoryTheory.Category.toCategoryStruct` `SemimoduleCat.moduleCategory` `tensorObj` `SemimoduleCat.of` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `tensorHom` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Iso.hom` `TensorProduct` `SemimoduleCat.carrier` `SemimoduleCat.isAddCommMonoid` `SemimoduleCat.isModule` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `rightUnitor`	—	`SemimoduleCat.hom_ext` `TensorProduct.ext` `LinearMap.ext` `smulCommClass_self` `RingHomCompTriple.ids` `LinearMap.ext_ring` `one_smul` `RingHomInvPair.ids`
`tensorHom_comp_tensorHom` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SemimoduleCat` `CommSemiring.toSemiring` `CategoryTheory.Category.toCategoryStruct` `SemimoduleCat.moduleCategory` `tensorObj` `tensorHom`	—	`SemimoduleCat.hom_ext` `TensorProduct.ext` `smulCommClass_self` `RingHomCompTriple.ids`
`tensorHom_def` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.tensorHom` `SemimoduleCat` `CommSemiring.toSemiring` `SemimoduleCat.moduleCategory` `instMonoidalCategoryStruct` `tensorHom`	—	—
`tensorHom_tmul` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SemimoduleCat` `CommSemiring.toSemiring` `SemimoduleCat.moduleCategory` `instMonoidalCategoryStruct` `SemimoduleCat.carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SemimoduleCat.isAddCommMonoid` `SemimoduleCat.isModule` `LinearMap.instFunLike` `SemimoduleCat.instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.MonoidalCategoryStruct.tensorHom` `TensorProduct.tmul`	—	—
`tensorLift_tmul` 📖	mathematical	`SemimoduleCat.carrier` `CommSemiring.toSemiring` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SemimoduleCat.isAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `SemimoduleCat.isModule`	`DFunLike.coe` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SemimoduleCat` `SemimoduleCat.moduleCategory` `instMonoidalCategoryStruct` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `SemimoduleCat.instConcreteCategoryLinearMapIdCarrier` `tensorLift` `TensorProduct.tmul`	—	—
`tensorObj_def` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.tensorObj` `SemimoduleCat` `CommSemiring.toSemiring` `SemimoduleCat.moduleCategory` `instMonoidalCategoryStruct` `tensorObj`	—	—
`tensorUnit_carrier` 📖	mathematical	—	`SemimoduleCat.carrier` `CommSemiring.toSemiring` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `SemimoduleCat` `SemimoduleCat.moduleCategory` `instMonoidalCategoryStruct`	—	—
`tensorUnit_isAddCommMonoid` 📖	mathematical	—	`SemimoduleCat.isAddCommMonoid` `CommSemiring.toSemiring` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `SemimoduleCat` `SemimoduleCat.moduleCategory` `instMonoidalCategoryStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	—
`tensorUnit_isModule` 📖	mathematical	—	`SemimoduleCat.isModule` `CommSemiring.toSemiring` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `SemimoduleCat` `SemimoduleCat.moduleCategory` `instMonoidalCategoryStruct` `Semiring.toModule`	—	—
`tensor_ext` 📖	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `SemimoduleCat.carrier` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SemimoduleCat` `SemimoduleCat.moduleCategory` `instMonoidalCategoryStruct` `SemimoduleCat.isAddCommMonoid` `SemimoduleCat.isModule` `LinearMap.instFunLike` `SemimoduleCat.Hom.hom` `TensorProduct.tmul`	—	—	`SemimoduleCat.hom_ext` `TensorProduct.ext` `LinearMap.ext` `smulCommClass_self` `RingHomCompTriple.ids`
`tensor_ext₃` 📖	—	`DFunLike.coe` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SemimoduleCat` `CommSemiring.toSemiring` `SemimoduleCat.moduleCategory` `instMonoidalCategoryStruct` `SemimoduleCat.carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SemimoduleCat.isAddCommMonoid` `SemimoduleCat.isModule` `LinearMap.instFunLike` `SemimoduleCat.instConcreteCategoryLinearMapIdCarrier` `TensorProduct.tmul`	—	—	`CategoryTheory.cancel_epi` `CategoryTheory.epi_of_strongEpi` `CategoryTheory.strongEpi_of_isIso` `CategoryTheory.Iso.isIso_hom` `tensor_ext₃'`
`tensor_ext₃'` 📖	—	`DFunLike.coe` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SemimoduleCat` `CommSemiring.toSemiring` `SemimoduleCat.moduleCategory` `instMonoidalCategoryStruct` `SemimoduleCat.carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SemimoduleCat.isAddCommMonoid` `SemimoduleCat.isModule` `LinearMap.instFunLike` `SemimoduleCat.instConcreteCategoryLinearMapIdCarrier` `TensorProduct.tmul`	—	—	`SemimoduleCat.hom_ext` `TensorProduct.ext_threefold`
`triangle` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SemimoduleCat` `CommSemiring.toSemiring` `CategoryTheory.Category.toCategoryStruct` `SemimoduleCat.moduleCategory` `tensorObj` `SemimoduleCat.of` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `CategoryTheory.Iso.hom` `associator` `tensorHom` `CategoryTheory.CategoryStruct.id` `TensorProduct` `SemimoduleCat.carrier` `SemimoduleCat.isAddCommMonoid` `SemimoduleCat.isModule` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `leftUnitor` `rightUnitor`	—	`SemimoduleCat.hom_ext` `TensorProduct.ext_threefold` `TensorProduct.tmul_smul` `smulCommClass_self` `TensorProduct.CompatibleSMul.isScalarTower` `IsScalarTower.left`
`whiskerLeft_apply` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SemimoduleCat` `CommSemiring.toSemiring` `SemimoduleCat.moduleCategory` `instMonoidalCategoryStruct` `SemimoduleCat.carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SemimoduleCat.isAddCommMonoid` `SemimoduleCat.isModule` `LinearMap.instFunLike` `SemimoduleCat.instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `TensorProduct.tmul`	—	—
`whiskerLeft_def` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `SemimoduleCat` `CommSemiring.toSemiring` `SemimoduleCat.moduleCategory` `instMonoidalCategoryStruct` `whiskerLeft`	—	—
`whiskerRight_apply` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SemimoduleCat` `CommSemiring.toSemiring` `SemimoduleCat.moduleCategory` `instMonoidalCategoryStruct` `SemimoduleCat.carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SemimoduleCat.isAddCommMonoid` `SemimoduleCat.isModule` `LinearMap.instFunLike` `SemimoduleCat.instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.MonoidalCategoryStruct.whiskerRight` `TensorProduct.tmul`	—	—
`whiskerRight_def` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.whiskerRight` `SemimoduleCat` `CommSemiring.toSemiring` `SemimoduleCat.moduleCategory` `instMonoidalCategoryStruct` `whiskerRight`	—	—

---

← Back to Index