# Tensor products of coalgebras #

Given two `R`

-coalgebras `M, N`

, we can define a natural comultiplication map
`Δ : M ⊗[R] N → (M ⊗[R] N) ⊗[R] (M ⊗[R] N)`

and counit map `ε : M ⊗[R] N → R`

induced by
the comultiplication and counit maps of `M`

and `N`

. These `Δ, ε`

are declared as linear maps
in `TensorProduct.instCoalgebraStruct`

in `Mathlib.RingTheory.Coalgebra.Basic`

.

In this file we show that `Δ, ε`

satisfy the axioms of a coalgebra, and also define other data
in the monoidal structure on `R`

-coalgebras, like the tensor product of two coalgebra morphisms
as a coalgebra morphism.

## Implementation notes #

We keep the linear maps underlying `Δ, ε`

and other definitions in this file syntactically equal
to the corresponding definitions for tensor products of modules in the hope that this makes
life easier. However, to fill in prop fields, we use the API in
`Mathlib.Algebra.Category.CoalgebraCat.ComonEquivalence`

. That file defines the monoidal category
structure on coalgebras induced by an equivalence with comonoid objects in the category of modules,
`CoalgebraCat.instMonoidalCategoryAux`

, but we do not declare this as an instance - we just use it
to prove things. Then, we use the definitions in this file to make a monoidal category instance on
`CoalgebraCat R`

in `Mathlib.Algebra.Category.CoalgebraCat.Monoidal`

that has simpler data.

However, this approach forces our coalgebras to be in the same universe as the base ring `R`

,
since it relies on the monoidal category structure on `ModuleCat R`

, which is currently
universe monomorphic. Any contribution that achieves universe polymorphism would be welcome. For
instance, the tensor product of coalgebras in the
FLT repo
is already universe polymorphic since it does not go via category theory.

## Equations

- One or more equations did not get rendered due to their size.

The tensor product of two coalgebra morphisms as a coalgebra morphism.

## Equations

- Coalgebra.TensorProduct.map f g = { toLinearMap := TensorProduct.map f.toLinearMap g.toLinearMap, counit_comp := ⋯, map_comp_comul := ⋯ }

## Instances For

The associator for tensor products of R-coalgebras, as a coalgebra equivalence.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

The base ring is a left identity for the tensor product of coalgebras, up to coalgebra equivalence.

## Equations

- Coalgebra.TensorProduct.lid R M = { toLinearMap := ↑(TensorProduct.lid R M), counit_comp := ⋯, map_comp_comul := ⋯, invFun := (TensorProduct.lid R M).invFun, left_inv := ⋯, right_inv := ⋯ }

## Instances For

The base ring is a right identity for the tensor product of coalgebras, up to coalgebra equivalence.

## Equations

- Coalgebra.TensorProduct.rid R M = { toLinearMap := ↑(TensorProduct.rid R M), counit_comp := ⋯, map_comp_comul := ⋯, invFun := (TensorProduct.rid R M).invFun, left_inv := ⋯, right_inv := ⋯ }

## Instances For

`lTensor M f : M ⊗ N →ₗc M ⊗ P`

is the natural coalgebra morphism induced by `f : N →ₗc P`

.

## Equations

- CoalgHom.lTensor M f = Coalgebra.TensorProduct.map (CoalgHom.id R M) f

## Instances For

`rTensor M f : N ⊗ M →ₗc P ⊗ M`

is the natural coalgebra morphism induced by `f : N →ₗc P`

.

## Equations

- CoalgHom.rTensor M f = Coalgebra.TensorProduct.map f (CoalgHom.id R M)