Structures · Algebra
CoalgebraStruct
Data fields for Coalgebra, to allow API to be constructed before proving Coalgebra.coassoc.
See Coalgebra for documentation.
- Defined in
- Mathlib.RingTheory.Coalgebra.Basic
- Shape
- 2 explicit arguments · adds comul, counit
Extends0
Extends nothing: this is a root of the hierarchy.
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 by283
- CoalgebraStruct.comul
- CoalgebraStruct.counit
- BialgHom.toAlgHom
- CoalgHom.toLinearMap
- BialgHom.comp
- CoalgEquiv.symm
- BialgHomClass.toBialgHom
- CoalgHomClass.toCoalgHom
- BialgHom.id
- Coalgebra.Repr.right
- Coalgebra.Repr.left
- BialgEquiv.symm
- Coalgebra.Repr.index
- CoalgEquiv.toLinearEquiv
- BialgEquiv.toAlgEquiv
- CoalgHom.comp
- CoalgEquivClass.toCoalgEquiv
- CoalgHom.id
- CoalgEquiv.toCoalgHom
- BialgEquiv.toCoalgEquiv
- CoalgEquiv.trans
- BialgEquiv.toEquiv
- BialgEquiv.trans
- BialgHom.toCoalgHom
- BialgHom.coe_toAlgHom_injective
- Pi.comul_single
- CoalgEquiv.refl
- Coalgebra.Repr.eq
- BialgEquiv.refl
- BialgHom.comp_apply
- CoalgEquiv.toEquiv
- Finsupp.comul_single
- Coalgebra.Repr.arbitrary
- CoalgHom.copy
- CoalgEquiv.invFun
- Finsupp.counit_single
- CoalgEquiv.toEquiv_injective
- BialgEquiv.toBialgHom
- CoalgHom.coe_linearMap_injective
- DFinsupp.comul_single
- Coalgebra.Repr.convMul_apply
- Pi.counit_single
- BialgHom.id_apply
- CoalgEquiv.ofBijective
- BialgHom.coe_fn_injective
- BialgEquiv.toEquiv_injective
- CoalgHomClass.counit_comp_apply
- CoalgEquiv.ofCoalgHom
- BialgEquiv.ofBialgHom
- DFinsupp.counit_single
Ancestors0
No ancestors.