The tensor product of comodules over a bialgebra

This file constructs the tensor product of two right comodules over a bialgebra C. If M and N are right C-comodules, the coaction on M ⊗ N is the usual diagonal formula

m ⊗ n ↦ m₀ ⊗ n₀ ⊗ m₁ n₁,

which multiplies the two coefficient factors in C. The file first builds this map (tensorCombine, tensorCoact), then verifies the coassociativity and counit laws and packages them as Comodule.tensor, and finally makes the construction functorial in both arguments (Comodule.Hom.tensorMap).

Coefficient combination is natural in both carrier modules and respects the associator and unitors. Associativity needs only an associative coefficient multiplication, while the unitor laws need a multiplicative identity. For commutative coefficients it also respects the tensor symmetry. These compatibilities give the tensor product its monoidal structure.

Following Comodule.cofree, Comodule.tensor is not a global instance: an R-module can carry many coactions, so a global instance on a tensor product would make Comodule resolution non-confluent.

Main declarations

• TauCeti.Comodule.tensorCombine: combines two coacted tensor factors.
• TauCeti.Comodule.tensorCoact: the diagonal coaction on M ⊗ N.
• TauCeti.Comodule.tensorCombine_natural: naturality of the combining map in the two comodule carriers.
• TauCeti.Comodule.tensorCombine_assoc, tensorCombine_lid, and tensorCombine_rid: compatibility of coefficient combination with the tensor associator and unitors.
• TauCeti.Comodule.tensorCombine_comm: compatibility of coefficient combination with swapping the two carrier factors when the coefficient algebra is commutative.
• TauCeti.Comodule.tensorCoact_natural: the diagonal coaction commutes with tensoring comodule morphisms.
• TauCeti.Comodule.lTensor_comp_tensorCombine: an algebra homomorphism on the coefficients passes through the combining map.
• TauCeti.Comodule.tensorCoact_coassoc and TauCeti.Comodule.tensorCoact_counit: the two comodule laws for the diagonal coaction.
• TauCeti.Comodule.tensor: the right C-comodule structure on M ⊗[R] N.
• TauCeti.Comodule.Hom.tensorMap: the tensor product of two comodule morphisms, with tensorMap_id and tensorMap_comp.

References

This is the standard tensor product of right comodules over a bialgebra; see Sweedler, Hopf Algebras, Chapter 2. The tensor product is the underlying bifunctor of the monoidal category of comodules.

