Documentation Verification Report

Adjunctions

📁 Source: Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean

Statistics

Metric	Count
Definitions `embedding`, `embeddingLiftIso`, `ext`, `instLinear`, `instPreadditive`, `liftUnique`, `of`, `categoryFree`, `εIso`, `μIso`, `adj`, `free`, `freeDesc`, `freeHomEquiv`, `freeMk`, `instMonoidalFree`	16
Theorems `embedding_map`, `embedding_obj`, `lift_additive`, `lift_linear`, `lift_map`, `lift_map_single`, `lift_obj`, `single_comp_single`, `εIso_hom_one`, `εIso_inv_freeMk`, `μIso_hom_freeMk_tmul_freeMk`, `μIso_inv_freeMk`, `adj_homEquiv`, `freeDesc_apply`, `freeHomEquiv_apply`, `freeHomEquiv_symm_apply`, `free_hom_ext`, `free_hom_ext_iff`, `free_map_apply`, `free_δ_freeMk`, `free_ε_one`, `free_η_freeMk`, `free_μ_freeMk_tmul_freeMk`, `instIsRightAdjointForgetLinearMapIdCarrier`	24
Total	40

CategoryTheory

Definitions

Name	Category	Theorems
`categoryFree` 📖	CompOp	8 math math: `Free.embedding_obj`, `Free.lift_linear`, `Free.single_comp_single`, `Free.embedding_map`, `Free.lift_obj`, `Free.lift_additive`, `Free.lift_map_single`, `Free.lift_map`

CategoryTheory.Free

Definitions

Name	Category	Theorems
`embedding` 📖	CompOp	2 math math: `embedding_obj`, `embedding_map`
`embeddingLiftIso` 📖	CompOp	—
`ext` 📖	CompOp	—
`instLinear` 📖	CompOp	1 math math: `lift_linear`
`instPreadditive` 📖	CompOp	2 math math: `lift_linear`, `lift_additive`
`liftUnique` 📖	CompOp	—
`of` 📖	CompOp	1 math math: `single_comp_single`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`embedding_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.Free` `CategoryTheory.categoryFree` `embedding` `Finsupp.single` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	—
`embedding_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.Free` `CategoryTheory.categoryFree` `embedding`	—	—
`lift_additive` 📖	mathematical	—	`CategoryTheory.Functor.Additive` `CategoryTheory.Free` `CategoryTheory.categoryFree` `instPreadditive` `lift`	—	`Finsupp.sum_add_index'` `zero_smul` `add_smul`
`lift_linear` 📖	mathematical	—	`CategoryTheory.Functor.Linear` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CategoryTheory.Free` `CategoryTheory.categoryFree` `instPreadditive` `instLinear` `lift`	—	`Finsupp.sum_smul_index` `zero_smul` `SemigroupAction.mul_smul` `Finsupp.smul_sum`
`lift_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.Free` `CategoryTheory.categoryFree` `lift` `Finsupp.sum` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `CategoryTheory.Preadditive.homGroup` `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` `CategoryTheory.Linear.homModule`	—	—
`lift_map_single` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.Free` `CategoryTheory.categoryFree` `lift` `Finsupp.single` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `CategoryTheory.Functor.obj` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `CategoryTheory.Linear.homModule`	—	`Finsupp.sum_single_index` `zero_smul`
`lift_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.Free` `CategoryTheory.categoryFree` `lift`	—	—
`single_comp_single` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Free` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.categoryFree` `of` `Finsupp.single` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`Finsupp.sum_single_index` `MulZeroClass.mul_zero` `Finsupp.single_zero` `MulZeroClass.zero_mul`

ModuleCat

Definitions

Name	Category	Theorems
`adj` 📖	CompOp	1 math math: `adj_homEquiv`
`free` 📖	CompOp	18 math math: `freeHomEquiv_apply`, `PresheafOfModules.free_map_app`, `PresheafOfModules.freeObj_map`, `adj_homEquiv`, `free_ε_one`, `FreeMonoidal.εIso_inv_freeMk`, `PresheafOfModules.freeObj_obj`, `free_η_freeMk`, `free_μ_freeMk_tmul_freeMk`, `FreeMonoidal.μIso_hom_freeMk_tmul_freeMk`, `free_δ_freeMk`, `FreeMonoidal.μIso_inv_freeMk`, `instProjectiveObjFree`, `free_map_apply`, `FreeMonoidal.εIso_hom_one`, `freeHomEquiv_symm_apply`, `freeDesc_apply`, `free_hom_ext_iff`
`freeDesc` 📖	CompOp	4 math math: `PresheafOfModules.freeObj_map`, `freeHomEquiv_symm_apply`, `freeDesc_apply`, `PresheafOfModules.freeObjDesc_app`
`freeHomEquiv` 📖	CompOp	3 math math: `freeHomEquiv_apply`, `adj_homEquiv`, `freeHomEquiv_symm_apply`
`freeMk` 📖	CompOp	16 math math: `freeHomEquiv_apply`, `PresheafOfModules.freeYonedaEquiv_symm_app`, `PresheafOfModules.freeObj_map`, `free_ε_one`, `FreeMonoidal.εIso_inv_freeMk`, `free_η_freeMk`, `PresheafOfModules.freeAdjunctionUnit_app`, `free_μ_freeMk_tmul_freeMk`, `FreeMonoidal.μIso_hom_freeMk_tmul_freeMk`, `PresheafOfModules.Elements.fromFreeYoneda_app_apply`, `free_δ_freeMk`, `FreeMonoidal.μIso_inv_freeMk`, `free_map_apply`, `FreeMonoidal.εIso_hom_one`, `freeDesc_apply`, `free_hom_ext_iff`
`instMonoidalFree` 📖	CompOp	4 math math: `free_ε_one`, `free_η_freeMk`, `free_μ_freeMk_tmul_freeMk`, `free_δ_freeMk`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adj_homEquiv` 📖	mathematical	—	`CategoryTheory.Adjunction.homEquiv` `CategoryTheory.types` `ModuleCat` `moduleCategory` `free` `CategoryTheory.forget` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `carrier` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `LinearMap.instFunLike` `instConcreteCategoryLinearMapIdCarrier` `adj` `freeHomEquiv`	—	`CategoryTheory.Adjunction.mkOfHomEquiv_homEquiv`
`freeDesc_apply` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Functor.obj` `CategoryTheory.types` `ModuleCat` `moduleCategory` `free` `carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `LinearMap.instFunLike` `instConcreteCategoryLinearMapIdCarrier` `freeDesc` `freeMk`	—	`Finsupp.lift_apply` `Finsupp.sum_single_index` `zero_smul` `one_smul`
`freeHomEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `ModuleCat` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `moduleCategory` `CategoryTheory.Functor.obj` `CategoryTheory.types` `free` `EquivLike.toFunLike` `Equiv.instEquivLike` `freeHomEquiv` `carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `LinearMap.instFunLike` `instConcreteCategoryLinearMapIdCarrier` `freeMk`	—	—
`freeHomEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `ModuleCat` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `moduleCategory` `CategoryTheory.Functor.obj` `CategoryTheory.types` `free` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `freeHomEquiv` `freeDesc`	—	—
`free_hom_ext` 📖	—	`DFunLike.coe` `CategoryTheory.Functor.obj` `CategoryTheory.types` `ModuleCat` `moduleCategory` `free` `carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `LinearMap.instFunLike` `instConcreteCategoryLinearMapIdCarrier` `freeMk`	—	—	`hom_ext` `Finsupp.lhom_ext'` `LinearMap.ext_ring` `RingHomCompTriple.ids`
`free_hom_ext_iff` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Functor.obj` `CategoryTheory.types` `ModuleCat` `moduleCategory` `free` `carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `LinearMap.instFunLike` `instConcreteCategoryLinearMapIdCarrier` `freeMk`	—	`free_hom_ext`
`free_map_apply` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Functor.obj` `CategoryTheory.types` `ModuleCat` `moduleCategory` `free` `carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `LinearMap.instFunLike` `instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.Functor.map` `freeMk`	—	`Finsupp.mapDomain_single`
`free_δ_freeMk` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Functor.obj` `CategoryTheory.types` `ModuleCat` `CommRing.toRing` `moduleCategory` `free` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `monoidalCategory` `carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `LinearMap.instFunLike` `instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.Functor.OplaxMonoidal.δ` `CategoryTheory.Functor.Monoidal.toOplaxMonoidal` `instMonoidalFree` `freeMk` `TensorProduct.tmul` `CommRing.toCommSemiring`	—	`FreeMonoidal.μIso_inv_freeMk`
`free_ε_one` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `ModuleCat` `CommRing.toRing` `moduleCategory` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `monoidalCategory` `CategoryTheory.Functor.obj` `CategoryTheory.types` `free` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `LinearMap.instFunLike` `instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.Functor.LaxMonoidal.ε` `CategoryTheory.Functor.Monoidal.toLaxMonoidal` `instMonoidalFree` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `instCommRingCarrierTensorUnit` `freeMk`	—	—
`free_η_freeMk` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Functor.obj` `CategoryTheory.types` `ModuleCat` `CommRing.toRing` `moduleCategory` `free` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `monoidalCategory` `carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `LinearMap.instFunLike` `instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.Functor.OplaxMonoidal.η` `CategoryTheory.Functor.Monoidal.toOplaxMonoidal` `instMonoidalFree` `freeMk` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `instCommRingCarrierTensorUnit`	—	`FreeMonoidal.εIso_inv_freeMk`
`free_μ_freeMk_tmul_freeMk` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `ModuleCat` `CommRing.toRing` `moduleCategory` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `monoidalCategory` `CategoryTheory.Functor.obj` `CategoryTheory.types` `free` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `LinearMap.instFunLike` `instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.Functor.LaxMonoidal.μ` `CategoryTheory.Functor.Monoidal.toLaxMonoidal` `instMonoidalFree` `TensorProduct.tmul` `CommRing.toCommSemiring` `freeMk`	—	`FreeMonoidal.μIso_hom_freeMk_tmul_freeMk`
`instIsRightAdjointForgetLinearMapIdCarrier` 📖	mathematical	—	`CategoryTheory.Functor.IsRightAdjoint` `CategoryTheory.types` `ModuleCat` `moduleCategory` `CategoryTheory.forget` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `carrier` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `LinearMap.instFunLike` `instConcreteCategoryLinearMapIdCarrier`	—	`CategoryTheory.Adjunction.isRightAdjoint`

ModuleCat.FreeMonoidal

Definitions

Name	Category	Theorems
`εIso` 📖	CompOp	2 math math: `εIso_inv_freeMk`, `εIso_hom_one`
`μIso` 📖	CompOp	2 math math: `μIso_hom_freeMk_tmul_freeMk`, `μIso_inv_freeMk`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`εIso_hom_one` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `ModuleCat.MonoidalCategory.instMonoidalCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.types` `ModuleCat.free` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `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` `εIso` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `ModuleCat.freeMk`	—	—
`εIso_inv_freeMk` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Functor.obj` `CategoryTheory.types` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `ModuleCat.free` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `ModuleCat.MonoidalCategory.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` `εIso` `ModuleCat.freeMk` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`Finsupp.lapply_apply` `Finsupp.single_eq_same`
`μIso_hom_freeMk_tmul_freeMk` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `ModuleCat.MonoidalCategory.instMonoidalCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.types` `ModuleCat.free` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `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` `μIso` `TensorProduct.tmul` `CommRing.toCommSemiring` `ModuleCat.freeMk`	—	`RingHomInvPair.ids` `finsuppTensorFinsupp'_single_tmul_single` `mul_one`
`μIso_inv_freeMk` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Functor.obj` `CategoryTheory.types` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `ModuleCat.free` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `ModuleCat.MonoidalCategory.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` `μIso` `ModuleCat.freeMk` `TensorProduct.tmul` `CommRing.toCommSemiring`	—	`RingHomInvPair.ids` `finsuppTensorFinsupp'_symm_single_eq_single_one_tmul`

---

← Back to Index