Theorems · Definition · category theory

CommBialgCat.of

(R : Type u) → [inst : CommRing R] → (X : Type v) → [inst_1 : CommRing X] → [Bialgebra R X] → CommBialgCat R

Turn an unbundled R-bialgebra into the corresponding object in the category of R-bialgebras. This is the preferred way to construct a term of CommBialgCat R.

Defined in

Mathlib.Algebra.Category.CommBialgCat

Cited by

19 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

CommRingCommRingBialgebra