Diagonalizable bialgebras

We define diagonalizable bialgebras (over a commutative ring R) as those that are isomorphic to a group algebra over R.

We then prove that any diagonalizable bialgebra is spanned by its group-like elements.

If the base ring is a domain, we prove the converse: any bialgebra spanned by its group-like elements is diagonalizable. The idea is that, if A is a bialgebra over R and G is its set of group-like elements, then G is a group (for the multiplication of A), so we get a morphism of algebras from R[G] to A, which is actually a morphism of bialgebras. This morphism is surjective by assumption, and, if R is a domain, it is also injective because group-like elements are linearly independent.

Note that the last result is false in general.

class Bialgebra.IsDiagonalisable (R : Type u_1) (A : Type u) [CommRing R] [Semiring A] [Bialgebra R A] : Prop

A bialgebra is called diagonalisable if it is isomorphic to a group algebra.

• existsIso : ∃ (G : Type u) (x : Group G), Nonempty (A ≃ₐc[R] MonoidAlgebra R G)

theorem Bialgebra.isDiagonalisable_iff (R : Type u_1) (A : Type u) [CommRing R] [Semiring A] [Bialgebra R A] : IsDiagonalisable R A ↔ ∃ (G : Type u) (x : Group G), Nonempty (A ≃ₐc[R] MonoidAlgebra R G)

instance Bialgebra.instIsDiagonalisableMonoidAlgebra {R : Type u_1} {G : Type u_2} [CommRing R] [Group G] : IsDiagonalisable R (MonoidAlgebra R G)

A group algebra is diagonalisable.

instance Bialgebra.instIsDiagonalisableOfSubsingleton {R : Type u_1} {A : Type u} [CommRing R] [Semiring A] [Bialgebra R A] [Subsingleton R] : IsDiagonalisable R A

theorem Bialgebra.IsDiagonalisable.ofBialgEquiv {R : Type u_1} {A : Type u} [CommRing R] [Semiring A] [Bialgebra R A] {B : Type u_3} [Semiring B] [Bialgebra R B] [hA : IsDiagonalisable R A] (e : A ≃ₐc[R] B) : IsDiagonalisable R B

instance Bialgebra.instIsDiagonalisable {R : Type u_1} [CommRing R] : IsDiagonalisable R R

theorem Bialgebra.span_isGroupLikeElem_eq_top_of_isDiagonalisable {R : Type u_1} {A : Type u} [CommRing R] [Semiring A] [Bialgebra R A] : IsDiagonalisable R A → Submodule.span R {a : A | IsGroupLikeElem R a} = ⊤

A diagonalisable bialgebra is generated by its group-like elements.

theorem Bialgebra.liftGroupLikeBialgHom_bijective_of_span_isGroupLikeElem_eq_top {R : Type u_1} {A : Type u_2} [CommRing R] [IsDomain R] [Ring A] [HopfAlgebra R A] [NoZeroSMulDivisors R A] (h : Submodule.span R {a : A | IsGroupLikeElem R a} = ⊤) : Function.Bijective ⇑(MonoidAlgebra.liftGroupLikeBialgHom R A)

A Hopf algebra over a domain that is generated by its group-like elements is isomorphic to the group algebra on its group-like elements.

theorem Bialgebra.IsDiagonalisable.of_span_isGroupLikeElem_eq_top {R : Type u_1} {A : Type u_2} [CommRing R] [IsDomain R] [Ring A] [HopfAlgebra R A] [NoZeroSMulDivisors R A] (h : Submodule.span R {a : A | IsGroupLikeElem R a} = ⊤) : IsDiagonalisable R A

A Hopf algebra over a domain that is generated by its group-like elements is diagonalisable.

This is also true over a commutative ring, but with a more complicated proof.

theorem Bialgebra.isDiagonalisable_iff_span_isGroupLikeElem_eq_top {R : Type u_1} {A : Type u_2} [CommRing R] [IsDomain R] [Ring A] [HopfAlgebra R A] [NoZeroSMulDivisors R A] : IsDiagonalisable R A ↔ Submodule.span R {a : A | IsGroupLikeElem R a} = ⊤

A Hopf algebra over a domain is diagonalizable if and only if it is generated by its group-like elements.

This is also true over a commutative ring, but with a more complicated proof.