The group algebra functor

We show that, for a domain R, G ↦ R[G] forms a fully faithful functor from commutative groups to commutative R-Hopf algebras.

noncomputable def commMonAlg (R : Type u_1) [CommRing R] : CategoryTheory.Functor CommMonCat (CommBialgCat R)

The functor of commutative monoid algebras.

Equations

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

@[simp]

theorem commMonAlg_obj (R : Type u_1) [CommRing R] (M : CommMonCat) : (commMonAlg R).obj M = CommBialgCat.of R (MonoidAlgebra R ↑M)

@[simp]

theorem commMonAlg_map (R : Type u_1) [CommRing R] {X✝ Y✝ : CommMonCat} (f : X✝ ⟶ Y✝) : (commMonAlg R).map f = CommBialgCat.ofHom (MonoidAlgebra.mapDomainBialgHom R (CommMonCat.Hom.hom f))

noncomputable def commGrpAlg (R : Type u_1) [CommRing R] : CategoryTheory.Functor CommGrpCat (CommHopfAlgCat R)

The functor of commutative group algebras.

Equations

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

@[simp]

theorem commGrpAlg_obj (R : Type u_1) [CommRing R] (G : CommGrpCat) : (commGrpAlg R).obj G = CommHopfAlgCat.of R (MonoidAlgebra R ↑G)

@[simp]

theorem commGrpAlg_map (R : Type u_1) [CommRing R] {X✝ Y✝ : CommGrpCat} (f : X✝ ⟶ Y✝) : (commGrpAlg R).map f = CommHopfAlgCat.ofHom (MonoidAlgebra.mapDomainBialgHom R (CommGrpCat.Hom.hom f))

instance commMonAlg.instFaithful {R : Type u_1} [CommRing R] [Nontrivial R] : (commMonAlg R).Faithful

instance commGrpAlg.instFaithful {R : Type u_1} [CommRing R] [Nontrivial R] : (commGrpAlg R).Faithful

noncomputable def commGrpAlg.fullyFaithful {R : Type u_1} [CommRing R] [IsDomain R] : (commGrpAlg R).FullyFaithful

The group algebra functor over a domain is fully faithful.

Equations

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

instance commGrpAlg.instFull {R : Type u_1} [CommRing R] [IsDomain R] : (commGrpAlg R).Full