The monoidal category of finitely generated comodules

This file equips finitely generated right comodules over a bialgebra with their standard monoidal structure. The tensor product is the diagonal comodule constructed in TauCeti.Algebra.Coalgebra.Comodule.Finite.TensorProduct, and the tensor unit is the base semiring with its trivial coaction.

The associator and unitors are the usual tensor-product linear equivalences. Their compatibility with the diagonal coaction reduces on pure coaction tensors to associativity and the unit laws in the coefficient bialgebra; compatibility of the inverse maps is then automatic, and is supplied by TauCeti.FGComoduleCat.isoOfLinearEquiv. The coherence laws are inherited from SemimoduleCat along the faithful forgetful functor.

Main declarations

• TauCeti.FGComoduleCat.tensorUnit: the finitely generated trivial comodule on the base.
• TauCeti.FGComoduleCat.tensorAssociator, TauCeti.FGComoduleCat.tensorLeftUnitor, and TauCeti.FGComoduleCat.tensorRightUnitor: the coherence isomorphisms, together with the tensorAssociator_eq family identifying them with α_, λ_, and ρ_.
• MonoidalCategory (TauCeti.FGComoduleCat R C): the standard monoidal category structure.
• TauCeti.FGComoduleCat.tensorHom_tmul: tensor products of morphisms on pure tensors.
• TauCeti.FGComoduleCat.leftUnitor_hom_apply, TauCeti.FGComoduleCat.rightUnitor_hom_apply, and TauCeti.FGComoduleCat.associator_hom_apply: concrete formulas for the coherence maps.
• TauCeti.FGComoduleCat.leftUnitor_hom_toLinearMap, TauCeti.FGComoduleCat.rightUnitor_hom_toLinearMap, and TauCeti.FGComoduleCat.associator_hom_toLinearMap: the same formulas at the level of underlying linear maps, together with their inverse variants.

References

This is the monoidal-category part of Layer 1 of the Tau Ceti reductive-groups roadmap, ReductiveGroups/README.md in TauCetiRoadmap, which asks for the rigid monoidal category of finite-dimensional comodules. The construction is standard; see Sweedler, Hopf Algebras, Chapter 2. The categorical packaging follows Mathlib's monoidal structure on SemimoduleCat in Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic.

@[reducible, inline]

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

The tensor unit in finitely generated right comodules: the base semiring with the trivial coaction r ↦ r ⊗ 1.

Equations

• TauCeti.FGComoduleCat.tensorUnit R C = TauCeti.FGComoduleCat.of R

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

The associator on finitely generated comodules: the associativity equivalence of tensor products, which intertwines the diagonal coactions because the coefficient multiplication is associative. The user-facing form is α_, characterized by associator_hom_apply below.

Equations

• TauCeti.FGComoduleCat.tensorAssociator R C M N P = TauCeti.FGComoduleCat.isoOfLinearEquiv (TensorProduct.assoc R ↑M ↑N ↑P) ⋯

noncomputable def TauCeti.FGComoduleCat.tensorLeftUnitor (R : Type u) [CommSemiring R] (C : Type v) [Semiring C] [Bialgebra R C] (M : FGComoduleCat R C) : tensor R C (tensorUnit R C) M ≅ M

The left unitor on finitely generated comodules: the equivalence R ⊗ M ≃ M, which intertwines the diagonal coactions because 1 is a left unit for the coefficient multiplication. The user-facing form is λ_, characterized by leftUnitor_hom_apply below.

Equations

• TauCeti.FGComoduleCat.tensorLeftUnitor R C M = TauCeti.FGComoduleCat.isoOfLinearEquiv (TensorProduct.lid R ↑M) ⋯

noncomputable def TauCeti.FGComoduleCat.tensorRightUnitor (R : Type u) [CommSemiring R] (C : Type v) [Semiring C] [Bialgebra R C] (M : FGComoduleCat R C) : tensor R C M (tensorUnit R C) ≅ M

The right unitor on finitely generated comodules: the equivalence M ⊗ R ≃ M, which intertwines the diagonal coactions because 1 is a right unit for the coefficient multiplication. The user-facing form is ρ_, characterized by rightUnitor_hom_apply below.

