Documentation Verification Report

Adjunction

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

Statistics

Metric	Count
Definitions `instLaxMonoidalRestrictScalars`, `instMonoidalExtendScalars`	2
Theorems `extendScalars_δ`, `extendScalars_δ_tmul`, `extendScalars_ε`, `extendScalars_η`, `extendScalars_μ`, `extendsScalars_map_leftUnitor_inv_one_tmul`, `extendsScalars_map_rightUnitor_inv_one_tmul`, `restrictScalars_η`, `restrictScalars_μ_tmul`	9
Total	11

ModuleCat

Definitions

Name	Category	Theorems
`instLaxMonoidalRestrictScalars` 📖	CompOp	2 math math: `restrictScalars_η`, `restrictScalars_μ_tmul`
`instMonoidalExtendScalars` 📖	CompOp	5 math math: `extendScalars_δ_tmul`, `extendScalars_η`, `extendScalars_δ`, `extendScalars_ε`, `extendScalars_μ`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`extendScalars_δ` 📖	mathematical	—	`CategoryTheory.Functor.OplaxMonoidal.δ` `ModuleCat` `CommRing.toRing` `moduleCategory` `monoidalCategory` `extendScalars` `CategoryTheory.Functor.Monoidal.toOplaxMonoidal` `instMonoidalExtendScalars` `ofHom` `TensorProduct` `CommRing.toCommSemiring` `carrier` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `Algebra.toModule` `RingHom.toAlgebra` `TensorProduct.instModule` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `TensorProduct.addCommGroup` `Ring.toAddCommGroup` `LinearEquiv.toLinearMap` `Ring.toSemiring` `RingHom.id` `TensorProduct.AlgebraTensorModule.distribBaseChange`	—	—
`extendScalars_δ_tmul` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `CommRing.toRing` `RingHom.id` `Semiring.toNonAssocSemiring` `carrier` `CategoryTheory.Functor.obj` `ModuleCat` `moduleCategory` `extendScalars` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `monoidalCategory` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `CategoryTheory.ConcreteCategory.hom` `LinearMap.instFunLike` `instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.Functor.OplaxMonoidal.δ` `CategoryTheory.Functor.Monoidal.toOplaxMonoidal` `instMonoidalExtendScalars` `TensorProduct.tmul` `CommRing.toCommSemiring` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `TensorProduct.addCommMonoid` `Algebra.toModule` `CommSemiring.toSemiring` `RingHom.toAlgebra` `TensorProduct.instModule` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass`	—	—
`extendScalars_ε` 📖	mathematical	—	`CategoryTheory.Functor.LaxMonoidal.ε` `ModuleCat` `CommRing.toRing` `moduleCategory` `monoidalCategory` `extendScalars` `CategoryTheory.Functor.Monoidal.toLaxMonoidal` `instMonoidalExtendScalars` `ofHom` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Algebra.toModule` `RingHom.toAlgebra` `Semiring.toModule` `Ring.toAddCommGroup` `TensorProduct.addCommGroup` `TensorProduct.leftModule` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `LinearEquiv.toLinearMap` `Ring.toSemiring` `RingHom.id` `AddCommGroup.toAddCommMonoid` `LinearEquiv.symm` `TensorProduct.AlgebraTensorModule.rid`	—	—
`extendScalars_η` 📖	mathematical	—	`CategoryTheory.Functor.OplaxMonoidal.η` `ModuleCat` `CommRing.toRing` `moduleCategory` `monoidalCategory` `extendScalars` `CategoryTheory.Functor.Monoidal.toOplaxMonoidal` `instMonoidalExtendScalars` `ofHom` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Algebra.toModule` `RingHom.toAlgebra` `Semiring.toModule` `TensorProduct.addCommGroup` `Ring.toAddCommGroup` `TensorProduct.leftModule` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `LinearEquiv.toLinearMap` `Ring.toSemiring` `RingHom.id` `AddCommGroup.toAddCommMonoid` `TensorProduct.AlgebraTensorModule.rid`	—	—
`extendScalars_μ` 📖	mathematical	—	`CategoryTheory.Functor.LaxMonoidal.μ` `ModuleCat` `CommRing.toRing` `moduleCategory` `monoidalCategory` `extendScalars` `CategoryTheory.Functor.Monoidal.toLaxMonoidal` `instMonoidalExtendScalars` `ofHom` `TensorProduct` `CommRing.toCommSemiring` `carrier` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `Algebra.toModule` `RingHom.toAlgebra` `isModule` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `TensorProduct.instModule` `TensorProduct.addCommGroup` `Ring.toAddCommGroup` `LinearEquiv.toLinearMap` `Ring.toSemiring` `RingHom.id` `LinearEquiv.symm` `TensorProduct.AlgebraTensorModule.distribBaseChange`	—	—
`extendsScalars_map_leftUnitor_inv_one_tmul` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Functor.obj` `ModuleCat` `CommRing.toRing` `moduleCategory` `extendScalars` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `MonoidalCategory.instMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `LinearMap.instFunLike` `instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.Functor.map` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategoryStruct.leftUnitor` `TensorProduct.tmul` `CommRing.toCommSemiring` `restrictScalars` `of` `Ring.toAddCommGroup` `Semiring.toModule` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `TensorProduct.addCommMonoid` `Algebra.toModule` `CommSemiring.toSemiring` `RingHom.toAlgebra`	—	—
`extendsScalars_map_rightUnitor_inv_one_tmul` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Functor.obj` `ModuleCat` `CommRing.toRing` `moduleCategory` `extendScalars` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `MonoidalCategory.instMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `LinearMap.instFunLike` `instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.Functor.map` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategoryStruct.rightUnitor` `TensorProduct.tmul` `CommRing.toCommSemiring` `restrictScalars` `of` `Ring.toAddCommGroup` `Semiring.toModule` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `TensorProduct.addCommMonoid` `Algebra.toModule` `CommSemiring.toSemiring` `RingHom.toAlgebra`	—	—
`restrictScalars_η` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `ModuleCat` `CommRing.toRing` `moduleCategory` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `monoidalCategory` `CategoryTheory.Functor.obj` `restrictScalars` `carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `LinearMap.instFunLike` `instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.Functor.LaxMonoidal.ε` `instLaxMonoidalRestrictScalars` `RingHom` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike`	—	`extendRestrictScalarsAdj_homEquiv_apply` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `extendScalars_η` `RingHomInvPair.ids` `TensorProduct.AlgebraTensorModule.rid_tmul` `RingHom.smul_toAlgebra` `mul_one`
`restrictScalars_μ_tmul` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `CommRing.toRing` `RingHom.id` `Semiring.toNonAssocSemiring` `carrier` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `ModuleCat` `moduleCategory` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `monoidalCategory` `CategoryTheory.Functor.obj` `restrictScalars` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `CategoryTheory.ConcreteCategory.hom` `LinearMap.instFunLike` `instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.Functor.LaxMonoidal.μ` `instLaxMonoidalRestrictScalars` `TensorProduct.tmul` `CommRing.toCommSemiring`	—	`extendRestrictScalarsAdj_homEquiv_apply` `Algebra.to_smulCommClass` `extendScalars_δ_tmul` `MonoidalCategory.tensorHom_tmul` `extendRestrictScalarsAdj_counit_app_apply_one_tmul`

---

← Back to Index