Theorems · Theorem · group theory

TannakaDuality.FiniteGroup.ofRightFDRep_hom

∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Finite G] [inst_3 : Fintype G] (X : FDRep k G)
  (v : ↑X.V),
  (TannakaDuality.FiniteGroup.ofRightFDRep X v).hom =
    CategoryTheory.InducedCategory.homMk (ModuleCat.ofHom (TannakaDuality.FiniteGroup.sumSMulInv v))

Defined in: Mathlib.RepresentationTheory.Tannaka
Cited by: 1 results in Mathlib
Foundations: Depth 88 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing Group Finite Fintype

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites21

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Quiver.Homstatement · cited by 32,603
CommRingstatement and proof · cited by 17,173
Fintypestatement and proof · cited by 7,736
Groupstatement and proof · cited by 6,238
Finitestatement and proof · cited by 3,029
ModuleCatstatement · cited by 1,429
CategoryTheory.ObjectProperty.FullSubcategory.objstatement · cited by 1,316
ModuleCat.carrierstatement · cited by 997
CategoryTheory.ObjectProperty.FullSubcategorystatement · cited by 726
ModuleCat.ofHomstatement · cited by 200
Action.Vstatement and proof · cited by 176
Action.Hom.homstatement and proof · cited by 86

Cited by1

Results whose statement or proof uses this declaration.

TannakaDuality.FiniteGroup.toRightFDRepComp_injectiveproof · cited by 1