Star coalgebras

A star coalgebra is a coalgebra A over a commutative star ring R, carrying a conjugate-linear involution star, whose comultiplication is a star map: Δ(a*) = Δ(a)*, where the tensor square carries the star structure (x ⊗ y)* = x* ⊗ y*. Together with a compatible star algebra structure this is the defining condition of a Hopf star algebra, the algebraic shadow of a compact quantum group.

The counit is then automatically a star map, ε(a*) = conj (ε a): starring the counit law for a* exhibits a ↦ conj (ε (a*)) as a left counit, and a left counit agrees with the right counit ε.

Main declarations

• TauCeti.StarCoalgebra: the comultiplication commutes with the star operation.
• Coalgebra.Repr.star: starring both legs of a representation of Δ a represents Δ (a*).
• TauCeti.StarCoalgebra.counit_star: the counit of a star coalgebra is a star map.

References

• A. Klimyk and K. Schmüdgen, Quantum Groups and Their Representations, Springer, 1997, Section 1.2.7.

class TauCeti.StarCoalgebra (R : Type u_1) (A : Type u_2) [CommSemiring R] [StarRing R] [AddCommMonoid A] [StarAddMonoid A] [Module R A] [StarModule R A] [CoalgebraStruct R A] : Prop

A star coalgebra: a coalgebra over a commutative star ring, with a conjugate-linear star operation, whose comultiplication commutes with star, Δ(a*) = Δ(a)*.

• comul_star (a : A) : CoalgebraStruct.comul (star a) = star (CoalgebraStruct.comul a)

  The comultiplication commutes with the star operation.

def Coalgebra.Repr.star {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [AddCommMonoid A] [StarAddMonoid A] [Module R A] [StarModule R A] [CoalgebraStruct R A] [TauCeti.StarCoalgebra R A] {a : A} {ι : Type u_3} (𝓡 : Repr R a ι) : Repr R (Star.star a) ι

Starring both legs of a representation Δ a = ∑ xᵢ ⊗ yᵢ gives the representation Δ (a*) = ∑ xᵢ* ⊗ yᵢ*.

@[simp]

theorem Coalgebra.Repr.star_index {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [AddCommMonoid A] [StarAddMonoid A] [Module R A] [StarModule R A] [CoalgebraStruct R A] [TauCeti.StarCoalgebra R A] {a : A} {ι : Type u_3} (𝓡 : Repr R a ι) : 𝓡.star.index = 𝓡.index

@[simp]

theorem Coalgebra.Repr.star_left {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [AddCommMonoid A] [StarAddMonoid A] [Module R A] [StarModule R A] [CoalgebraStruct R A] [TauCeti.StarCoalgebra R A] {a : A} {ι : Type u_3} (𝓡 : Repr R a ι) (i : ι) : 𝓡.star.left i = Star.star (𝓡.left i)

@[simp]

theorem Coalgebra.Repr.star_right {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [AddCommMonoid A] [StarAddMonoid A] [Module R A] [StarModule R A] [CoalgebraStruct R A] [TauCeti.StarCoalgebra R A] {a : A} {ι : Type u_3} (𝓡 : Repr R a ι) (i : ι) : 𝓡.star.right i = Star.star (𝓡.right i)

@[simp]

theorem TauCeti.StarCoalgebra.counit_star {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [AddCommMonoid A] [StarAddMonoid A] [Module R A] [StarModule R A] [Coalgebra R A] [StarCoalgebra R A] (a : A) : CoalgebraStruct.counit (star a) = star (CoalgebraStruct.counit a)

The counit of a star coalgebra is a star map: ε(a*) = conj (ε a).