Structures · Algebra
Bialgebra
A bialgebra over a commutative (semi)ring R is both an algebra and a coalgebra over R, such
that the counit and comultiplication are algebra morphisms.
- Defined in
- Mathlib.RingTheory.Bialgebra.Basic
- Shape
- 2 explicit arguments · adds counit_one, mul_compr₂_counit, comul_one, mul_compr₂_comul
Extends2
Extended by1
Concrete types that are instances1
- CommRingCat.carrier
How is a type an instance?
Loading the hierarchy index…
Assumed by223
- Bialgebra.counitAlgHom
- Bialgebra.comulAlgHom
- CommBialgCat.of
- BialgCat.of
- BialgHom.ofAlgHom
- Bialgebra.TensorProduct.map
- BialgEquiv.toBialgIso
- Bialgebra.mulBialgHom
- Bialgebra.TensorProduct.rid
- Bialgebra.comul_one
- Bialgebra.TensorProduct.assoc
- Bialgebra.TensorProduct.lid
- Bialgebra.counit_one
- BialgCat.ofHom
- AddMonoidAlgebra.isGroupLikeElem_single_one
- Coalgebra.Repr.tmul
- Bialgebra.counitBialgHom
- Coalgebra.Repr.mul
- Bialgebra.comulAlgHom_apply
- MonoidAlgebra.isGroupLikeElem_single_one
- AddMonoidAlgebra.bialgHom_ext
- BialgEquiv.ofAlgEquiv
- Bialgebra.mulCoalgHom
- MonoidAlgebra.toAdditiveBialgEquiv
- MonoidAlgebra.bialgHom_ext
- Bialgebra.counitAlgHom_apply
- Bialgebra.comulBialgHom
- AddMonoidAlgebra.toMultiplicativeBialgEquiv
- Bialgebra.Quotient.comulAlgHom
- Bialgebra.comul_mul
- AddMonoidAlgebra.domCongrBialgEquiv
- AlgHom.convMul_apply
- AlgHom.toLinearMap_convMul
- isGroupLikeElem_unitsInv
- BialgEquiv.ofAlgEquiv_apply
- Bialgebra.counit_algebraMap
- MonoidAlgebra.domCongrBialgEquiv
- BialgHom.rTensor
- BialgHom.lTensor
- CommBialgCat.isoEquivBialgEquiv
- BialgEquiv.ofBijective
- IsGroupLikeElem.of_mul_eq_one
- Bialgebra.Quotient.counitAlgHom
- Bialgebra.counit_mul
- Coalgebra.Repr.mul_left
- GroupLike.valMonoidHom
- isGroupLikeElem_iff_of_mul_eq_one
- Bialgebra.TensorProduct.comm
- Bialgebra.unitBialgHom
- Coalgebra.Repr.tmul_left