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).
Both laws come from the same source: the bialgebra axioms say that the comultiplication and
the counit of C are algebra homomorphisms, hence commute with the multiplication that
tensorCombine performs. That single observation is isolated as
lTensor_comp_tensorCombine, and instantiating it at Bialgebra.comulAlgHom and
Bialgebra.counitAlgHom supplies the coefficient half of each law; the remaining half is the
coefficient-free reassociation bookkeeping in
assoc_comp_tensorCombine_rTensor_comp_tensorCombine.
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 onM ⊗ N.TauCeti.Comodule.tensorCombine_natural: naturality of the combining map in the two comodule carriers.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_coassocandTauCeti.Comodule.tensorCoact_counit: the two comodule laws for the diagonal coaction.TauCeti.Comodule.tensor: the rightC-comodule structure onM ⊗[R] N.TauCeti.Comodule.Hom.tensorMap: the tensor product of two comodule morphisms, withtensorMap_idandtensorMap_comp.
References #
This is the standard tensor product of right comodules over a bialgebra; see Sweedler, Hopf
Algebras, Chapter 2. It advances the Layer 1 target "Comodules over a coalgebra/Hopf algebra
... tensor products, duals, the regular representation" of the Tau Ceti reductive-groups
roadmap, ReductiveGroups/README.md in TauCetiRoadmap, which asks for the rigid monoidal
category of finite-dimensional comodules; the tensor product built here is its underlying
bifunctor.
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
Instances For
tensorCombine sends (m ⊗ c) ⊗ (n ⊗ d) to (m ⊗ n) ⊗ cd.
The combining map is natural in the two comodule carriers.
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
Instances For
The tensor-product coaction, before expanding the two component coactions.
The diagonal tensor coaction is natural under tensor products of comodule morphisms.
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.
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.
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.
The diagonal coaction on M ⊗[R] N satisfies the counit law: the counit of C is an
algebra homomorphism, so it turns the product of the two coefficients into the product of
their counits, which is 1.
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 := ⋯ }
Instances For
The coaction of the tensor-product comodule is the diagonal coaction tensorCoact.
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 := ⋯ }
Instances For
The underlying linear map of tensorMap f g is the tensor product of the two underlying
linear maps.
tensorMap f g acts as f ⊗ g.
tensorMap acts on a simple tensor as the pair of component morphisms.
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.)
The tensor product of morphisms is compatible with composition.