Tensor products of finitely generated comodules

This file lifts the tensor product of right comodules over a bialgebra to the category of finitely generated comodules. If M and N are finitely generated right C-comodules, their tensor product has the diagonal coaction

m ⊗ n ↦ (m₀ ⊗ n₀) ⊗ m₁n₁.

The tensor-product carrier remains finitely generated by Module.Finite.tensorProduct. Tensoring two comodule morphisms therefore gives a morphism between finite objects, and these maps assemble into a bifunctor on FGComoduleCat.

Main declarations

• TauCeti.FGComoduleCat.tensor: the tensor product as a finitely generated comodule.
• TauCeti.FGComoduleCat.tensorMap: the tensor product of two morphisms.
• TauCeti.FGComoduleCat.tensorBifunctor: tensor product as a bifunctor on finite comodules.

References

This is finite-category infrastructure for Layer 1 of the Tau Ceti reductive-groups roadmap, ReductiveGroups/README.md in TauCetiRoadmap, specifically the requested rigid monoidal category of finite-dimensional comodules. It packages the diagonal comodule constructed in TauCeti.Algebra.Coalgebra.Comodule.TensorProduct and reuses Mathlib's finite-generation instance for tensor products.

@[reducible, inline]

noncomputable abbrev TauCeti.FGComoduleCat.tensor (R : Type u) [CommSemiring R] (C : Type v) [Semiring C] [Bialgebra R C] (M N : FGComoduleCat R C) : FGComoduleCat R C

The tensor product of two finitely generated right comodules over a bialgebra.

Its carrier is the tensor product of the underlying modules, equipped with the diagonal coaction from Comodule.tensor.

Equations

• TauCeti.FGComoduleCat.tensor R C M N = TauCeti.FGComoduleCat.of (TensorProduct R ↑M ↑N)

@[simp]

theorem TauCeti.FGComoduleCat.tensor_obj (R : Type u) [CommSemiring R] (C : Type v) [Semiring C] [Bialgebra R C] (M N : FGComoduleCat R C) : (tensor R C M N).obj = ComoduleCat.of R C (TensorProduct R ↑M ↑N)

The ambient comodule underlying the finite tensor product is the diagonal tensor-product comodule.

@[simp]

theorem TauCeti.FGComoduleCat.tensor_coe (R : Type u) [CommSemiring R] (C : Type v) [Semiring C] [Bialgebra R C] (M N : FGComoduleCat R C) : ↑(tensor R C M N) = TensorProduct R ↑M ↑N

The underlying type of the finite tensor product is the tensor product of the underlying modules.

@[simp]

theorem TauCeti.FGComoduleCat.tensor_coact (R : Type u) [CommSemiring R] (C : Type v) [Semiring C] [Bialgebra R C] (M N : FGComoduleCat R C) : Comodule.coact = Comodule.tensorCoact

The coaction on the finite tensor product is the diagonal tensor coaction.

@[simp]

theorem TauCeti.FGComoduleCat.incl_tensor (R : Type u) [CommSemiring R] (C : Type v) [Semiring C] [Bialgebra R C] (M N : FGComoduleCat R C) : incl.obj (tensor R C M N) = ComoduleCat.of R C (TensorProduct R ↑M ↑N)

The inclusion into all comodules sends the finite tensor product to the ambient tensor-product comodule.

@[simp]

theorem TauCeti.FGComoduleCat.forget₂_semimoduleCat_tensor_obj (R : Type u) [CommSemiring R] (C : Type v) [Semiring C] [Bialgebra R C] (M N : FGComoduleCat R C) : (CategoryTheory.forget₂ (FGComoduleCat R C) (SemimoduleCat R)).obj (tensor R C M N) = ↧(TensorProduct R ↑M ↑N)

Forgetting the finite tensor product to semimodules gives the ordinary tensor-product module.

@[reducible, inline]

noncomputable abbrev TauCeti.FGComoduleCat.tensorMap {R : Type u} [CommSemiring R] {C : Type v} [Semiring C] [Bialgebra R C] {M M' N N' : FGComoduleCat R C} (f : M ⟶ M') (g : N ⟶ N') : tensor R C M N ⟶ tensor R C M' N'

The tensor product of two morphisms of finitely generated comodules.

Equations