Equations

• TauCeti.FGComoduleCat.tensorRightUnitor R C M = TauCeti.FGComoduleCat.isoOfLinearEquiv (TensorProduct.rid R ↑M) ⋯

@[instance_reducible]

noncomputable instance TauCeti.FGComoduleCat.instMonoidalCategoryStruct (R : Type u) [CommSemiring R] (C : Type v) [Semiring C] [Bialgebra R C] : CategoryTheory.MonoidalCategoryStruct (FGComoduleCat R C)

The tensor product, trivial unit, associator, and unitors on finitely generated right comodules over a bialgebra.

Equations

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

@[instance_reducible]

noncomputable instance TauCeti.FGComoduleCat.instMonoidalCategory (R : Type u) [CommSemiring R] (C : Type v) [Semiring C] [Bialgebra R C] : CategoryTheory.MonoidalCategory (FGComoduleCat R C)

Finitely generated right comodules over a bialgebra form a monoidal category under the diagonal tensor product. Over a field, these are precisely finite-dimensional comodules.

Equations

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

@[simp]

theorem TauCeti.FGComoduleCat.tensorAssociator_eq {R : Type u} [CommSemiring R] {C : Type v} [Semiring C] [Bialgebra R C] {M N P : FGComoduleCat R C} : tensorAssociator R C M N P = CategoryTheory.MonoidalCategoryStruct.associator M N P

The monoidal associator is the named one. Rewriting in this direction sends the implementation name to the notation, where associator_hom_apply and associator_inv_apply take over.

@[simp]

theorem TauCeti.FGComoduleCat.tensorLeftUnitor_eq {R : Type u} [CommSemiring R] {C : Type v} [Semiring C] [Bialgebra R C] {M : FGComoduleCat R C} : tensorLeftUnitor R C M = CategoryTheory.MonoidalCategoryStruct.leftUnitor M

The monoidal left unitor is the named one; see tensorAssociator_eq.

@[simp]

theorem TauCeti.FGComoduleCat.tensorRightUnitor_eq {R : Type u} [CommSemiring R] {C : Type v} [Semiring C] [Bialgebra R C] {M : FGComoduleCat R C} : tensorRightUnitor R C M = CategoryTheory.MonoidalCategoryStruct.rightUnitor M

The monoidal right unitor is the named one; see tensorAssociator_eq.

@[simp]

theorem TauCeti.FGComoduleCat.tensorHom_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') : (CategoryTheory.MonoidalCategoryStruct.tensorHom f g).hom.toLinearMap = TensorProduct.map f.hom.toLinearMap g.hom.toLinearMap

The monoidal tensor product of two finite-comodule morphisms is their ordinary tensor product on underlying linear maps.

@[simp]

theorem TauCeti.FGComoduleCat.tensorHom_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 (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)) (m ⊗ₜ[R] n) = (CategoryTheory.ConcreteCategory.hom f) m ⊗ₜ[R] (CategoryTheory.ConcreteCategory.hom g) n

The monoidal tensor product of finite-comodule morphisms acts componentwise on pure tensors.

@[simp]

theorem TauCeti.FGComoduleCat.leftUnitor_hom_apply {R : Type u} [CommSemiring R] {C : Type v} [Semiring C] [Bialgebra R C] {M : FGComoduleCat R C} (r : R) (m : ↑M) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).hom) (r ⊗ₜ[R] m) = r • m

The left unitor acts by scalar multiplication.

@[simp]

theorem TauCeti.FGComoduleCat.leftUnitor_inv_apply {R : Type u} [CommSemiring R] {C : Type v} [Semiring C] [Bialgebra R C] {M : FGComoduleCat R C} (m : ↑M) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).inv) m = 1 ⊗ₜ[R] m

The inverse left unitor sends m to 1 ⊗ m.

@[simp]

theorem TauCeti.FGComoduleCat.rightUnitor_hom_apply {R : Type u} [CommSemiring R] {C : Type v} [Semiring C] [Bialgebra R C] {M : FGComoduleCat R C} (m : ↑M) (r : R) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).hom) (m ⊗ₜ[R] r) = r • m

The right unitor acts by scalar multiplication.

@[simp]

theorem TauCeti.FGComoduleCat.rightUnitor_inv_apply {R : Type u} [CommSemiring R] {C : Type v} [Semiring C] [Bialgebra R C] {M : FGComoduleCat R C} (m : ↑M) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).inv) m = m ⊗ₜ[R] 1

The inverse right unitor sends m to m ⊗ 1.

@[simp]

theorem TauCeti.FGComoduleCat.associator_hom_apply {R : Type u} [CommSemiring R] {C : Type v} [Semiring C] [Bialgebra R C] {M N P : FGComoduleCat R C} (m : ↑M) (n : ↑N) (p : ↑P) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator M N P).hom) (m ⊗ₜ[R] n ⊗ₜ[R] p) = m ⊗ₜ[R] (n ⊗ₜ[R] p)

The associator sends (m ⊗ n) ⊗ p to m ⊗ (n ⊗ p).

@[simp]

theorem TauCeti.FGComoduleCat.associator_inv_apply {R : Type u} [CommSemiring R] {C : Type v} [Semiring C] [Bialgebra R C] {M N P : FGComoduleCat R C} (m : ↑M) (n : ↑N) (p : ↑P) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator M N P).inv) (m ⊗ₜ[R] (n ⊗ₜ[R] p)) = m ⊗ₜ[R] n ⊗ₜ[R] p

The inverse associator sends m ⊗ (n ⊗ p) to (m ⊗ n) ⊗ p.

@[simp]

theorem TauCeti.FGComoduleCat.associator_hom_toLinearMap {R : Type u} [CommSemiring R] {C : Type v} [Semiring C] [Bialgebra R C] {M N P : FGComoduleCat R C} : (CategoryTheory.MonoidalCategoryStruct.associator M N P).hom.hom.toLinearMap = ↑(TensorProduct.assoc R ↑M ↑N ↑P)

The associator has the associativity equivalence of tensor products underneath.

@[simp]

theorem TauCeti.FGComoduleCat.associator_inv_toLinearMap {R : Type u} [CommSemiring R] {C : Type v} [Semiring C] [Bialgebra R C] {M N P : FGComoduleCat R C} : (CategoryTheory.MonoidalCategoryStruct.associator M N P).inv.hom.toLinearMap = ↑(TensorProduct.assoc R ↑M ↑N ↑P).symm

The inverse associator has the inverse associativity equivalence underneath.

@[simp]

theorem TauCeti.FGComoduleCat.leftUnitor_hom_toLinearMap {R : Type u} [CommSemiring R] {C : Type v} [Semiring C] [Bialgebra R C] {M : FGComoduleCat R C} : (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).hom.hom.toLinearMap = ↑(TensorProduct.lid R ↑M)

The left unitor has the left tensor identity underneath.

@[simp]

theorem TauCeti.FGComoduleCat.leftUnitor_inv_toLinearMap {R : Type u} [CommSemiring R] {C : Type v} [Semiring C] [Bialgebra R C] {M : FGComoduleCat R C} : (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).inv.hom.toLinearMap = ↑(TensorProduct.lid R ↑M).symm

The inverse left unitor has the inverse left tensor identity underneath.

@[simp]

theorem TauCeti.FGComoduleCat.rightUnitor_hom_toLinearMap {R : Type u} [CommSemiring R] {C : Type v} [Semiring C] [Bialgebra R C] {M : FGComoduleCat R C} : (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).hom.hom.toLinearMap = ↑(TensorProduct.rid R ↑M)

The right unitor has the right tensor identity underneath.

@[simp]

theorem TauCeti.FGComoduleCat.rightUnitor_inv_toLinearMap {R : Type u} [CommSemiring R] {C : Type v} [Semiring C] [Bialgebra R C] {M : FGComoduleCat R C} : (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).inv.hom.toLinearMap = ↑(TensorProduct.rid R ↑M).symm

The inverse right unitor has the inverse right tensor identity underneath.