# Bialgebras #

In this file we define `Bialgebra`

s.

## Main definitions #

`Bialgebra R A`

: the structure of a bialgebra on the`R`

-algebra`A`

;`CommSemiring.toBialgebra`

: a commutative semiring is a bialgebra over itself.

## Implementation notes #

Rather than the "obvious" axiom `∀ a b, counit (a * b) = counit a * counit b`

, the far
more convoluted `mul_compr₂_counit`

is used as a structure field; this says that
the corresponding two maps `A →ₗ[R] A →ₗ[R] R`

are equal; a similar trick is
used for comultiplication as well. An alternative constructor `Bialgebra.mk'`

is provided
with the more easily-readable axioms. The argument for using the more convoluted axioms
is that in practice there is evidence that they will be easier to prove (especially
when dealing with things like tensor products of bialgebras). This does make the definition
more surprising to mathematicians, however mathlib is no stranger to definitions which
are surprising to mathematicians -- see for example its definition of a group.
Note that this design decision is also compatible with that of `Coalgebra`

. The lengthy
docstring for these convoluted fields attempts to explain what is going on.

## References #

## Tags #

bialgebra

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.

## Instances

The counit on a bialgebra preserves 1.

The counit on a bialgebra preserves multiplication. Note that this is written
in a rather obscure way: it says that two bilinear maps `A →ₗ[R] A →ₗ[R]`

are equal.
The two corresponding equal linear maps `A ⊗[R] A →ₗ[R]`

are the following: the first factors through `A`

and is multiplication on `A`

followed
by `counit`

. The second factors through `R ⊗[R] R`

, and is `counit ⊗ counit`

followed by
multiplication on `R`

.

See `Bialgebra.mk'`

for a constructor for bialgebras which uses
the more familiar but mathematically equivalent `counit (a * b) = counit a * counit b`

.

The comultiplication on a bialgebra preserves `1`

.

The comultiplication on a bialgebra preserves multiplication. This is written in
a rather obscure way: it says that two bilinear maps `A →ₗ[R] A →ₗ[R] (A ⊗[R] A)`

are equal. The corresponding equal linear maps `A ⊗[R] A →ₗ[R] A ⊗[R] A`

are firstly multiplication followed by `comul`

, and secondly `comul ⊗ comul`

followed
by multiplication on `A ⊗[R] A`

.

See `Bialgebra.mk'`

for a constructor for bialgebras which uses the more familiar
but mathematically equivalent `comul (a * b) = comul a * comul b`

.

If `R`

is a field (or even a commutative semiring) and `A`

is an `R`

-algebra with a coalgebra structure, then `Bialgebra.mk'`

consumes proofs that the counit and comultiplication preserve
the identity and multiplication, and produces a bialgebra
structure on `A`

.

## Equations

- Bialgebra.mk' R A counit_one counit_mul comul_one comul_mul = Bialgebra.mk counit_one ⋯ comul_one ⋯

## Instances For

`counitAlgHom R A`

is the counit of the `R`

-bialgebra `A`

, as an `R`

-algebra map.

## Equations

- Bialgebra.counitAlgHom R A = AlgHom.ofLinearMap Coalgebra.counit ⋯ ⋯

## Instances For

`comulAlgHom R A`

is the comultiplication of the `R`

-bialgebra `A`

, as an `R`

-algebra map.

## Equations

- Bialgebra.comulAlgHom R A = AlgHom.ofLinearMap Coalgebra.comul ⋯ ⋯

## Instances For

Every commutative (semi)ring is a bialgebra over itself

## Equations

- CommSemiring.toBialgebra R = Bialgebra.mk ⋯ ⋯ ⋯ ⋯