TensorProduct

📁 Source: Mathlib/RingTheory/Bialgebra/TensorProduct.lean

Statistics

Metric	Count
Definitions lTensor, rTensor, assoc, lid, map, rid, instBialgebra	7
Theorems assoc_symm_tmul, assoc_tmul, assoc_toAlgEquiv, assoc_toCoalgEquiv, coalgebra_rid_eq_algebra_rid_apply, comulAlgHom_def, comul_eq_algHom_toLinearMap, counitAlgHom_def, counit_eq_algHom_toLinearMap, lid_symm_apply, lid_tmul, lid_toAlgEquiv, lid_toCoalgEquiv, map_tmul, map_toAlgHom, map_toCoalgHom, rid_symm_apply, rid_tmul, rid_toAlgEquiv, rid_toCoalgEquiv	20
Total	27

BialgHom

Definitions

Name	Category	Theorems
lTensor 📖	CompOp	2 math math: BialgCat.whiskerLeft_def, HopfAlgCat.whiskerLeft_def
rTensor 📖	CompOp	2 math math: HopfAlgCat.whiskerRight_def, BialgCat.whiskerRight_def

Bialgebra.TensorProduct

Definitions

Name	Category	Theorems
assoc 📖	CompOp	6 math math: BialgCat.associator_def, assoc_tmul, HopfAlgCat.associator_def, assoc_toCoalgEquiv, assoc_symm_tmul, assoc_toAlgEquiv
lid 📖	CompOp	6 math math: lid_toAlgEquiv, lid_toCoalgEquiv, HopfAlgCat.leftUnitor_def, lid_tmul, BialgCat.leftUnitor_def, lid_symm_apply
map 📖	CompOp	5 math math: map_toAlgHom, map_toCoalgHom, BialgCat.tensorHom_def, map_tmul, HopfAlgCat.tensorHom_def
rid 📖	CompOp	6 math math: BialgCat.rightUnitor_def, HopfAlgCat.rightUnitor_def, rid_toAlgEquiv, rid_symm_apply, rid_tmul, rid_toCoalgEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
assoc_symm_tmul 📖	mathematical	—	DFunLike.coe BialgEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toAlgebra TensorProduct.addCommMonoid TensorProduct.leftModule CommSemiring.toSemiring IsScalarTower.to_smulCommClass IsScalarTower.to_smulCommClass' Algebra.TensorProduct.instSemiring Algebra.TensorProduct.leftAlgebra Algebra.TensorProduct.instAlgebra TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction TensorProduct.instCoalgebraStruct Algebra.id IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Coalgebra.toCoalgebraStruct Bialgebra.toCoalgebra TensorProduct.instModule TensorProduct.isScalarTower Algebra.toSMul BialgEquiv.instFunLike BialgEquiv.symm assoc TensorProduct.tmul	—	IsScalarTower.to_smulCommClass' IsScalarTower.to_smulCommClass TensorProduct.smulCommClass_left IsScalarTower.left TensorProduct.isScalarTower
assoc_tmul 📖	mathematical	—	DFunLike.coe BialgEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toAlgebra TensorProduct.addCommMonoid TensorProduct.leftModule CommSemiring.toSemiring IsScalarTower.to_smulCommClass' IsScalarTower.to_smulCommClass Algebra.TensorProduct.instSemiring Algebra.TensorProduct.leftAlgebra Algebra.TensorProduct.instAlgebra TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction TensorProduct.instCoalgebraStruct TensorProduct.instModule TensorProduct.isScalarTower Algebra.toSMul Coalgebra.toCoalgebraStruct Bialgebra.toCoalgebra Algebra.id IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid BialgEquiv.instFunLike assoc TensorProduct.tmul	—	IsScalarTower.to_smulCommClass IsScalarTower.to_smulCommClass' TensorProduct.smulCommClass_left TensorProduct.isScalarTower IsScalarTower.left
assoc_toAlgEquiv 📖	mathematical	—	AlgEquivClass.toAlgEquiv BialgEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toAlgebra TensorProduct.addCommMonoid TensorProduct.leftModule CommSemiring.toSemiring IsScalarTower.to_smulCommClass' IsScalarTower.to_smulCommClass Algebra.TensorProduct.instSemiring Algebra.TensorProduct.leftAlgebra Algebra.TensorProduct.instAlgebra TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction TensorProduct.instCoalgebraStruct TensorProduct.instModule TensorProduct.isScalarTower Algebra.toSMul Coalgebra.toCoalgebraStruct Bialgebra.toCoalgebra Algebra.id IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid BialgEquiv.instEquivLike BialgEquivClass.toAlgEquivClass BialgEquiv.instBialgEquivClass assoc Algebra.TensorProduct.assoc	—	IsScalarTower.to_smulCommClass' IsScalarTower.to_smulCommClass IsScalarTower.left TensorProduct.smulCommClass_left TensorProduct.isScalarTower BialgEquivClass.toAlgEquivClass BialgEquiv.instBialgEquivClass
assoc_toCoalgEquiv 📖	mathematical	—	CoalgEquivClass.toCoalgEquiv BialgEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toAlgebra TensorProduct.addCommMonoid TensorProduct.leftModule CommSemiring.toSemiring IsScalarTower.to_smulCommClass' IsScalarTower.to_smulCommClass Algebra.TensorProduct.instSemiring Algebra.TensorProduct.leftAlgebra Algebra.TensorProduct.instAlgebra TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction TensorProduct.instCoalgebraStruct TensorProduct.instModule TensorProduct.isScalarTower Algebra.toSMul Coalgebra.toCoalgebraStruct Bialgebra.toCoalgebra Algebra.id IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid BialgEquiv.instEquivLike BialgEquivClass.toCoalgEquivClass BialgEquiv.instBialgEquivClass assoc Coalgebra.TensorProduct.assoc	—	IsScalarTower.to_smulCommClass' IsScalarTower.to_smulCommClass TensorProduct.smulCommClass_left TensorProduct.isScalarTower IsScalarTower.left BialgEquivClass.toCoalgEquivClass BialgEquiv.instBialgEquivClass
coalgebra_rid_eq_algebra_rid_apply 📖	mathematical	—	DFunLike.coe CoalgEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule Semiring.toModule TensorProduct.addCommMonoid TensorProduct.leftModule Bialgebra.toAlgebra IsScalarTower.to_smulCommClass TensorProduct.instCoalgebraStruct Coalgebra.toCoalgebraStruct CommSemiring.toCoalgebra Bialgebra.toCoalgebra CoalgEquiv.instFunLike Coalgebra.TensorProduct.rid AlgEquiv Algebra.TensorProduct.instSemiring Algebra.id Algebra.TensorProduct.leftAlgebra IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction AlgEquiv.instFunLike Algebra.TensorProduct.rid	—	IsScalarTower.to_smulCommClass
comulAlgHom_def 📖	mathematical	—	Bialgebra.comulAlgHom TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toAlgebra Algebra.TensorProduct.instSemiring TensorProduct.instBialgebra AlgHom.comp TensorProduct.addCommMonoid TensorProduct.leftModule CommSemiring.toSemiring IsScalarTower.to_smulCommClass' IsScalarTower.to_smulCommClass Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.TensorProduct.leftAlgebra TensorProduct.smulCommClass_left AlgEquiv.toAlgHom Algebra.TensorProduct.tensorTensorTensorComm Algebra.TensorProduct.map TensorProduct.isScalarTower Algebra.toSMul Algebra.TensorProduct.instAlgebra	—	—
comul_eq_algHom_toLinearMap 📖	mathematical	—	CoalgebraStruct.comul TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toAlgebra TensorProduct.addCommMonoid TensorProduct.leftModule CommSemiring.toSemiring IsScalarTower.to_smulCommClass TensorProduct.instCoalgebraStruct Coalgebra.toCoalgebraStruct Bialgebra.toCoalgebra AlgHom.toLinearMap Algebra.TensorProduct.instSemiring Algebra.TensorProduct.leftAlgebra TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.id IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid AlgHom.comp IsScalarTower.to_smulCommClass' AlgEquiv.toAlgHom Algebra.TensorProduct.tensorTensorTensorComm Algebra.TensorProduct.map TensorProduct.isScalarTower Algebra.toSMul Algebra.TensorProduct.instAlgebra Bialgebra.comulAlgHom	—	IsScalarTower.to_smulCommClass
counitAlgHom_def 📖	mathematical	—	Bialgebra.counitAlgHom TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toAlgebra Algebra.TensorProduct.instSemiring TensorProduct.instBialgebra AlgHom.comp CommSemiring.toSemiring Semiring.toModule Algebra.id Algebra.TensorProduct.leftAlgebra IsScalarTower.to_smulCommClass IsScalarTower.right AlgEquiv.toAlgHom Algebra.TensorProduct.rid Algebra.TensorProduct.map	—	—
counit_eq_algHom_toLinearMap 📖	mathematical	—	CoalgebraStruct.counit TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toAlgebra TensorProduct.addCommMonoid TensorProduct.leftModule CommSemiring.toSemiring IsScalarTower.to_smulCommClass TensorProduct.instCoalgebraStruct Coalgebra.toCoalgebraStruct Bialgebra.toCoalgebra AlgHom.toLinearMap Algebra.TensorProduct.instSemiring Algebra.TensorProduct.leftAlgebra Algebra.id AlgHom.comp Semiring.toModule IsScalarTower.right AlgEquiv.toAlgHom Algebra.TensorProduct.rid Algebra.TensorProduct.map Bialgebra.counitAlgHom	—	IsScalarTower.to_smulCommClass
lid_symm_apply 📖	mathematical	—	DFunLike.coe BialgEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule Algebra.toModule Bialgebra.toAlgebra Algebra.TensorProduct.instSemiring Algebra.id Algebra.TensorProduct.instAlgebra Coalgebra.toCoalgebraStruct Bialgebra.toCoalgebra TensorProduct.instCoalgebraStruct IsScalarTower.right CommSemiring.toBialgebra BialgEquiv.instFunLike BialgEquiv.symm lid TensorProduct.tmul AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	IsScalarTower.right
lid_tmul 📖	mathematical	—	DFunLike.coe BialgEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule Algebra.toModule Bialgebra.toAlgebra Algebra.TensorProduct.instSemiring Algebra.id Algebra.TensorProduct.instAlgebra TensorProduct.instCoalgebraStruct IsScalarTower.right Coalgebra.toCoalgebraStruct Bialgebra.toCoalgebra CommSemiring.toBialgebra BialgEquiv.instFunLike lid TensorProduct.tmul Algebra.toSMul	—	IsScalarTower.right
lid_toAlgEquiv 📖	mathematical	—	AlgEquivClass.toAlgEquiv BialgEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule Algebra.toModule Bialgebra.toAlgebra Algebra.TensorProduct.instSemiring Algebra.id Algebra.TensorProduct.instAlgebra TensorProduct.instCoalgebraStruct IsScalarTower.right Coalgebra.toCoalgebraStruct Bialgebra.toCoalgebra CommSemiring.toBialgebra BialgEquiv.instEquivLike BialgEquivClass.toAlgEquivClass BialgEquiv.instBialgEquivClass lid Algebra.TensorProduct.lid	—	IsScalarTower.right BialgEquivClass.toAlgEquivClass BialgEquiv.instBialgEquivClass
lid_toCoalgEquiv 📖	mathematical	—	CoalgEquivClass.toCoalgEquiv BialgEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule Algebra.toModule Bialgebra.toAlgebra Algebra.TensorProduct.instSemiring Algebra.id Algebra.TensorProduct.instAlgebra TensorProduct.instCoalgebraStruct IsScalarTower.right Coalgebra.toCoalgebraStruct Bialgebra.toCoalgebra CommSemiring.toBialgebra TensorProduct.addCommMonoid BialgEquiv.instEquivLike BialgEquivClass.toCoalgEquivClass BialgEquiv.instBialgEquivClass lid Coalgebra.TensorProduct.lid	—	IsScalarTower.right BialgEquivClass.toCoalgEquivClass BialgEquiv.instBialgEquivClass
map_tmul 📖	mathematical	—	DFunLike.coe BialgHom TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toAlgebra Algebra.TensorProduct.instSemiring Algebra.TensorProduct.leftAlgebra IsScalarTower.to_smulCommClass CommSemiring.toSemiring TensorProduct.instCoalgebraStruct Coalgebra.toCoalgebraStruct Bialgebra.toCoalgebra BialgHom.funLike map TensorProduct.tmul	—	IsScalarTower.to_smulCommClass
map_toAlgHom 📖	mathematical	—	AlgHomClass.toAlgHom TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toAlgebra Algebra.TensorProduct.instSemiring Algebra.TensorProduct.leftAlgebra IsScalarTower.to_smulCommClass CommSemiring.toSemiring BialgHom TensorProduct.instCoalgebraStruct Coalgebra.toCoalgebraStruct Bialgebra.toCoalgebra BialgHom.funLike BialgHomClass.toAlgHomClass BialgHom.bialgHomClass map Algebra.TensorProduct.map	—	IsScalarTower.to_smulCommClass BialgHomClass.toAlgHomClass BialgHom.bialgHomClass
map_toCoalgHom 📖	mathematical	—	CoalgHomClass.toCoalgHom TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toAlgebra BialgHom Algebra.TensorProduct.instSemiring Algebra.TensorProduct.leftAlgebra IsScalarTower.to_smulCommClass CommSemiring.toSemiring TensorProduct.instCoalgebraStruct Coalgebra.toCoalgebraStruct Bialgebra.toCoalgebra TensorProduct.addCommMonoid BialgHom.funLike BialgHomClass.toCoalgHomClass BialgHom.bialgHomClass map Coalgebra.TensorProduct.map	—	IsScalarTower.to_smulCommClass BialgHomClass.toCoalgHomClass BialgHom.bialgHomClass
rid_symm_apply 📖	mathematical	—	DFunLike.coe BialgEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule Semiring.toModule Algebra.TensorProduct.instSemiring Algebra.id Bialgebra.toAlgebra Algebra.TensorProduct.leftAlgebra IsScalarTower.to_smulCommClass Coalgebra.toCoalgebraStruct Bialgebra.toCoalgebra TensorProduct.instCoalgebraStruct CommSemiring.toBialgebra BialgEquiv.instFunLike BialgEquiv.symm rid TensorProduct.tmul AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	IsScalarTower.to_smulCommClass
rid_tmul 📖	mathematical	—	DFunLike.coe BialgEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule Semiring.toModule Algebra.TensorProduct.instSemiring Algebra.id Algebra.TensorProduct.leftAlgebra Bialgebra.toAlgebra IsScalarTower.to_smulCommClass TensorProduct.instCoalgebraStruct Coalgebra.toCoalgebraStruct Bialgebra.toCoalgebra CommSemiring.toBialgebra BialgEquiv.instFunLike rid TensorProduct.tmul Algebra.toSMul	—	IsScalarTower.to_smulCommClass
rid_toAlgEquiv 📖	mathematical	—	AlgEquivClass.toAlgEquiv BialgEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule Semiring.toModule Algebra.TensorProduct.instSemiring Algebra.id Algebra.TensorProduct.leftAlgebra Bialgebra.toAlgebra IsScalarTower.to_smulCommClass TensorProduct.instCoalgebraStruct Coalgebra.toCoalgebraStruct Bialgebra.toCoalgebra CommSemiring.toBialgebra BialgEquiv.instEquivLike BialgEquivClass.toAlgEquivClass BialgEquiv.instBialgEquivClass rid Algebra.TensorProduct.rid	—	AlgEquiv.ext IsScalarTower.to_smulCommClass BialgEquivClass.toAlgEquivClass BialgEquiv.instBialgEquivClass coalgebra_rid_eq_algebra_rid_apply
rid_toCoalgEquiv 📖	mathematical	—	CoalgEquivClass.toCoalgEquiv BialgEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule Semiring.toModule Algebra.TensorProduct.instSemiring Algebra.id Algebra.TensorProduct.leftAlgebra Bialgebra.toAlgebra IsScalarTower.to_smulCommClass TensorProduct.instCoalgebraStruct Coalgebra.toCoalgebraStruct Bialgebra.toCoalgebra CommSemiring.toBialgebra TensorProduct.addCommMonoid BialgEquiv.instEquivLike BialgEquivClass.toCoalgEquivClass BialgEquiv.instBialgEquivClass rid Coalgebra.TensorProduct.rid	—	IsScalarTower.to_smulCommClass BialgEquivClass.toCoalgEquivClass BialgEquiv.instBialgEquivClass

TensorProduct

Definitions

Name	Category	Theorems
instBialgebra 📖	CompOp	9 math math: BialgCat.rightUnitor_def, Bialgebra.TensorProduct.counitAlgHom_def, BialgCat.associator_def, BialgCat.whiskerLeft_def, Bialgebra.TensorProduct.comulAlgHom_def, BialgCat.tensorHom_def, BialgCat.whiskerRight_def, BialgCat.tensorObj_def, BialgCat.leftUnitor_def

---

← Back to Index