Structures · Algebra
HopfAlgebra
A Hopf algebra over a commutative (semi)ring R is a bialgebra over R equipped with an
R-linear endomorphism antipode satisfying the antipode axioms.
- Defined in
- Mathlib.RingTheory.HopfAlgebra.Basic
- Shape
- 2 explicit arguments · adds mul_antipode_rTensor_comul, mul_antipode_lTensor_comul
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- CommRingCat.carrier
How is a type an instance?
Loading the hierarchy index…
Assumed by79
- HopfAlgCat.of
- BialgEquiv.toHopfAlgIso
- HopfAlgCat.ofHom
- HopfAlgebra.antipodeAlgHom
- AddMonoidAlgebra.antipode_single
- HopfAlgebra.sum_antipode_mul_eq_algebraMap_counit
- GroupLike.toUnits
- HopfAlgebra.sum_mul_antipode_eq_algebraMap_counit
- HopfAlgebra.antipode_mul_antidistrib
- HopfAlgebra.mul_antipode_rTensor_comul_apply
- IsGroupLikeElem.antipode_mul_cancel
- HopfAlgebra.mul_antipode_lTensor_comul
- CommHopfAlgCat.isoEquivBialgEquiv
- HopfAlgebra.mul_antipode_rTensor_comul
- HopfAlgebra.mul_antipode_lTensor_comul_apply
- HopfAlgebra.antipode_comp_mul_comp_comm
- HopfAlgebra.antipodeAlgHomOp
- IsGroupLikeElem.antipode
- HopfAlgebra.counit_antipode
- LinearMap.id_mul_antipode
- IsGroupLikeElem.mul_antipode_cancel
- HopfAlgebra.antipode_one
- LinearMap.antipode_mul_id
- HopfAlgebra.counit_comp_antipode
- HopfAlgebra.sum_mul_antipode_eq_smul
- LaurentPolynomial.antipode_C
- CommHopfAlgCat.coe_of
- BialgEquiv.toHopfAlgIso_hom
- GroupLike.val_inv
- LinearMap.convOne_comp_coalgHom
- AlgHom.antipode_id_cancel
- BialgEquiv.toHopfAlgIso_symm
- LaurentPolynomial.antipode_T
- MonoidAlgebra.antipode_single
- CommAlgCat.grpObjOpOf
- CommAlgCat.inv_op_of_unop_hom
- HopfAlgebra.Quotient.instQuotientIdeal
- HopfAlgebra.toLinearMap_antipodeAlgHom
- LinearMap.algHom_comp_convOne
- GroupLike.val_toUnits_apply
- CommHopfAlgCat.isoEquivBialgEquiv_apply
- CommHopfAlgCat.ofHom_comp
- AlgHom.counitAlgHom_comp_antipodeAlgHom
- HopfAlgebra.antipode_mul_distrib
- CommHopfAlgCat.isoEquivBialgEquiv_symm_apply
- AddMonoidAlgebra.instHopfAlgebra
- IsGroupLikeElem.isUnit
- HopfAlgebra.sum_antipode_mul_eq_smul
- CommHopfAlgCat.ofHom_apply
- HopfAlgCat.of_comul