Theorems · Definition · ring theory

MonoidAlgebra.mapDomainBialgHomEquiv

{R : Type u_1} →
  {G : Type u_5} →
    {H : Type u_6} →
      [inst : CommRing R] →
        [IsDomain R] → [inst_2 : Group G] → [inst_3 : Group H] → (G →* H) ≃ (MonoidAlgebra R G →ₐc[R] MonoidAlgebra R H)

The equivalence between group homs G → H and bialgebra homs R[G] → R[H] of group algebras over a domain.

Defined in

Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Cited by

3 results in Mathlib

Foundations

Depth 121 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsDomainGroupGroup