TensorProduct

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

Statistics

Metric	Count
Definitions lTensor, rTensor, assoc, lid, map, rid, instCoalgebra, instCoalgebraStruct, tacticHopf_tensor_induction_With__	9
Theorems assoc_symm_tmul, assoc_tmul, assoc_toLinearEquiv, lid_symm_apply, lid_tmul, lid_toLinearEquiv, map_tmul, map_toLinearMap, rid_symm_apply, rid_tmul, rid_toLinearEquiv, comul_def, comul_tmul, counit_def, counit_tmul, instIsCocomm	16
Total	25

CoalgHom

Definitions

Name	Category	Theorems
lTensor 📖	CompOp	1 math math: CoalgCat.whiskerLeft_def
rTensor 📖	CompOp	1 math math: CoalgCat.whiskerRight_def

Coalgebra.TensorProduct

Definitions

Name	Category	Theorems
assoc 📖	CompOp	5 math math: CoalgCat.associator_def, assoc_tmul, assoc_symm_tmul, Bialgebra.TensorProduct.assoc_toCoalgEquiv, assoc_toLinearEquiv
lid 📖	CompOp	5 math math: lid_tmul, lid_toLinearEquiv, Bialgebra.TensorProduct.lid_toCoalgEquiv, CoalgCat.leftUnitor_def, lid_symm_apply
map 📖	CompOp	4 math math: Bialgebra.TensorProduct.map_toCoalgHom, CoalgCat.tensorHom_def, map_tmul, map_toLinearMap
rid 📖	CompOp	6 math math: Bialgebra.TensorProduct.coalgebra_rid_eq_algebra_rid_apply, rid_symm_apply, rid_toLinearEquiv, CoalgCat.rightUnitor_def, rid_tmul, Bialgebra.TensorProduct.rid_toCoalgEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
assoc_symm_tmul 📖	mathematical	—	DFunLike.coe CoalgEquiv TensorProduct TensorProduct.addCommMonoid TensorProduct.leftModule CommSemiring.toSemiring IsScalarTower.to_smulCommClass IsScalarTower.to_smulCommClass' TensorProduct.instModule TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction TensorProduct.instCoalgebraStruct Algebra.id IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Coalgebra.toCoalgebraStruct TensorProduct.isScalarTower Algebra.toSMul CoalgEquiv.instFunLike CoalgEquiv.symm assoc TensorProduct.tmul	—	IsScalarTower.to_smulCommClass' IsScalarTower.to_smulCommClass TensorProduct.smulCommClass_left IsScalarTower.left TensorProduct.isScalarTower
assoc_tmul 📖	mathematical	—	DFunLike.coe CoalgEquiv TensorProduct TensorProduct.addCommMonoid TensorProduct.leftModule CommSemiring.toSemiring IsScalarTower.to_smulCommClass' IsScalarTower.to_smulCommClass TensorProduct.instModule TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction TensorProduct.instCoalgebraStruct TensorProduct.isScalarTower Algebra.toSMul Coalgebra.toCoalgebraStruct Algebra.id IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid CoalgEquiv.instFunLike assoc TensorProduct.tmul	—	IsScalarTower.to_smulCommClass IsScalarTower.to_smulCommClass' TensorProduct.smulCommClass_left TensorProduct.isScalarTower IsScalarTower.left
assoc_toLinearEquiv 📖	mathematical	—	SemilinearEquivClass.semilinearEquiv TensorProduct TensorProduct.addCommMonoid TensorProduct.leftModule CommSemiring.toSemiring IsScalarTower.to_smulCommClass' IsScalarTower.to_smulCommClass CoalgEquiv TensorProduct.instModule TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction TensorProduct.instCoalgebraStruct TensorProduct.isScalarTower Algebra.toSMul Coalgebra.toCoalgebraStruct Algebra.id IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids CoalgEquiv.instEquivLike CoalgEquivClass.toSemilinearEquivClass CoalgEquiv.instCoalgEquivClass assoc TensorProduct.AlgebraTensorModule.assoc smulCommClass_self CommSemiring.toCommMonoid CommMonoid.toMonoid	—	RingHomInvPair.ids IsScalarTower.to_smulCommClass' IsScalarTower.to_smulCommClass TensorProduct.smulCommClass_left TensorProduct.isScalarTower IsScalarTower.left CoalgEquivClass.toSemilinearEquivClass CoalgEquiv.instCoalgEquivClass
lid_symm_apply 📖	mathematical	—	DFunLike.coe CoalgEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule TensorProduct.addCommMonoid TensorProduct.instModule Coalgebra.toCoalgebraStruct TensorProduct.instCoalgebraStruct Algebra.id IsScalarTower.right CommSemiring.toCoalgebra CoalgEquiv.instFunLike CoalgEquiv.symm lid TensorProduct.tmul AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	IsScalarTower.right
lid_tmul 📖	mathematical	—	DFunLike.coe CoalgEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule TensorProduct.addCommMonoid TensorProduct.instModule TensorProduct.instCoalgebraStruct Algebra.id IsScalarTower.right Coalgebra.toCoalgebraStruct CommSemiring.toCoalgebra CoalgEquiv.instFunLike lid TensorProduct.tmul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	IsScalarTower.right
lid_toLinearEquiv 📖	mathematical	—	SemilinearEquivClass.semilinearEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule CoalgEquiv TensorProduct.addCommMonoid TensorProduct.instModule TensorProduct.instCoalgebraStruct Algebra.id IsScalarTower.right Coalgebra.toCoalgebraStruct CommSemiring.toCoalgebra RingHom.id RingHomInvPair.ids CoalgEquiv.instEquivLike CoalgEquivClass.toSemilinearEquivClass CoalgEquiv.instCoalgEquivClass lid TensorProduct.lid	—	RingHomInvPair.ids IsScalarTower.right CoalgEquivClass.toSemilinearEquivClass CoalgEquiv.instCoalgEquivClass
map_tmul 📖	mathematical	—	DFunLike.coe CoalgHom TensorProduct TensorProduct.addCommMonoid TensorProduct.leftModule CommSemiring.toSemiring IsScalarTower.to_smulCommClass TensorProduct.instCoalgebraStruct Coalgebra.toCoalgebraStruct CoalgHom.funLike map TensorProduct.tmul	—	IsScalarTower.to_smulCommClass
map_toLinearMap 📖	mathematical	—	SemilinearMapClass.semilinearMap TensorProduct CoalgHom TensorProduct.addCommMonoid TensorProduct.leftModule CommSemiring.toSemiring IsScalarTower.to_smulCommClass TensorProduct.instCoalgebraStruct Coalgebra.toCoalgebraStruct RingHom.id Semiring.toNonAssocSemiring map CoalgHom.funLike CoalgHomClass.toSemilinearMapClass CoalgHom.coalgHomClass TensorProduct.AlgebraTensorModule.map	—	IsScalarTower.to_smulCommClass CoalgHomClass.toSemilinearMapClass CoalgHom.coalgHomClass
rid_symm_apply 📖	mathematical	—	DFunLike.coe CoalgEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule TensorProduct.addCommMonoid TensorProduct.leftModule IsScalarTower.to_smulCommClass Coalgebra.toCoalgebraStruct TensorProduct.instCoalgebraStruct CommSemiring.toCoalgebra CoalgEquiv.instFunLike CoalgEquiv.symm rid TensorProduct.tmul AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	IsScalarTower.to_smulCommClass
rid_tmul 📖	mathematical	—	DFunLike.coe CoalgEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule TensorProduct.addCommMonoid TensorProduct.leftModule IsScalarTower.to_smulCommClass TensorProduct.instCoalgebraStruct Coalgebra.toCoalgebraStruct CommSemiring.toCoalgebra CoalgEquiv.instFunLike rid TensorProduct.tmul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	IsScalarTower.to_smulCommClass
rid_toLinearEquiv 📖	mathematical	—	SemilinearEquivClass.semilinearEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule CoalgEquiv TensorProduct.addCommMonoid TensorProduct.leftModule IsScalarTower.to_smulCommClass TensorProduct.instCoalgebraStruct Coalgebra.toCoalgebraStruct CommSemiring.toCoalgebra RingHom.id RingHomInvPair.ids CoalgEquiv.instEquivLike CoalgEquivClass.toSemilinearEquivClass CoalgEquiv.instCoalgEquivClass rid TensorProduct.AlgebraTensorModule.rid	—	RingHomInvPair.ids IsScalarTower.to_smulCommClass CoalgEquivClass.toSemilinearEquivClass CoalgEquiv.instCoalgEquivClass

TensorProduct

Definitions

Name	Category	Theorems
instCoalgebra 📖	CompOp	8 math math: CoalgCat.tensorHom_def, CoalgCat.associator_def, CoalgCat.whiskerRight_def, instIsCocomm, CoalgCat.whiskerLeft_def, CoalgCat.rightUnitor_def, CoalgCat.tensorObj_instCoalgebra, CoalgCat.leftUnitor_def
instCoalgebraStruct 📖	CompOp	40 math math: Bialgebra.TensorProduct.map_toAlgHom, CoalgCat.MonoidalCategoryAux.counit_tensorObj_tensorObj_right, Bialgebra.TensorProduct.comul_eq_algHom_toLinearMap, Bialgebra.TensorProduct.map_toCoalgHom, Bialgebra.TensorProduct.counit_eq_algHom_toLinearMap, Coalgebra.TensorProduct.lid_tmul, CoalgCat.MonoidalCategoryAux.comul_tensorObj_tensorObj_left, Bialgebra.TensorProduct.assoc_tmul, counit_tmul, Coalgebra.TensorProduct.map_tmul, Bialgebra.TensorProduct.rid_toAlgEquiv, Bialgebra.TensorProduct.map_tmul, CoalgCat.MonoidalCategoryAux.counit_tensorObj, Bialgebra.TensorProduct.coalgebra_rid_eq_algebra_rid_apply, CoalgCat.MonoidalCategoryAux.counit_tensorObj_tensorObj_left, counit_def, CoalgCat.MonoidalCategoryAux.comul_tensorObj_tensorObj_right, Bialgebra.TensorProduct.lid_toAlgEquiv, Coalgebra.TensorProduct.assoc_tmul, comul_tmul, comul_def, Coalgebra.TensorProduct.lid_toLinearEquiv, Coalgebra.TensorProduct.assoc_symm_tmul, map_convMul_map, CoalgCat.MonoidalCategoryAux.comul_tensorObj, Bialgebra.TensorProduct.assoc_toCoalgEquiv, Coalgebra.TensorProduct.rid_symm_apply, Bialgebra.TensorProduct.lid_toCoalgEquiv, Coalgebra.TensorProduct.rid_toLinearEquiv, Bialgebra.TensorProduct.rid_symm_apply, Coalgebra.TensorProduct.rid_tmul, Bialgebra.TensorProduct.rid_tmul, Bialgebra.TensorProduct.lid_tmul, Coalgebra.TensorProduct.map_toLinearMap, Bialgebra.TensorProduct.lid_symm_apply, Bialgebra.TensorProduct.rid_toCoalgEquiv, Coalgebra.TensorProduct.assoc_toLinearEquiv, Bialgebra.TensorProduct.assoc_symm_tmul, Bialgebra.TensorProduct.assoc_toAlgEquiv, Coalgebra.TensorProduct.lid_symm_apply
tacticHopf_tensor_induction_With__ 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comul_def 📖	mathematical	—	CoalgebraStruct.comul TensorProduct addCommMonoid leftModule CommSemiring.toSemiring IsScalarTower.to_smulCommClass instCoalgebraStruct LinearMap.comp IsScalarTower.to_smulCommClass' instModule isScalarTower MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.toSMul RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids Algebra.id IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid smulCommClass_left AlgebraTensorModule.tensorTensorTensorComm AlgebraTensorModule.map	—	IsScalarTower.to_smulCommClass
comul_tmul 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct addCommMonoid leftModule IsScalarTower.to_smulCommClass instModule LinearMap.instFunLike CoalgebraStruct.comul instCoalgebraStruct tmul LinearEquiv RingHomInvPair.ids IsScalarTower.to_smulCommClass' Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction smulCommClass_left EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv AlgebraTensorModule.tensorTensorTensorComm	—	IsScalarTower.to_smulCommClass
counit_def 📖	mathematical	—	CoalgebraStruct.counit TensorProduct addCommMonoid leftModule CommSemiring.toSemiring IsScalarTower.to_smulCommClass instCoalgebraStruct LinearMap.comp NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Semiring.toModule IsScalarTower.right RingHom.id RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids AlgebraTensorModule.rid AlgebraTensorModule.map	—	IsScalarTower.to_smulCommClass
counit_tmul 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring leftModule IsScalarTower.to_smulCommClass Semiring.toModule LinearMap.instFunLike CoalgebraStruct.counit instCoalgebraStruct tmul Algebra.toSMul	—	IsScalarTower.to_smulCommClass
instIsCocomm 📖	mathematical	—	Coalgebra.IsCocomm TensorProduct addCommMonoid leftModule CommSemiring.toSemiring IsScalarTower.to_smulCommClass instCoalgebra	—	IsScalarTower.to_smulCommClass AlgebraTensorModule.curry_injective smulCommClass_left IsScalarTower.to_smulCommClass' isScalarTower isScalarTower_left RingHomCompTriple.ids RingHomInvPair.ids LinearMap.ext IsScalarTower.left Coalgebra.comm_comul induction_on zero_tmul LinearEquiv.map_zero tmul_zero tmul_add LinearEquiv.map_add add_tmul

---

← Back to Index