Theorems · Definition · group theory

TannakaDuality.FiniteGroup.sumSMulInv

{k G : Type u} → [inst : CommRing k] → [inst_1 : Group G] → [Fintype G] → {X : FDRep k G} → ↑X.V → (G → k) →ₗ[k] ↑X.V

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

Defined in

Mathlib.RepresentationTheory.Tannaka

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingGroupFintype