Revision #1277 → #2287 · back to history
addedCayley's theoremc85ae5ad2cee
modifiedSemisimple action3ee25c6b77dd
| Field | From #1277 | To #2287 |
|---|
| mathlib.decl | IsSemisimpleRepresentation | Representation.IsSemisimpleRepresentation |
| note | `IsSemisimpleRepresentation` (equiv. `IsSemisimpleModule` over `k[G]`) is the semisimplicity of a linear action. | `Representation.IsSemisimpleRepresentation ρ` (equivalent to `IsSemisimpleModule` over `MonoidAlgebra k G`) is the semisimplicity of a linear action. |
addedKernel of action equals intersection of stabilizers4db33c37e8bd
modifiedCategory of G-sets398a7ba11287
| Field | From #1277 | To #2287 |
|---|
| mathlib.decl | CategoryTheory.Action | Action |
| note | `Action (Type u) G` is the category of G-sets (the docstring notes `V = Type` gives G-actions). | `Action (Type u) G` is the category of G-sets (specializing the general `Action V G` structure to `V = Type u`). |
modifiedAction groupoid4198f868bafc
| Field | From #1277 | To #2287 |
|---|
| note | `CategoryTheory.ActionCategory M X` is the action groupoid (groupoid when `M` is a group). | `CategoryTheory.ActionCategory M X` is the action groupoid (a groupoid when `M` is a group). |
modifiedG-sets form a Grothendieck toposae9878fa8096
| Field | From #1277 | To #2287 |
|---|
| mathlib.decl | CategoryTheory.Action | Action |
modifiedActions on objects of a categorycf85ae469760
| Field | From #1277 | To #2287 |
|---|
| mathlib.decl | CategoryTheory.Action | Action |