• TauCeti.FGComoduleCat.tensorMap f g = TauCeti.FGComoduleCat.ofHom (TauCeti.Comodule.Hom.tensorMap f.hom g.hom)

@[simp]

theorem TauCeti.FGComoduleCat.tensorMap_toLinearMap {R : Type u} [CommSemiring R] {C : Type v} [Semiring C] [Bialgebra R C] {M M' N N' : FGComoduleCat R C} (f : M ⟶ M') (g : N ⟶ N') : (tensorMap f g).hom.toLinearMap = TensorProduct.map f.hom.toLinearMap g.hom.toLinearMap

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

@[simp]

theorem TauCeti.FGComoduleCat.tensorMap_apply {R : Type u} [CommSemiring R] {C : Type v} [Semiring C] [Bialgebra R C] {M M' N N' : FGComoduleCat R C} (f : M ⟶ M') (g : N ⟶ N') (x : TensorProduct R ↑M ↑N) : (CategoryTheory.ConcreteCategory.hom (tensorMap f g)) x = (TensorProduct.map f.hom.toLinearMap g.hom.toLinearMap) x

The finite-comodule tensor map acts as the ordinary tensor product of its two underlying linear maps.

@[simp]

theorem TauCeti.FGComoduleCat.tensorMap_tmul {R : Type u} [CommSemiring R] {C : Type v} [Semiring C] [Bialgebra R C] {M M' N N' : FGComoduleCat R C} (f : M ⟶ M') (g : N ⟶ N') (m : ↑M) (n : ↑N) : (CategoryTheory.ConcreteCategory.hom (tensorMap f g)) (m ⊗ₜ[R] n) = (CategoryTheory.ConcreteCategory.hom f) m ⊗ₜ[R] (CategoryTheory.ConcreteCategory.hom g) n

On a simple tensor, tensorMap f g applies the two component morphisms.

@[simp]

theorem TauCeti.FGComoduleCat.tensorMap_id {R : Type u} [CommSemiring R] {C : Type v} [Semiring C] [Bialgebra R C] (M N : FGComoduleCat R C) : tensorMap (CategoryTheory.CategoryStruct.id M) (CategoryTheory.CategoryStruct.id N) = CategoryTheory.CategoryStruct.id (tensor R C M N)

Tensoring two identity morphisms gives the identity of the finite tensor product.

@[simp]

theorem TauCeti.FGComoduleCat.tensorMap_comp {R : Type u} [CommSemiring R] {C : Type v} [Semiring C] [Bialgebra R C] {M M' M'' N N' N'' : FGComoduleCat R C} (f : M ⟶ M') (f' : M' ⟶ M'') (g : N ⟶ N') (g' : N' ⟶ N'') : tensorMap (CategoryTheory.CategoryStruct.comp f f') (CategoryTheory.CategoryStruct.comp g g') = CategoryTheory.CategoryStruct.comp (tensorMap f g) (tensorMap f' g')

Tensor products of finite-comodule morphisms preserve composition.

noncomputable def TauCeti.FGComoduleCat.tensorBifunctor (R : Type u) [CommSemiring R] (C : Type v) [Semiring C] [Bialgebra R C] : CategoryTheory.Functor (FGComoduleCat R C × FGComoduleCat R C) (FGComoduleCat R C)

Tensor product as a bifunctor on finitely generated right comodules.

It sends (M, N) to the finite diagonal comodule M ⊗ N and a pair of morphisms (f, g) to f ⊗ g. This is the tensor bifunctor underlying the future monoidal structure on FGComoduleCat.

Equations

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

@[simp]

theorem TauCeti.FGComoduleCat.tensorBifunctor_obj (R : Type u) [CommSemiring R] (C : Type v) [Semiring C] [Bialgebra R C] (P : FGComoduleCat R C × FGComoduleCat R C) : (tensorBifunctor R C).obj P = tensor R C P.1 P.2

The object part of tensorBifunctor is the finite tensor product.

@[simp]

theorem TauCeti.FGComoduleCat.tensorBifunctor_map (R : Type u) [CommSemiring R] (C : Type v) [Semiring C] [Bialgebra R C] {P Q : FGComoduleCat R C × FGComoduleCat R C} (fg : P ⟶ Q) : (tensorBifunctor R C).map fg = tensorMap fg.1 fg.2

The morphism part of tensorBifunctor is the tensor product of the two component morphisms.