Theorems · Theorem · group theory

TannakaDuality.FiniteGroup.map_mul_toRightFDRepComp

∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Finite G]
  (η : CategoryTheory.Aut (TannakaDuality.FiniteGroup.forget k G)) (f g : G → k),
  have α := ModuleCat.Hom.hom (η.hom.hom.app TannakaDuality.FiniteGroup.rightFDRep).hom;
  α (f * g) = α f * α g

The rightFDRep component of η : Aut (forget k G) preserves multiplication

Defined in

Mathlib.RepresentationTheory.Tannaka

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingGroupFinite