Theorems · Definition · group theory

TannakaDuality.FiniteGroup.ofRightFDRep

{k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      [inst_2 : Finite G] → [Fintype G] → (X : FDRep k G) → ↑X.V → (TannakaDuality.FiniteGroup.rightFDRep ⟶ X)

For v : X and G a finite group, the representation morphism from the right regular representation rightFDRep to X sending single 1 1 to v.

Defined in

Mathlib.RepresentationTheory.Tannaka

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingGroupFiniteFintype