Documentation Verification Report

Closed

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

Statistics

Metric	Count
Definitions `instMonoidalClosed`, `monoidalClosedHomEquiv`	2
Theorems `ihom_coev_app`, `ihom_ev_app`, `ihom_map_apply`, `monoidalClosed_curry`, `monoidalClosed_pre_app`, `monoidalClosed_uncurry`	6
Total	8

ModuleCat

Definitions

Name	Category	Theorems
`instMonoidalClosed` 📖	CompOp	8 math math: `monoidalClosed_uncurry`, `monoidalClosed_curry`, `FGModuleCat.instIsMonoidalClosedModuleCatIsFG`, `FGModuleCat.ihom_obj`, `ihom_map_apply`, `ihom_coev_app`, `monoidalClosed_pre_app`, `ihom_ev_app`
`monoidalClosedHomEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ihom_coev_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `ModuleCat` `CommRing.toRing` `moduleCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.MonoidalCategory.tensorLeft` `monoidalCategory` `CategoryTheory.ihom` `CategoryTheory.MonoidalClosed.closed` `instMonoidalClosed` `CategoryTheory.ihom.coev` `ofHom₂` `CategoryTheory.Functor.obj` `Opposite.unop` `Opposite.op` `LinearMap.flip` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `carrier` `TensorProduct` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `TensorProduct.smulCommClass_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `RingHom.id` `Semiring.toNonAssocSemiring`	—	—
`ihom_ev_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `ModuleCat` `CommRing.toRing` `moduleCategory` `CategoryTheory.Functor.comp` `CategoryTheory.ihom` `monoidalCategory` `CategoryTheory.MonoidalClosed.closed` `instMonoidalClosed` `CategoryTheory.MonoidalCategory.tensorLeft` `CategoryTheory.Functor.id` `CategoryTheory.ihom.ev` `ofHom` `TensorProduct` `CommRing.toCommSemiring` `carrier` `CategoryTheory.Functor.obj` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `TensorProduct.addCommGroup` `TensorProduct.instModule` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `TensorProduct.addCommMonoid` `LinearMap.instSMulCommClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `LinearMap.instFunLike` `TensorProduct.uncurry` `LinearMap.comp` `Ring.toSemiring` `Opposite.unop` `Opposite.op` `Algebra.instModuleCarrier` `Algebra.id` `Algebra.instSMulCommClassCarrier` `RingHomCompTriple.ids` `LinearMap.lcomp` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instAddCommGroupHom` `Hom.instModule` `homLinearEquiv` `LinearMap.flip` `LinearMap.id`	—	`smulCommClass_self` `LinearMap.instSMulCommClass` `Algebra.instSMulCommClassCarrier` `RingHomCompTriple.ids` `RingHomInvPair.ids` `CategoryTheory.MonoidalClosed.uncurry_id_eq_ev` `hom_ext` `TensorProduct.ext'` `monoidalClosed_uncurry`
`ihom_map_apply` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Functor.obj` `ModuleCat` `CommRing.toRing` `moduleCategory` `CategoryTheory.ihom` `monoidalCategory` `CategoryTheory.MonoidalClosed.closed` `instMonoidalClosed` `carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `LinearMap.instFunLike` `instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.Functor.map` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	`smulCommClass_self`
`monoidalClosed_curry` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `CommRing.toRing` `RingHom.id` `Semiring.toNonAssocSemiring` `carrier` `Opposite.unop` `ModuleCat` `Opposite.op` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `LinearMap.instFunLike` `Hom.hom` `CategoryTheory.Functor.obj` `moduleCategory` `CategoryTheory.ihom` `monoidalCategory` `CategoryTheory.MonoidalClosed.closed` `instMonoidalClosed` `CategoryTheory.MonoidalClosed.curry` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `MonoidalCategory.instMonoidalCategoryStruct` `CategoryTheory.ConcreteCategory.hom` `instConcreteCategoryLinearMapIdCarrier` `TensorProduct.tmul` `CommRing.toCommSemiring`	—	—
`monoidalClosed_pre_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `ModuleCat` `CommRing.toRing` `moduleCategory` `CategoryTheory.ihom` `monoidalCategory` `CategoryTheory.MonoidalClosed.closed` `instMonoidalClosed` `CategoryTheory.MonoidalClosed.pre` `ofHom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instAddCommGroupHom` `Hom.instModule` `Ring.toSemiring` `Algebra.instModuleCarrier` `CommRing.toCommSemiring` `Algebra.id` `Algebra.instSMulCommClassCarrier` `LinearMap.comp` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `carrier` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `LinearMap.addCommMonoid` `LinearMap.module` `RingHomCompTriple.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `LinearEquiv.symm` `homLinearEquiv` `LinearMap.lcomp` `Hom.hom`	—	—
`monoidalClosed_uncurry` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `ModuleCat` `CommRing.toRing` `moduleCategory` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `monoidalCategory` `carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `LinearMap.instFunLike` `instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.MonoidalClosed.uncurry` `CategoryTheory.MonoidalClosed.closed` `instMonoidalClosed` `TensorProduct.tmul` `CommRing.toCommSemiring` `Opposite.unop` `Opposite.op` `Hom.hom` `CategoryTheory.Functor.obj` `CategoryTheory.ihom`	—	—

---

← Back to Index