Structures · Algebra
Coalgebra
A coalgebra over a commutative (semi)ring R is an R-module equipped with a coassociative
comultiplication Δ and a counit ε obeying the left and right counitality laws.
- Defined in
- Mathlib.RingTheory.Coalgebra.Basic
- Shape
- 2 explicit arguments · adds coassoc, rTensor_counit_comp_comul, lTensor_counit_comp_comul
Extends1
Extended by1
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by153
- CoalgCat.of
- GroupLike.val
- IsGroupLikeElem.comul_eq_tmul_self
- IsGroupLikeElem.counit_eq_one
- CoalgEquiv.toCoalgIso
- CoalgCat.ofHom
- Coalgebra.TensorProduct.rid
- Coalgebra.TensorProduct.assoc
- Coalgebra.TensorProduct.lid
- AddMonoidAlgebra.counit_single
- AddMonoidAlgebra.comul_single
- Coalgebra.TensorProduct.map
- Coalgebra.rTensor_counit_comp_comul
- GroupLike.valEquiv
- Coalgebra.coassoc
- Coalgebra.Repr.induced
- MonoidAlgebra.counit_single
- Coalgebra.lTensor_counit_comp_comul
- linearIndepOn_isGroupLikeElem
- Coalgebra.counitCoalgHom
- Coalgebra.comm_comul
- Coalgebra.comm_comp_comul
- MonoidAlgebra.comul_single
- Prod.comul_comp_inr
- Prod.comul_comp_inl
- Coalgebra.sum_counit_tmul_eq
- CoassocSimps.assoc_comp_map_comm_comp_comul_comp_comul
- CoalgHom.lTensor
- IsGroupLikeElem.ne_zero
- IsGroupLikeElem.map
- CoassocSimps.map_counit_comp_comul_right
- GroupLike.val_injective
- Coalgebra.coassoc_symm_apply
- CoassocSimps.coassoc_right
- Coalgebra.sum_tmul_counit_eq
- LaurentPolynomial.comul_C_mul_T
- Coalgebra.ext_to_ring
- Equiv.coalgebra
- CoassocSimps.coassoc_left
- Coalgebra.coassoc_apply
- Coalgebra.sum_counit_smul
- GroupLike.isGroupLikeElem_val
- Coalgebra.sum_tmul_tmul_eq
- CoassocSimps.map_counit_comp_comul_left
- CoalgHom.rTensor
- InnerProductSpace.mulOfCoalgebra
- LinearMap.convNonUnitalSemiring
- Prod.instCoalgebra
- Prod.comul_apply
- AddMonoidAlgebra.instCoalgebra