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.

noncomputable instance TensorProduct.instCoalgebra {R M N : Type u} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Coalgebra R M] [Coalgebra R N] : Coalgebra R (TensorProduct R M N)

Equations

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

noncomputable def Coalgebra.TensorProduct.map {R M N P Q : Type u} [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [AddCommGroup Q] [Module R M] [Module R N] [Module R P] [Module R Q] [Coalgebra R M] [Coalgebra R N] [Coalgebra R P] [Coalgebra R Q] (f : M →ₗc[R] N) (g : P →ₗc[R] Q) : TensorProduct R M P →ₗc[R] TensorProduct R N Q

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 := ⋯ }

@[simp]

theorem Coalgebra.TensorProduct.map_tmul {R M N P Q : Type u} [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [AddCommGroup Q] [Module R M] [Module R N] [Module R P] [Module R Q] [Coalgebra R M] [Coalgebra R N] [Coalgebra R P] [Coalgebra R Q] (f : M →ₗc[R] N) (g : P →ₗc[R] Q) (x : M) (y : P) : (Coalgebra.TensorProduct.map f g) (x ⊗ₜ[R] y) = f x ⊗ₜ[R] g y

@[simp]

theorem Coalgebra.TensorProduct.map_toLinearMap {R M N P Q : Type u} [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [AddCommGroup Q] [Module R M] [Module R N] [Module R P] [Module R Q] [Coalgebra R M] [Coalgebra R N] [Coalgebra R P] [Coalgebra R Q] (f : M →ₗc[R] N) (g : P →ₗc[R] Q) : ↑(Coalgebra.TensorProduct.map f g) = TensorProduct.map ↑f ↑g

noncomputable def Coalgebra.TensorProduct.assoc (R M N P : Type u) [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] [Coalgebra R M] [Coalgebra R N] [Coalgebra R P] : TensorProduct R (TensorProduct R M N) P ≃ₗc[R] TensorProduct R M (TensorProduct R N P)

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.

@[simp]

theorem Coalgebra.TensorProduct.assoc_tmul {R M N P : Type u} [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] [Coalgebra R M] [Coalgebra R N] [Coalgebra R P] (x : M) (y : N) (z : P) : (Coalgebra.TensorProduct.assoc R M N P) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) = x ⊗ₜ[R] y ⊗ₜ[R] z

@[simp]

theorem Coalgebra.TensorProduct.assoc_symm_tmul {R M N P : Type u} [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] [Coalgebra R M] [Coalgebra R N] [Coalgebra R P] (x : M) (y : N) (z : P) : (Coalgebra.TensorProduct.assoc R M N P).symm (x ⊗ₜ[R] y ⊗ₜ[R] z) = (x ⊗ₜ[R] y) ⊗ₜ[R] z

@[simp]

theorem Coalgebra.TensorProduct.assoc_toLinearEquiv {R M N P : Type u} [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] [Coalgebra R M] [Coalgebra R N] [Coalgebra R P] : ↑(Coalgebra.TensorProduct.assoc R M N P) = TensorProduct.assoc R M N P

noncomputable def Coalgebra.TensorProduct.lid (R M : Type u) [CommRing R] [AddCommGroup M] [Module R M] [Coalgebra R M] : TensorProduct R R M ≃ₗc[R] M

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 := ⋯ }

@[simp]

theorem Coalgebra.TensorProduct.lid_toLinearEquiv {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] [Coalgebra R M] : ↑(Coalgebra.TensorProduct.lid R M) = TensorProduct.lid R M

@[simp]

theorem Coalgebra.TensorProduct.lid_tmul {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] [Coalgebra R M] (r : R) (a : M) : (Coalgebra.TensorProduct.lid R M) (r ⊗ₜ[R] a) = r • a

@[simp]

theorem Coalgebra.TensorProduct.lid_symm_apply {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] [Coalgebra R M] (a : M) : (Coalgebra.TensorProduct.lid R M).symm a = 1 ⊗ₜ[R] a

noncomputable def Coalgebra.TensorProduct.rid (R M : Type u) [CommRing R] [AddCommGroup M] [Module R M] [Coalgebra R M] : TensorProduct R M R ≃ₗc[R] M

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 := ⋯ }

@[simp]

theorem Coalgebra.TensorProduct.rid_toLinearEquiv {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] [Coalgebra R M] : ↑(Coalgebra.TensorProduct.rid R M) = TensorProduct.rid R M

@[simp]

theorem Coalgebra.TensorProduct.rid_tmul {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] [Coalgebra R M] (r : R) (a : M) : (Coalgebra.TensorProduct.rid R M) (a ⊗ₜ[R] r) = r • a

@[simp]

theorem Coalgebra.TensorProduct.rid_symm_apply {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] [Coalgebra R M] (a : M) : (Coalgebra.TensorProduct.rid R M).symm a = a ⊗ₜ[R] 1

@[reducible, inline]

noncomputable abbrev CoalgHom.lTensor {R : Type u} (M : Type u) {N P : Type u} [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] [Coalgebra R M] [Coalgebra R N] [Coalgebra R P] (f : N →ₗc[R] P) : TensorProduct R M N →ₗc[R] TensorProduct R M P

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

@[reducible, inline]

noncomputable abbrev CoalgHom.rTensor {R : Type u} (M : Type u) {N P : Type u} [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] [Coalgebra R M] [Coalgebra R N] [Coalgebra R P] (f : N →ₗc[R] P) : TensorProduct R N M →ₗc[R] TensorProduct R P M

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)