The regular comodule

This file packages the regular right comodule of a coalgebra as a bundled object of ComoduleCat, and, when the coalgebra is finitely generated as a module, as an object of FGComoduleCat. It also records the canonical morphism from the group-like comodule on the rank-one free module R into the regular comodule, and multiplication of a bialgebra as a morphism from the tensor square of its regular comodule.

This is Layer 1 infrastructure for the Tau Ceti reductive-groups roadmap target "Comodules over a coalgebra/Hopf algebra", specifically the regular-representation part of the finitely generated comodule category.

Main definitions

• TauCeti.ComoduleCat.regular: the bundled regular right comodule.
• TauCeti.Comodule.Hom.groupLikeToRegular: the map r ↦ r • g from the group-like comodule on R into the regular comodule.
• TauCeti.Comodule.Hom.trivialToRegular: the bialgebraic special case g = 1.
• TauCeti.Comodule.Hom.regularMul: bialgebra multiplication as a morphism from the tensor square of the regular comodule.
• TauCeti.FGComoduleCat.regular: the regular comodule as a finitely generated comodule, when the underlying coalgebra is finitely generated as an R-module.

References

This is the standard regular right comodule of a coalgebra; see Sweedler, Hopf Algebras, Chapter 2. The group-like morphisms reuse Mathlib's GroupLike API, and the multiplication morphism reuses Bialgebra.mulCoalgHom.

def TauCeti.Comodule.Hom.groupLikeToRegular {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (g : GroupLike R C) : Hom R C R C

The canonical morphism from the group-like comodule on R attached to g into the regular comodule, sending r to r • g.

Equations

• TauCeti.Comodule.Hom.groupLikeToRegular g = { toLinearMap := LinearMap.toSpanSingleton R C ↑g, map_coact := ⋯ }

@[simp]

theorem TauCeti.Comodule.Hom.groupLikeToRegular_toLinearMap {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (g : GroupLike R C) : (groupLikeToRegular g).toLinearMap = LinearMap.toSpanSingleton R C ↑g

The underlying linear map of groupLikeToRegular g sends r to r • g.

@[simp]

theorem TauCeti.Comodule.Hom.groupLikeToRegular_apply {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (g : GroupLike R C) (r : R) : (groupLikeToRegular g) r = r • ↑g

The morphism groupLikeToRegular g sends r to r • g.

def TauCeti.Comodule.Hom.trivialToRegular {R : Type u} {C : Type v} [CommSemiring R] [Semiring C] [Bialgebra R C] : Hom R C R C

The canonical morphism from the trivial comodule on R to the regular comodule of a bialgebra, induced by the unit map R → C.

Equations

• TauCeti.Comodule.Hom.trivialToRegular = TauCeti.Comodule.Hom.groupLikeToRegular 1

@[simp]

theorem TauCeti.Comodule.Hom.trivialToRegular_toLinearMap {R : Type u} {C : Type v} [CommSemiring R] [Semiring C] [Bialgebra R C] : trivialToRegular.toLinearMap = Algebra.linearMap R C

The underlying linear map of trivialToRegular is Algebra.linearMap R C.

@[simp]

theorem TauCeti.Comodule.Hom.trivialToRegular_apply {R : Type u} {C : Type v} [CommSemiring R] [Semiring C] [Bialgebra R C] (r : R) : trivialToRegular r = (algebraMap R C) r

The morphism trivialToRegular sends r to algebraMap R C r.

noncomputable def TauCeti.Comodule.Hom.regularMul {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [Bialgebra R H] : Hom R H (TensorProduct R H H) H

Multiplication of a bialgebra, regarded as a morphism from the tensor square of its regular right comodule to the regular right comodule.

Equations

• TauCeti.Comodule.Hom.regularMul = { toLinearMap := LinearMap.mul' R H, map_coact := ⋯ }

@[simp]

theorem TauCeti.Comodule.Hom.regularMul_toLinearMap {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [Bialgebra R H] : regularMul.toLinearMap = LinearMap.mul' R H

The underlying linear map of regular-comodule multiplication is bialgebra multiplication.

@[simp]

theorem TauCeti.Comodule.Hom.regularMul_tmul {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [Bialgebra R H] (x y : H) : regularMul (x ⊗ₜ[R] y) = x * y

Regular-comodule multiplication sends a pure tensor to the product of its factors.

@[reducible, inline]

abbrev TauCeti.ComoduleCat.regular (R : Type u) (C : Type v) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] : ComoduleCat R C

The regular right comodule, bundled as an object of ComoduleCat.

Equations

• TauCeti.ComoduleCat.regular R C = TauCeti.ComoduleCat.of R C C

@[simp]

theorem TauCeti.ComoduleCat.regular_toSemimoduleCat (R : Type u) (C : Type v) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] : (regular R C).toSemimoduleCat = ↧C

The underlying type of the bundled regular comodule is the coalgebra itself.

@[simp]

theorem TauCeti.ComoduleCat.regular_coact (R : Type u) (C : Type v) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] : Comodule.coact = CoalgebraStruct.comul

The coaction on the bundled regular comodule is the coalgebra comultiplication.

@[reducible, inline]

abbrev TauCeti.ComoduleCat.groupLikeToRegular {R C : Type u} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (g : GroupLike R C) : of R C R ⟶ regular R C

The categorical morphism from the group-like comodule on R into the regular comodule.

Equations

• TauCeti.ComoduleCat.groupLikeToRegular g = TauCeti.Comodule.Hom.groupLikeToRegular g

@[simp]

theorem TauCeti.ComoduleCat.groupLikeToRegular_apply {R C : Type u} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (g : GroupLike R C) (r : R) : (CategoryTheory.ConcreteCategory.hom (groupLikeToRegular g)) r = r • ↑g

The bundled morphism groupLikeToRegular g sends r to r • g.

@[reducible, inline]

abbrev TauCeti.ComoduleCat.trivialToRegular {R C : Type u} [CommSemiring R] [Semiring C] [Bialgebra R C] : trivial R C ⟶ regular R C

The categorical morphism from the bundled trivial comodule into the regular comodule.

Equations

• TauCeti.ComoduleCat.trivialToRegular = TauCeti.Comodule.Hom.trivialToRegular

theorem TauCeti.ComoduleCat.trivialToRegular_apply {R C : Type u} [CommSemiring R] [Semiring C] [Bialgebra R C] (r : R) : (CategoryTheory.ConcreteCategory.hom trivialToRegular) r = (algebraMap R C) r

The bundled morphism trivialToRegular sends r to algebraMap R C r.

@[reducible, inline]

abbrev TauCeti.FGComoduleCat.regular (R : Type u) (C : Type v) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Finite R C] : FGComoduleCat R C

The regular right comodule, bundled as a finitely generated comodule when the coalgebra is finitely generated as an R-module.

Equations

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

@[simp]

theorem TauCeti.FGComoduleCat.regular_obj (R : Type u) (C : Type v) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Finite R C] : (regular R C).obj = ComoduleCat.regular R C

The ambient comodule underlying the finitely generated regular comodule is the regular comodule.

@[simp]

theorem TauCeti.FGComoduleCat.regular_coact (R : Type u) (C : Type v) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Finite R C] : Comodule.coact = CoalgebraStruct.comul

The coaction on the finitely generated regular comodule is the coalgebra comultiplication.