Documentation Verification Report

Matrix

📁 Source: Mathlib/RingTheory/Morita/Matrix.lean

Statistics

Metric	Count
Definitions `counitIso`, `fromMatrixLinear`, `toModuleCat`, `toModuleCatObj`, `unitIso`, `matrixEquivalence`, `toMatrixModCat`, `fromModuleCatToModuleCatLinearEquiv`, `fromModuleCatToModuleCatLinearEquivtoModuleCatObj`, `moritaEquivalenceMatrix`, `toModuleCatFromModuleCatLinearEquiv`	11
Theorems `fromMatrixLinear_apply_coe`, `isScalarTower_toModuleCat`, `mem_toModuleCatObj`, `toModuleCat_map`, `toModuleCat_obj_carrier`, `toModuleCat_obj_isAddCommGroup`, `toModuleCat_obj_isModule`, `matrixEquivalence_counitIso`, `matrixEquivalence_functor`, `matrixEquivalence_inverse`, `matrixEquivalence_unitIso`, `toMatrixModCat_map`, `toMatrixModCat_obj_carrier`, `toMatrixModCat_obj_isAddCommGroup`, `toMatrixModCat_obj_isModule`, `fromModuleCatToModuleCatLinearEquiv_apply`, `fromModuleCatToModuleCatLinearEquiv_symm_apply_coe`, `moritaEquivalenceMatrix_eqv`	18
Total	29

MatrixModCat

Definitions

Name	Category	Theorems
`counitIso` 📖	CompOp	1 math math: `ModuleCat.matrixEquivalence_counitIso`
`fromMatrixLinear` 📖	CompOp	2 math math: `toModuleCat_map`, `fromMatrixLinear_apply_coe`
`toModuleCat` 📖	CompOp	6 math math: `ModuleCat.matrixEquivalence_inverse`, `toModuleCat_obj_carrier`, `ModuleCat.matrixEquivalence_unitIso`, `toModuleCat_map`, `toModuleCat_obj_isAddCommGroup`, `toModuleCat_obj_isModule`
`toModuleCatObj` 📖	CompOp	8 math math: `toModuleCat_obj_carrier`, `mem_toModuleCatObj`, `toModuleCat_map`, `toModuleCat_obj_isAddCommGroup`, `fromModuleCatToModuleCatLinearEquiv_apply`, `fromModuleCatToModuleCatLinearEquiv_symm_apply_coe`, `toModuleCat_obj_isModule`, `fromMatrixLinear_apply_coe`
`unitIso` 📖	CompOp	1 math math: `ModuleCat.matrixEquivalence_unitIso`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fromMatrixLinear_apply_coe` 📖	mathematical	—	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `toModuleCatObj` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule.addCommMonoid` `Submodule.module` `LinearMap.instFunLike` `fromMatrixLinear` `Matrix` `Matrix.semiring`	—	—
`isScalarTower_toModuleCat` 📖	mathematical	—	`IsScalarTower` `Matrix` `ModuleCat.carrier` `Matrix.instRing` `Matrix.smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DistribSMul.toSMulZeroClass` `instDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `ModuleCat.isAddCommGroup` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `ModuleCat.isModule` `Module.compHom` `Matrix.scalar`	—	`SemigroupAction.mul_smul` `Matrix.scalar_apply` `Matrix.smul_eq_diagonal_mul`
`mem_toModuleCatObj` 📖	mathematical	—	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `toModuleCatObj` `Matrix` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `Module.toDistribMulAction` `Matrix.single` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	—
`toModuleCat_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `ModuleCat` `Matrix` `Matrix.instRing` `ModuleCat.moduleCategory` `toModuleCat` `ModuleCat.ofHom` `ModuleCat.carrier` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `SetLike.instMembership` `Submodule.setLike` `toModuleCatObj` `ModuleCat.isModule` `isScalarTower_toModuleCat` `Submodule.addCommGroup` `Submodule.module` `fromMatrixLinear` `ModuleCat.Hom.hom`	—	`isScalarTower_toModuleCat`
`toModuleCat_obj_carrier` 📖	mathematical	—	`ModuleCat.carrier` `CategoryTheory.Functor.obj` `ModuleCat` `Matrix` `Matrix.instRing` `ModuleCat.moduleCategory` `toModuleCat` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `SetLike.instMembership` `Submodule.setLike` `toModuleCatObj` `ModuleCat.isModule` `isScalarTower_toModuleCat`	—	—
`toModuleCat_obj_isAddCommGroup` 📖	mathematical	—	`ModuleCat.isAddCommGroup` `CategoryTheory.Functor.obj` `ModuleCat` `Matrix` `Matrix.instRing` `ModuleCat.moduleCategory` `toModuleCat` `Submodule.addCommGroup` `ModuleCat.carrier` `toModuleCatObj` `ModuleCat.isModule` `isScalarTower_toModuleCat`	—	`isScalarTower_toModuleCat`
`toModuleCat_obj_isModule` 📖	mathematical	—	`ModuleCat.isModule` `CategoryTheory.Functor.obj` `ModuleCat` `Matrix` `Matrix.instRing` `ModuleCat.moduleCategory` `toModuleCat` `Submodule.module` `ModuleCat.carrier` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `toModuleCatObj` `isScalarTower_toModuleCat`	—	`isScalarTower_toModuleCat`

ModuleCat

Definitions

Name	Category	Theorems
`matrixEquivalence` 📖	CompOp	5 math math: `matrixEquivalence_inverse`, `matrixEquivalence_functor`, `matrixEquivalence_unitIso`, `matrixEquivalence_counitIso`, `moritaEquivalenceMatrix_eqv`
`toMatrixModCat` 📖	CompOp	6 math math: `toMatrixModCat_map`, `toMatrixModCat_obj_carrier`, `toMatrixModCat_obj_isAddCommGroup`, `matrixEquivalence_functor`, `matrixEquivalence_unitIso`, `toMatrixModCat_obj_isModule`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`matrixEquivalence_counitIso` 📖	mathematical	—	`CategoryTheory.Equivalence.counitIso` `ModuleCat` `Matrix` `Matrix.instRing` `moduleCategory` `matrixEquivalence` `MatrixModCat.counitIso`	—	—
`matrixEquivalence_functor` 📖	mathematical	—	`CategoryTheory.Equivalence.functor` `ModuleCat` `Matrix` `Matrix.instRing` `moduleCategory` `matrixEquivalence` `toMatrixModCat`	—	—
`matrixEquivalence_inverse` 📖	mathematical	—	`CategoryTheory.Equivalence.inverse` `ModuleCat` `Matrix` `Matrix.instRing` `moduleCategory` `matrixEquivalence` `MatrixModCat.toModuleCat`	—	—
`matrixEquivalence_unitIso` 📖	mathematical	—	`CategoryTheory.Equivalence.unitIso` `ModuleCat` `Matrix` `Matrix.instRing` `moduleCategory` `matrixEquivalence` `CategoryTheory.Iso.symm` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `toMatrixModCat` `MatrixModCat.toModuleCat` `CategoryTheory.Functor.id` `MatrixModCat.unitIso`	—	—
`toMatrixModCat_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `ModuleCat` `moduleCategory` `Matrix` `Matrix.instRing` `toMatrixModCat` `ofHom` `Pi.addCommGroup` `carrier` `isAddCommGroup` `Matrix.Module.matrixModule` `isModule` `LinearMap.mapMatrixModule` `Hom.hom`	—	—
`toMatrixModCat_obj_carrier` 📖	mathematical	—	`carrier` `Matrix` `Matrix.instRing` `CategoryTheory.Functor.obj` `ModuleCat` `moduleCategory` `toMatrixModCat`	—	—
`toMatrixModCat_obj_isAddCommGroup` 📖	mathematical	—	`isAddCommGroup` `Matrix` `Matrix.instRing` `CategoryTheory.Functor.obj` `ModuleCat` `moduleCategory` `toMatrixModCat` `Pi.addCommGroup` `carrier`	—	—
`toMatrixModCat_obj_isModule` 📖	mathematical	—	`isModule` `Matrix` `Matrix.instRing` `CategoryTheory.Functor.obj` `ModuleCat` `moduleCategory` `toMatrixModCat` `Matrix.Module.matrixModule` `carrier` `isAddCommGroup`	—	—

(root)

Definitions

Name	Category	Theorems
`fromModuleCatToModuleCatLinearEquiv` 📖	CompOp	2 math math: `fromModuleCatToModuleCatLinearEquiv_apply`, `fromModuleCatToModuleCatLinearEquiv_symm_apply_coe`
`fromModuleCatToModuleCatLinearEquivtoModuleCatObj` 📖	CompOp	—
`moritaEquivalenceMatrix` 📖	CompOp	1 math math: `moritaEquivalenceMatrix_eqv`
`toModuleCatFromModuleCatLinearEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fromModuleCatToModuleCatLinearEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Submodule` `AddCommGroup.toAddCommMonoid` `Pi.addCommGroup` `Pi.Function.module` `SetLike.instMembership` `Submodule.setLike` `MatrixModCat.toModuleCatObj` `Matrix.Module.matrixModule` `Matrix.Module.instIsScalarTowerForall` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DistribSMul.toSMulZeroClass` `instDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Submodule.addCommMonoid` `Submodule.module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `fromModuleCatToModuleCatLinearEquiv` `Finset.sum` `Finset.univ`	—	`RingHomInvPair.ids` `Matrix.Module.instIsScalarTowerForall` `IsScalarTower.left`
`fromModuleCatToModuleCatLinearEquiv_symm_apply_coe` 📖	mathematical	—	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Pi.addCommGroup` `Pi.Function.module` `SetLike.instMembership` `Submodule.setLike` `MatrixModCat.toModuleCatObj` `Matrix.Module.matrixModule` `DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Matrix.Module.instIsScalarTowerForall` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DistribSMul.toSMulZeroClass` `instDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Submodule.addCommMonoid` `Submodule.module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `fromModuleCatToModuleCatLinearEquiv` `Pi.single` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`RingHomInvPair.ids` `Matrix.Module.instIsScalarTowerForall` `IsScalarTower.left`
`moritaEquivalenceMatrix_eqv` 📖	mathematical	—	`MoritaEquivalence.eqv` `CommRing.toCommSemiring` `Matrix` `Matrix.instRing` `Matrix.instAlgebra` `Ring.toSemiring` `moritaEquivalenceMatrix` `ModuleCat.matrixEquivalence`	—	—

---

← Back to Index