Theorems · Definition · group theory
FDRep
(R : Type u) → (G : Type v) → [Ring R] → [Monoid G] → Type (max (max (u + 1) v) u)
The category of finitely generated R-linear representations of a monoid G.
Note that R can be any ring,
but the main case of interest is when R = k is a field and G is a group.
- Defined in
- Mathlib.RepresentationTheory.FDRep
- Cited by
- 33 results in Mathlib
- Foundations
- Depth 28 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Ringstatement and proof · cited by 7,463
- Monoidstatement and proof · cited by 3,887
- Actionproof · cited by 206
- FGModuleCatproof · cited by 52
Cited by51
Results whose statement or proof uses this declaration.
- FDRep.ρstatement and proof · cited by 20
- FDRep.characterstatement and proof · cited by 11
- TannakaDuality.FiniteGroup.forgetstatement and proof · cited by 9
- FDRep.ofstatement · cited by 8
- TannakaDuality.FiniteGroup.rightFDRepstatement · cited by 6
- TannakaDuality.FiniteGroup.equivAppstatement and proof · cited by 4
- TannakaDuality.FiniteGroup.equivHomstatement · cited by 3
- TannakaDuality.FiniteGroup.sumSMulInvstatement and proof · cited by 3
- FDRep.isoToLinearEquivstatement and proof · cited by 2
- FDRep.scalar_product_char_eq_finrank_equivariantstatement and proof · cited by 2
- TannakaDuality.FiniteGroup.algHomOfRightFDRepCompstatement · cited by 2
- TannakaDuality.FiniteGroup.ofRightFDRepstatement and proof · cited by 2