Documentation Verification Report

Module

📁 Source: Mathlib/CategoryTheory/Monoidal/Internal/Module.lean

Statistics

Metric	Count
Definitions `Algebra_of_Mon_`, `toRing`, `functor`, `inverse`, `inverseObj`, `monModuleEquivalenceAlgebra`, `monModuleEquivalenceAlgebraForget`	7
Theorems `algebraMap`, `functor_map_hom_apply`, `functor_obj_carrier`, `inverseObj_mul`, `inverseObj_one`, `inverse_map_hom`, `inverse_obj_X_carrier`, `inverse_obj_X_isAddCommGroup`, `inverse_obj_X_isModule`, `inverse_obj_mon`	10
Total	17

ModuleCat

Definitions

Name	Category	Theorems
`monModuleEquivalenceAlgebra` 📖	CompOp	—
`monModuleEquivalenceAlgebraForget` 📖	CompOp	—

ModuleCat.MonModuleEquivalenceAlgebra

Definitions

Name	Category	Theorems
`Algebra_of_Mon_` 📖	CompOp	2 math math: `functor_map_hom_apply`, `algebraMap`
`functor` 📖	CompOp	2 math math: `functor_map_hom_apply`, `functor_obj_carrier`
`inverse` 📖	CompOp	5 math math: `inverse_obj_mon`, `inverse_obj_X_isAddCommGroup`, `inverse_obj_X_carrier`, `inverse_map_hom`, `inverse_obj_X_isModule`
`inverseObj` 📖	CompOp	4 math math: `inverse_obj_mon`, `inverseObj_mul`, `inverse_map_hom`, `inverseObj_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMap` 📖	mathematical	—	`DFunLike.coe` `RingHom` `ModuleCat.carrier` `CommRing.toRing` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ring.toSemiring` `MonObj.toRing` `RingHom.instFunLike` `algebraMap` `Algebra_of_Mon_` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `ModuleCat` `ModuleCat.moduleCategory` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `ModuleCat.monoidalCategory` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `RingHom.id` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.MonObj.one`	—	—
`functor_map_hom_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `ModuleCat.carrier` `CommRing.toRing` `CategoryTheory.Mon.X` `ModuleCat` `ModuleCat.moduleCategory` `ModuleCat.monoidalCategory` `CommRing.toCommSemiring` `Ring.toSemiring` `MonObj.toRing` `CategoryTheory.Mon.mon` `Algebra_of_Mon_` `AlgHom.funLike` `AlgCat.Hom.hom` `AlgCat.of` `CategoryTheory.Functor.map` `CategoryTheory.Mon` `CategoryTheory.Mon.instCategory` `AlgCat` `AlgCat.instCategory` `functor` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `CategoryTheory.ConcreteCategory.hom` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.Mon.Hom.hom`	—	—
`functor_obj_carrier` 📖	mathematical	—	`AlgCat.carrier` `CategoryTheory.Functor.obj` `CategoryTheory.Mon` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `ModuleCat.monoidalCategory` `CategoryTheory.Mon.instCategory` `AlgCat` `AlgCat.instCategory` `functor` `ModuleCat.carrier` `CategoryTheory.Mon.X`	—	—
`inverseObj_mul` 📖	mathematical	—	`CategoryTheory.MonObj.mul` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `ModuleCat.monoidalCategory` `ModuleCat.of` `AlgCat.carrier` `Ring.toAddCommGroup` `AlgCat.isRing` `Algebra.toModule` `CommRing.toCommSemiring` `Ring.toSemiring` `AlgCat.isAlgebra` `inverseObj` `ModuleCat.ofHom` `TensorProduct` `ModuleCat.carrier` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `TensorProduct.addCommGroup` `TensorProduct.instModule` `LinearMap.mul'` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	—
`inverseObj_one` 📖	mathematical	—	`CategoryTheory.MonObj.one` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `ModuleCat.monoidalCategory` `ModuleCat.of` `AlgCat.carrier` `Ring.toAddCommGroup` `AlgCat.isRing` `Algebra.toModule` `CommRing.toCommSemiring` `Ring.toSemiring` `AlgCat.isAlgebra` `inverseObj` `ModuleCat.ofHom` `Semiring.toModule` `Algebra.linearMap`	—	—
`inverse_map_hom` 📖	mathematical	—	`CategoryTheory.Mon.Hom.hom` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `ModuleCat.monoidalCategory` `ModuleCat.of` `AlgCat.carrier` `Ring.toAddCommGroup` `AlgCat.isRing` `Algebra.toModule` `CommRing.toCommSemiring` `Ring.toSemiring` `AlgCat.isAlgebra` `inverseObj` `CategoryTheory.Functor.map` `AlgCat` `AlgCat.instCategory` `CategoryTheory.Mon` `CategoryTheory.Mon.instCategory` `inverse` `ModuleCat.ofHom` `AlgHom.toLinearMap` `AlgCat.Hom.hom`	—	—
`inverse_obj_X_carrier` 📖	mathematical	—	`ModuleCat.carrier` `CommRing.toRing` `CategoryTheory.Mon.X` `ModuleCat` `ModuleCat.moduleCategory` `ModuleCat.monoidalCategory` `CategoryTheory.Functor.obj` `AlgCat` `AlgCat.instCategory` `CategoryTheory.Mon` `CategoryTheory.Mon.instCategory` `inverse` `AlgCat.carrier`	—	—
`inverse_obj_X_isAddCommGroup` 📖	mathematical	—	`ModuleCat.isAddCommGroup` `CommRing.toRing` `CategoryTheory.Mon.X` `ModuleCat` `ModuleCat.moduleCategory` `ModuleCat.monoidalCategory` `CategoryTheory.Functor.obj` `AlgCat` `AlgCat.instCategory` `CategoryTheory.Mon` `CategoryTheory.Mon.instCategory` `inverse` `Ring.toAddCommGroup` `AlgCat.carrier` `AlgCat.isRing`	—	—
`inverse_obj_X_isModule` 📖	mathematical	—	`ModuleCat.isModule` `CommRing.toRing` `CategoryTheory.Mon.X` `ModuleCat` `ModuleCat.moduleCategory` `ModuleCat.monoidalCategory` `CategoryTheory.Functor.obj` `AlgCat` `AlgCat.instCategory` `CategoryTheory.Mon` `CategoryTheory.Mon.instCategory` `inverse` `Algebra.toModule` `AlgCat.carrier` `CommRing.toCommSemiring` `Ring.toSemiring` `AlgCat.isRing` `AlgCat.isAlgebra`	—	—
`inverse_obj_mon` 📖	mathematical	—	`CategoryTheory.Mon.mon` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `ModuleCat.monoidalCategory` `CategoryTheory.Functor.obj` `AlgCat` `AlgCat.instCategory` `CategoryTheory.Mon` `CategoryTheory.Mon.instCategory` `inverse` `inverseObj`	—	—

ModuleCat.MonModuleEquivalenceAlgebra.MonObj

Definitions

Name	Category	Theorems
`toRing` 📖	CompOp	2 math math: `ModuleCat.MonModuleEquivalenceAlgebra.functor_map_hom_apply`, `ModuleCat.MonModuleEquivalenceAlgebra.algebraMap`

---

← Back to Index