Commit 2025-05-28 21:49 5f7fa5a0

View on Github →

chore(RingTheory/HopfAlgebra): make tensor product heterobasic (#25171) Suppose S is an R-algebra. Given an S-coalgebra A and R-coalgebra B, we generalize the existing construction to give A ⊗[R] B an S-coalgebra structure. Similar generalizations are done for bialgebras and Hopf algebras.

Estimated changes

Modified Mathlib/Algebra/Category/BialgCat/Monoidal.lean

Modified Mathlib/Algebra/Category/CoalgCat/Monoidal.lean

Modified Mathlib/Algebra/Category/HopfAlgCat/Monoidal.lean

Modified Mathlib/RingTheory/Bialgebra/TensorProduct.lean

modified theorem Bialgebra.TensorProduct.assoc_symm_tmul

modified theorem Bialgebra.TensorProduct.assoc_tmul

modified theorem Bialgebra.TensorProduct.lid_symm_apply

modified theorem Bialgebra.TensorProduct.lid_tmul

modified theorem Bialgebra.TensorProduct.map_tmul

modified theorem Bialgebra.TensorProduct.map_toAlgHom

modified theorem Bialgebra.TensorProduct.map_toCoalgHom

modified theorem Bialgebra.TensorProduct.rid_symm_apply

modified theorem Bialgebra.TensorProduct.rid_tmul

Modified Mathlib/RingTheory/Coalgebra/TensorProduct.lean

modified theorem Coalgebra.TensorProduct.map_tmul

modified theorem Coalgebra.TensorProduct.map_toLinearMap

modified theorem Coalgebra.TensorProduct.rid_symm_apply

modified theorem Coalgebra.TensorProduct.rid_tmul

Modified Mathlib/RingTheory/HopfAlgebra/TensorProduct.lean