Theorems · Definition · group theory

TannakaDuality.FiniteGroup.algHomOfRightFDRepComp

{k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] → [Finite G] → CategoryTheory.Aut (TannakaDuality.FiniteGroup.forget k G) → (G → k) →ₐ[k] G → k

The rightFDRep component of η : Aut (forget k G) gives rise to an algebra morphism (G → k) →ₐ[k] (G → k).

Defined in

Mathlib.RepresentationTheory.Tannaka

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingGroupFinite