Documentation Verification Report

Monoidal

📁 Source: Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat/Monoidal.lean

Statistics

Metric	Count
Definitions `instMonoidalCategory`, `tensorHom`, `tensorObj`, `instMonoidalCategoryStruct`	4
Theorems `forget₂_map_associator_hom`, `forget₂_map_associator_inv`, `hom_hom_associator`, `hom_inv_associator`, `tensorObj_form`, `toIsometry_hom_leftUnitor`, `toIsometry_hom_rightUnitor`, `toIsometry_inv_leftUnitor`, `toIsometry_inv_rightUnitor`, `toIsometry_tensorHom`, `toIsometry_whiskerLeft`, `toIsometry_whiskerRight`, `toModuleCat_tensor`	13
Total	17

QuadraticModuleCat

Definitions

Name	Category	Theorems
`instMonoidalCategory` 📖	CompOp	—
`instMonoidalCategoryStruct` 📖	CompOp	12 math math: `forget₂_map_associator_inv`, `forget₂_map_associator_hom`, `toIsometry_whiskerRight`, `toIsometry_tensorHom`, `toIsometry_hom_leftUnitor`, `toIsometry_hom_rightUnitor`, `toIsometry_inv_rightUnitor`, `toModuleCat_tensor`, `toIsometry_whiskerLeft`, `toIsometry_inv_leftUnitor`, `hom_hom_associator`, `hom_inv_associator`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`forget₂_map_associator_hom` 📖	mathematical	—	`CategoryTheory.Functor.map` `QuadraticModuleCat` `category` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `CategoryTheory.forget₂` `QuadraticMap.Isometry` `ModuleCat.carrier` `toModuleCat` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ModuleCat.isModule` `Semiring.toModule` `form` `QuadraticMap.Isometry.instFunLike` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `concreteCategory` `LinearMap` `Ring.toSemiring` `RingHom.id` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `hasForgetToModule` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `instMonoidalCategoryStruct` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.associator` `ModuleCat.MonoidalCategory.instMonoidalCategoryStruct`	—	`Nat.instAtLeastTwoHAddOfNat`
`forget₂_map_associator_inv` 📖	mathematical	—	`CategoryTheory.Functor.map` `QuadraticModuleCat` `category` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `CategoryTheory.forget₂` `QuadraticMap.Isometry` `ModuleCat.carrier` `toModuleCat` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ModuleCat.isModule` `Semiring.toModule` `form` `QuadraticMap.Isometry.instFunLike` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `concreteCategory` `LinearMap` `Ring.toSemiring` `RingHom.id` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `hasForgetToModule` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `instMonoidalCategoryStruct` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategoryStruct.associator` `ModuleCat.MonoidalCategory.instMonoidalCategoryStruct`	—	`Nat.instAtLeastTwoHAddOfNat`
`hom_hom_associator` 📖	mathematical	—	`Hom.toIsometry` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `QuadraticModuleCat` `category` `instMonoidalCategoryStruct` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.associator` `QuadraticMap.IsometryEquiv.toIsometry` `TensorProduct` `CommRing.toCommSemiring` `ModuleCat.carrier` `CommRing.toRing` `toModuleCat` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `TensorProduct.addCommGroup` `TensorProduct.instModule` `TensorProduct.leftModule` `CommSemiring.toSemiring` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `TensorProduct.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `TensorProduct.smulCommClass_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Semiring.toModule` `QuadraticForm.tmul` `Algebra.id` `TensorProduct.isScalarTower` `Algebra.toSMul` `IsScalarTower.left` `form` `QuadraticForm.tensorAssoc`	—	`Nat.instAtLeastTwoHAddOfNat`
`hom_inv_associator` 📖	mathematical	—	`Hom.toIsometry` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `QuadraticModuleCat` `category` `instMonoidalCategoryStruct` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategoryStruct.associator` `QuadraticMap.IsometryEquiv.toIsometry` `TensorProduct` `CommRing.toCommSemiring` `ModuleCat.carrier` `CommRing.toRing` `toModuleCat` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `TensorProduct.addCommGroup` `TensorProduct.leftModule` `CommSemiring.toSemiring` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `TensorProduct.instModule` `TensorProduct.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `TensorProduct.smulCommClass_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Semiring.toModule` `QuadraticForm.tmul` `Algebra.id` `IsScalarTower.left` `form` `TensorProduct.isScalarTower` `Algebra.toSMul` `QuadraticMap.IsometryEquiv.symm` `QuadraticForm.tensorAssoc`	—	`Nat.instAtLeastTwoHAddOfNat`
`toIsometry_hom_leftUnitor` 📖	mathematical	—	`Hom.toIsometry` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `QuadraticModuleCat` `category` `instMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.leftUnitor` `QuadraticMap.IsometryEquiv.toIsometry` `TensorProduct` `CommRing.toCommSemiring` `ModuleCat.carrier` `CommRing.toRing` `toModuleCat` `AddCommGroup.toAddCommMonoid` `Ring.toAddCommGroup` `ModuleCat.isAddCommGroup` `Semiring.toModule` `CommSemiring.toSemiring` `ModuleCat.isModule` `TensorProduct.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `TensorProduct.leftModule` `Algebra.to_smulCommClass` `Algebra.id` `QuadraticForm.tmul` `IsScalarTower.right` `QuadraticMap.sq` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `form` `QuadraticForm.tensorLId`	—	`Nat.instAtLeastTwoHAddOfNat`
`toIsometry_hom_rightUnitor` 📖	mathematical	—	`Hom.toIsometry` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `QuadraticModuleCat` `category` `instMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.rightUnitor` `QuadraticMap.IsometryEquiv.toIsometry` `TensorProduct` `CommRing.toCommSemiring` `ModuleCat.carrier` `CommRing.toRing` `toModuleCat` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `Ring.toAddCommGroup` `ModuleCat.isModule` `Semiring.toModule` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `TensorProduct.leftModule` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `QuadraticForm.tmul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `form` `QuadraticMap.sq` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.to_smulCommClass` `IsScalarTower.right` `QuadraticForm.tensorRId`	—	`Nat.instAtLeastTwoHAddOfNat`
`toIsometry_inv_leftUnitor` 📖	mathematical	—	`Hom.toIsometry` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `QuadraticModuleCat` `category` `instMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategoryStruct.leftUnitor` `QuadraticMap.IsometryEquiv.toIsometry` `ModuleCat.carrier` `CommRing.toRing` `toModuleCat` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Ring.toAddCommGroup` `ModuleCat.isAddCommGroup` `Semiring.toModule` `CommSemiring.toSemiring` `ModuleCat.isModule` `TensorProduct.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `TensorProduct.leftModule` `Algebra.to_smulCommClass` `Algebra.id` `form` `QuadraticForm.tmul` `IsScalarTower.right` `QuadraticMap.sq` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `QuadraticMap.IsometryEquiv.symm` `QuadraticForm.tensorLId`	—	`Nat.instAtLeastTwoHAddOfNat`
`toIsometry_inv_rightUnitor` 📖	mathematical	—	`Hom.toIsometry` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `QuadraticModuleCat` `category` `instMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategoryStruct.rightUnitor` `QuadraticMap.IsometryEquiv.toIsometry` `ModuleCat.carrier` `CommRing.toRing` `toModuleCat` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `Ring.toAddCommGroup` `ModuleCat.isModule` `Semiring.toModule` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `TensorProduct.leftModule` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `form` `QuadraticForm.tmul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `QuadraticMap.sq` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.to_smulCommClass` `IsScalarTower.right` `QuadraticMap.IsometryEquiv.symm` `QuadraticForm.tensorRId`	—	`Nat.instAtLeastTwoHAddOfNat`
`toIsometry_tensorHom` 📖	mathematical	—	`Hom.toIsometry` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `QuadraticModuleCat` `category` `instMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorHom` `QuadraticMap.Isometry.tmul` `ModuleCat.carrier` `CommRing.toRing` `toModuleCat` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `form`	—	`Nat.instAtLeastTwoHAddOfNat`
`toIsometry_whiskerLeft` 📖	mathematical	—	`Hom.toIsometry` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `QuadraticModuleCat` `category` `instMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `QuadraticMap.Isometry.tmul` `ModuleCat.carrier` `CommRing.toRing` `toModuleCat` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `form` `QuadraticMap.Isometry.id` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semiring.toModule`	—	`Nat.instAtLeastTwoHAddOfNat`
`toIsometry_whiskerRight` 📖	mathematical	—	`Hom.toIsometry` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `QuadraticModuleCat` `category` `instMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.whiskerRight` `QuadraticMap.Isometry.tmul` `ModuleCat.carrier` `CommRing.toRing` `toModuleCat` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `form` `QuadraticMap.Isometry.id` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semiring.toModule`	—	`Nat.instAtLeastTwoHAddOfNat`
`toModuleCat_tensor` 📖	mathematical	—	`toModuleCat` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `QuadraticModuleCat` `category` `instMonoidalCategoryStruct` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `ModuleCat.MonoidalCategory.instMonoidalCategoryStruct`	—	`Nat.instAtLeastTwoHAddOfNat`

QuadraticModuleCat.instMonoidalCategory

Definitions

Name	Category	Theorems
`tensorHom` 📖	CompOp	—
`tensorObj` 📖	CompOp	1 math math: `tensorObj_form`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tensorObj_form` 📖	mathematical	—	`QuadraticModuleCat.form` `tensorObj` `QuadraticForm.tmul` `ModuleCat.carrier` `CommRing.toRing` `QuadraticModuleCat.toModuleCat` `ModuleCat.isAddCommGroup` `Algebra.id` `CommRing.toCommSemiring` `ModuleCat.isModule`	—	`Nat.instAtLeastTwoHAddOfNat`

---

← Back to Index