@[reducible, inline]

abbrev RepBialgebra (H : Type u) [Ring H] : Type (u + 1)

The category of representations of a (bi)algebra H, i.e. the category of (left) H-modules, modelled as ModuleCat H.

def RepBialgebra.counitAlgHom (k : Type u) [CommRing k] (H : Type u) [Ring H] [Bialgebra k H] : H →ₐ[k] k

The counit of a bialgebra H as a k-algebra homomorphism H →ₐ[k] k.

@[reducible]

noncomputable def RepBialgebra.trivialModule (k : Type u) [CommRing k] (H : Type u) [Ring H] [Bialgebra k H] : Module H k

The trivial H-module structure on k, obtained by letting H act through its counit.