noncomputable def TauCeti.Comodule.tensorCombine {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [NonUnitalNonAssocSemiring C] [Module R C] [SMulCommClass R C C] [IsScalarTower R C C] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : TensorProduct R (TensorProduct R M C) (TensorProduct R N C) →ₗ[R] TensorProduct R (TensorProduct R M N) C

Combine two coacted tensor factors by shuffling the middle factors together and multiplying the two C-components.

On pure tensors it sends (m ⊗ c) ⊗ (n ⊗ d) to (m ⊗ n) ⊗ cd.

Equations

• TauCeti.Comodule.tensorCombine = TensorProduct.map LinearMap.id (LinearMap.mul' R C) ∘ₗ ↑(TensorProduct.tensorTensorTensorComm R M C N C)

@[simp]

theorem TauCeti.Comodule.tensorCombine_tmul_tmul {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [NonUnitalNonAssocSemiring C] [Module R C] [SMulCommClass R C C] [IsScalarTower R C C] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (m : M) (c : C) (n : N) (d : C) : tensorCombine (m ⊗ₜ[R] c ⊗ₜ[R] (n ⊗ₜ[R] d)) = m ⊗ₜ[R] n ⊗ₜ[R] (c * d)

tensorCombine sends (m ⊗ c) ⊗ (n ⊗ d) to (m ⊗ n) ⊗ cd.

theorem TauCeti.Comodule.tensorCombine_natural {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [NonUnitalNonAssocSemiring C] [Module R C] [SMulCommClass R C C] [IsScalarTower R C C] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {M' : Type y} {N' : Type z} [AddCommMonoid M'] [Module R M'] [AddCommMonoid N'] [Module R N'] (f : M →ₗ[R] M') (g : N →ₗ[R] N') : TensorProduct.map (TensorProduct.map f g) LinearMap.id ∘ₗ tensorCombine = tensorCombine ∘ₗ TensorProduct.map (TensorProduct.map f LinearMap.id) (TensorProduct.map g LinearMap.id)

The combining map is natural in the two comodule carriers.

theorem TauCeti.Comodule.tensorCombine_assoc {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] {P : Type u_1} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [NonUnitalSemiring C] [Module R C] [SMulCommClass R C C] [IsScalarTower R C C] (x : TensorProduct R M C) (y : TensorProduct R N C) (z : TensorProduct R P C) : (TensorProduct.map (↑(TensorProduct.assoc R M N P)) LinearMap.id) (tensorCombine (tensorCombine (x ⊗ₜ[R] y) ⊗ₜ[R] z)) = tensorCombine (x ⊗ₜ[R] tensorCombine (y ⊗ₜ[R] z))

Combining three coacted factors is compatible with reassociation. The two sides multiply the coefficient factors as (c * d) * e and c * (d * e), respectively.

theorem TauCeti.Comodule.tensorCombine_assoc_symm {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] {P : Type u_1} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [NonUnitalSemiring C] [Module R C] [SMulCommClass R C C] [IsScalarTower R C C] (x : TensorProduct R M C) (y : TensorProduct R N C) (z : TensorProduct R P C) : (TensorProduct.map (↑(TensorProduct.assoc R M N P).symm) LinearMap.id) (tensorCombine (x ⊗ₜ[R] tensorCombine (y ⊗ₜ[R] z))) = tensorCombine (tensorCombine (x ⊗ₜ[R] y) ⊗ₜ[R] z)

The inverse associator is compatible with combining three coacted factors.

theorem TauCeti.Comodule.tensorCombine_lid {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [NonAssocSemiring C] [Module R C] [SMulCommClass R C C] [IsScalarTower R C C] (r : R) (x : TensorProduct R M C) : (TensorProduct.map (↑(TensorProduct.lid R M)) LinearMap.id) (tensorCombine (r ⊗ₜ[R] 1 ⊗ₜ[R] x)) = r • x

Combining the trivial coefficient 1 on the left and applying the left tensor unitor scales a coacted vector by the scalar in the trivial factor.

theorem TauCeti.Comodule.tensorCombine_lid_symm {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [NonAssocSemiring C] [Module R C] [SMulCommClass R C C] [IsScalarTower R C C] (x : TensorProduct R M C) : tensorCombine (1 ⊗ₜ[R] 1 ⊗ₜ[R] x) = (TensorProduct.map (↑(TensorProduct.lid R M).symm) LinearMap.id) x

Combining the trivial coefficient 1 on the left agrees with applying the inverse left tensor unitor to the carrier factor.

theorem TauCeti.Comodule.tensorCombine_rid {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [NonAssocSemiring C] [Module R C] [SMulCommClass R C C] [IsScalarTower R C C] (x : TensorProduct R M C) (r : R) : (TensorProduct.map (↑(TensorProduct.rid R M)) LinearMap.id) (tensorCombine (x ⊗ₜ[R] (r ⊗ₜ[R] 1))) = r • x

Combining the trivial coefficient 1 on the right and applying the right tensor unitor scales a coacted vector by the scalar in the trivial factor.

theorem TauCeti.Comodule.tensorCombine_rid_symm {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [NonAssocSemiring C] [Module R C] [SMulCommClass R C C] [IsScalarTower R C C] (x : TensorProduct R M C) : tensorCombine (x ⊗ₜ[R] (1 ⊗ₜ[R] 1)) = (TensorProduct.map (↑(TensorProduct.rid R M).symm) LinearMap.id) x

Combining the trivial coefficient 1 on the right agrees with applying the inverse right tensor unitor to the carrier factor.

theorem TauCeti.Comodule.tensorCombine_comm {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [NonUnitalNonAssocCommSemiring C] [Module R C] [SMulCommClass R C C] [IsScalarTower R C C] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (x : TensorProduct R M C) (y : TensorProduct R N C) : (TensorProduct.map (↑(TensorProduct.comm R M N)) LinearMap.id) (tensorCombine (x ⊗ₜ[R] y)) = tensorCombine (y ⊗ₜ[R] x)

Swapping two coacted factors commutes with combining their coefficients when the coefficient algebra is commutative.

noncomputable def TauCeti.Comodule.tensorCoact {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [Semiring C] [Bialgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] : TensorProduct R M N →ₗ[R] TensorProduct R (TensorProduct R M N) C

The diagonal coaction map on the tensor product of two right comodules over a bialgebra.

The later full tensor-product comodule structure uses this map as its coaction.

Equations

• TauCeti.Comodule.tensorCoact = TauCeti.Comodule.tensorCombine ∘ₗ TensorProduct.map TauCeti.Comodule.coact TauCeti.Comodule.coact

@[simp]

theorem TauCeti.Comodule.tensorCoact_tmul {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [Semiring C] [Bialgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] (m : M) (n : N) : tensorCoact (m ⊗ₜ[R] n) = tensorCombine (coact m ⊗ₜ[R] coact n)

The tensor-product coaction, before expanding the two component coactions.

theorem TauCeti.Comodule.tensorCoact_natural {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] {M' : Type y} {N' : Type z} [Semiring C] [Bialgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] [AddCommMonoid M'] [Module R M'] [Comodule R C M'] [AddCommMonoid N'] [Module R N'] [Comodule R C N'] (f : Hom R C M M') (g : Hom R C N N') : TensorProduct.map (TensorProduct.map f.toLinearMap g.toLinearMap) LinearMap.id ∘ₗ tensorCoact = tensorCoact ∘ₗ TensorProduct.map f.toLinearMap g.toLinearMap

The diagonal tensor coaction is natural under tensor products of comodule morphisms.

theorem TauCeti.Comodule.lTensor_comp_tensorCombine {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] {D : Type y} [Semiring C] [Algebra R C] [Semiring D] [Algebra R D] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (φ : C →ₐ[R] D) : LinearMap.lTensor (TensorProduct R M N) φ.toLinearMap ∘ₗ tensorCombine = tensorCombine ∘ₗ TensorProduct.map (LinearMap.lTensor M φ.toLinearMap) (LinearMap.lTensor N φ.toLinearMap)

An R-algebra homomorphism φ : C →ₐ[R] D may be pushed through the combining map: tensorCombine multiplies the two coefficient factors, and φ is multiplicative.

Taking φ to be the comultiplication and the counit of a bialgebra gives precisely the two compatibilities that make tensorCoact a coaction.

theorem TauCeti.Comodule.comm_tensorCombine_eq_distribBaseChange_symm_tmul {R : Type u} {M : Type w} {N : Type x} [CommSemiring R] {A : Type y} [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (p : TensorProduct R M A) (q : TensorProduct R N A) : (TensorProduct.comm R (TensorProduct R M N) A) (tensorCombine (p ⊗ₜ[R] q)) = (TensorProduct.AlgebraTensorModule.distribBaseChange R A M N).symm ((TensorProduct.comm R M A) p ⊗ₜ[A] (TensorProduct.comm R N A) q)

Combining two coefficient columns and then commuting the carrier past the coefficients agrees with first commuting each column and then applying scalar-extension distributivity.

theorem TauCeti.Comodule.assoc_comp_tensorCombine_rTensor_comp_tensorCombine {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [Semiring C] [Algebra R C] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : ↑(TensorProduct.assoc R (TensorProduct R M N) C C) ∘ₗ LinearMap.rTensor C tensorCombine ∘ₗ tensorCombine = tensorCombine ∘ₗ TensorProduct.map ↑(TensorProduct.assoc R M C C) ↑(TensorProduct.assoc R N C C)

Combining twice and then reassociating agrees with reassociating each factor first and then combining once over C ⊗[R] C.

This is pure bookkeeping about tensorCombine — it uses no coalgebra structure — and it is what turns the coassociativity of the two factors into the coassociativity of tensorCoact.

theorem TauCeti.Comodule.tensorCoact_coassoc {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [Semiring C] [Bialgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] : ↑(TensorProduct.assoc R (TensorProduct R M N) C C) ∘ₗ LinearMap.rTensor C tensorCoact ∘ₗ tensorCoact = LinearMap.lTensor (TensorProduct R M N) CoalgebraStruct.comul ∘ₗ tensorCoact

The diagonal coaction on M ⊗[R] N is coassociative.

Coassociativity of the two factors puts the doubly coacted vectors into the form m₀ ⊗ Δ(m₁), and the comultiplication of C is an algebra homomorphism, so it commutes with the multiplication that tensorCombine performs on the coefficients.

theorem TauCeti.Comodule.tensorCoact_counit {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [Semiring C] [Bialgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] : LinearMap.lTensor (TensorProduct R M N) CoalgebraStruct.counit ∘ₗ tensorCoact = (TensorProduct.mk R (TensorProduct R M N) R).flip 1

Applying the counit to the diagonal coaction recovers the original tensor with coefficient 1.

@[implicit_reducible]

noncomputable def TauCeti.Comodule.tensor (R : Type u) (C : Type v) (M : Type w) (N : Type x) [CommSemiring R] [Semiring C] [Bialgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] : Comodule R C (TensorProduct R M N)

The tensor product of two right C-comodules over a bialgebra, with the diagonal coaction m ⊗ n ↦ (m₀ ⊗ n₀) ⊗ m₁ n₁.

Following Comodule.cofree, this is deliberately not a global instance: an R-module can carry many coactions, so a global instance on a tensor product would make Comodule resolution non-confluent. Select it explicitly, or register it as a local instance.

Equations

• TauCeti.Comodule.tensor R C M N = { coact := TauCeti.Comodule.tensorCoact, coassoc := ⋯, lTensor_counit_comp_coact := ⋯ }

@[simp]

theorem TauCeti.Comodule.tensor_coact {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [Semiring C] [Bialgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] : coact = tensorCoact

The coaction of the tensor-product comodule is the diagonal coaction tensorCoact.

noncomputable def TauCeti.Comodule.Hom.tensorMap {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [Semiring C] [Bialgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] {M' : Type y} {N' : Type z} [AddCommMonoid M'] [Module R M'] [Comodule R C M'] [AddCommMonoid N'] [Module R N'] [Comodule R C N'] (f : Hom R C M M') (g : Hom R C N N') : Hom R C (TensorProduct R M N) (TensorProduct R M' N')

The tensor product of two comodule morphisms, as a morphism of tensor-product comodules.

Both source and target carry the diagonal coaction of Comodule.tensor; the required compatibility is Comodule.tensorCoact_natural.

Equations

• f.tensorMap g = { toLinearMap := TensorProduct.map f.toLinearMap g.toLinearMap, map_coact := ⋯ }

@[simp]

theorem TauCeti.Comodule.Hom.tensorMap_toLinearMap {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [Semiring C] [Bialgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] {M' : Type y} {N' : Type z} [AddCommMonoid M'] [Module R M'] [Comodule R C M'] [AddCommMonoid N'] [Module R N'] [Comodule R C N'] (f : Hom R C M M') (g : Hom R C N N') : (f.tensorMap g).toLinearMap = TensorProduct.map f.toLinearMap g.toLinearMap

The underlying linear map of tensorMap f g is the tensor product of the two underlying linear maps.

@[simp]

theorem TauCeti.Comodule.Hom.tensorMap_apply {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [Semiring C] [Bialgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] {M' : Type y} {N' : Type z} [AddCommMonoid M'] [Module R M'] [Comodule R C M'] [AddCommMonoid N'] [Module R N'] [Comodule R C N'] (f : Hom R C M M') (g : Hom R C N N') (x : TensorProduct R M N) : (f.tensorMap g) x = (TensorProduct.map f.toLinearMap g.toLinearMap) x

tensorMap f g acts as f ⊗ g.

@[simp]

theorem TauCeti.Comodule.Hom.tensorMap_tmul {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [Semiring C] [Bialgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] {M' : Type y} {N' : Type z} [AddCommMonoid M'] [Module R M'] [Comodule R C M'] [AddCommMonoid N'] [Module R N'] [Comodule R C N'] (f : Hom R C M M') (g : Hom R C N N') (m : M) (n : N) : (f.tensorMap g) (m ⊗ₜ[R] n) = f m ⊗ₜ[R] g n

tensorMap acts on a simple tensor as the pair of component morphisms.

theorem TauCeti.Comodule.Hom.tensorMap_id {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [Semiring C] [Bialgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] : (id R C M).tensorMap (id R C N) = id R C (TensorProduct R M N)

The tensor product of two identity morphisms is the identity morphism.

This is not a simp lemma: its left-hand side is not in simp-normal form, because the @[simp] lemma ComoduleCat.ofHom_id rewrites each Comodule.Hom.id R C _ to the categorical identity 𝟙 (ComoduleCat.of R C _). This fires even though no ComoduleCat.ofHom appears syntactically in the left-hand side: ofHom is a reducible abbrev for the identity coercion (a categorical morphism of R C M ⟶ of R C N just is a Comodule.Hom R C M N), so simp unifies ofHom_id's left-hand side ofHom (Comodule.Hom.id R C _) with a bare Comodule.Hom.id R C _. Tagging this lemma @[simp] therefore fails the simpNF linter. (Contrast cofreeMap_id, whose left-hand side cofreeMap LinearMap.id carries no bare Comodule.Hom.id and so stays normal.)

@[simp]

theorem TauCeti.Comodule.Hom.tensorMap_comp {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [Semiring C] [Bialgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] {M' : Type y} {N' : Type z} [AddCommMonoid M'] [Module R M'] [Comodule R C M'] [AddCommMonoid N'] [Module R N'] [Comodule R C N'] {M'' : Type u_1} {N'' : Type u_2} [AddCommMonoid M''] [Module R M''] [Comodule R C M''] [AddCommMonoid N''] [Module R N''] [Comodule R C N''] (f : Hom R C M M') (f' : Hom R C M' M'') (g : Hom R C N N') (g' : Hom R C N' N'') : (f'.comp f).tensorMap (g'.comp g) = (f'.tensorMap g').comp (f.tensorMap g)

The tensor product of morphisms is compatible with composition.