Theorems · Inductive type · ring theory
Bialgebra
(R : Type u) → (A : Type v) → [CommSemiring R] → [Semiring A] → Type (max u v)
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
- Cited by
- 160 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 3 definitions · uses no axioms
- Assumes
- CommSemiringSemiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringstatement · cited by 13,802
- CommSemiringstatement · cited by 10,911
Cited by221
Results whose statement or proof uses this declaration.
- Bialgebra.counitAlgHomstatement and proof · cited by 23
- Bialgebra.comulAlgHomstatement and proof · cited by 20
- CommBialgCat.ofstatement and proof · cited by 19
- BialgCat.ofstatement and proof · cited by 17
- CommBialgCat.ofHomstatement and proof · cited by 12
- BialgHom.ofAlgHomstatement and proof · cited by 9
- BialgEquiv.toBialgIsostatement and proof · cited by 8
- Bialgebra.TensorProduct.mapstatement and proof · cited by 8
- BialgCat.ofHomstatement and proof · cited by 6
- Bialgebra.comul_onestatement and proof · cited by 6
- Bialgebra.counit_onestatement and proof · cited by 6
- Bialgebra.mulBialgHomstatement and proof · cited by 6
Showing the 200 most cited of 221.