Theorems · Definition · category theory
Action.V
{V : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} V] → {G : Type u_2} → [inst_1 : Monoid G] → Action V G → VThe object this action acts on
- Defined in
- Mathlib.CategoryTheory.Action.Basic
- Cited by
- 176 results in Mathlib
- Foundations
- Depth 2 from the axioms, rests on 4 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- Monoidstatement and proof · cited by 3,887
- Actionstatement and proof · cited by 206
Cited by227
Results whose statement or proof uses this declaration.
- Action.Hom.homstatement · cited by 86
- Action.ρstatement · cited by 51
- Representation.linearizestatement · cited by 36
- CategoryTheory.Functor.mapActionproof · cited by 21
- FDRep.ρstatement and proof · cited by 20
- Action.forgetproof · cited by 17
- Action.resproof · cited by 17
- Representation.linearizeMapstatement and proof · cited by 15
- Action.mkIsostatement and proof · cited by 14
- Action.FunctorCategoryEquivalence.functorproof · cited by 14
- Representation.LinearizeMonoidal.μstatement and proof · cited by 13
- FDRep.characterproof · cited by 11
Showing the 200 most cited of 227.