Documentation

Mathlib.RepresentationTheory.Action.Concrete

Constructors for Action V G for some concrete categories #

We construct Action (Type u) G from a [MulAction G X] instance and give some applications.

source
def Action.ofMulAction (G : Type u) (H : Type u) [Monoid G] [MulAction G H] :
Action (Type u) (MonCat.of G)

Bundles a type H with a multiplicative action of G as an Action.

Equations
source
@[simp]
theorem Action.ofMulAction_apply {G : Type u} {H : Type u} [Monoid G] [MulAction G H] (g : G) (x : H) :
(Action.ofMulAction G H).ρ g x = g • x
source
def Action.ofMulActionLimitCone {ι : Type v} (G : Type (max v u)) [Monoid G] (F : ι → Type (max v u)) [(i : ι) → MulAction G (F i)] :
CategoryTheory.Limits.LimitCone (CategoryTheory.Discrete.functor fun (i : ι) => Action.ofMulAction G (F i))

Given a family F of types with G-actions, this is the limit cone demonstrating that the product of F as types is a product in the category of G-sets.

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem Action.leftRegular_ρ_apply (G : Type u) [Monoid G] :
∀ (x1 : ↑(MonCat.of G)) (x2 : G), (Action.leftRegular G).ρ x1 x2 = x1 * x2
source
@[simp]
theorem Action.leftRegular_V (G : Type u) [Monoid G] :
(Action.leftRegular G).V = G
source
def Action.leftRegular (G : Type u) [Monoid G] :
Action (Type u) (MonCat.of G)

The G-set G, acting on itself by left multiplication.

Equations
source
@[simp]
theorem Action.diagonal_ρ_apply (G : Type u) [Monoid G] (n : ℕ) :
∀ (x1 : ↑(MonCat.of G)) (x2 : Fin n → G) (a : Fin n), (Action.diagonal G n).ρ x1 x2 a = (x1 • x2) a
source
@[simp]
theorem Action.diagonal_V (G : Type u) [Monoid G] (n : ℕ) :
(Action.diagonal G n).V = (Fin n → G)
source
def Action.diagonal (G : Type u) [Monoid G] (n : ℕ) :
Action (Type u) (MonCat.of G)

The G-set Gⁿ, acting on itself by left multiplication.

Equations
source
def Action.diagonalOneIsoLeftRegular (G : Type u) [Monoid G] :
Action.diagonal G 1 ≅ Action.leftRegular G

We have Fin 1 → G ≅ G as G-sets, with G acting by left multiplication.

Equations
source
instance Action.FintypeCat.instMulActionαFintypeOf (G : Type u_1) (X : Type u_2) [Monoid G] [MulAction G X] [Fintype X] :
MulAction G ↑(FintypeCat.of X)

If X is a type with [Fintype X] and G acts on X, then G also acts on FintypeCat.of X.

Equations
source
def Action.FintypeCat.ofMulAction (G : Type u) (H : FintypeCat) [Monoid G] [MulAction G ↑H] :
Action FintypeCat (MonCat.of G)

Bundles a finite type H with a multiplicative action of G as an Action.

Equations
source
@[simp]
theorem Action.FintypeCat.ofMulAction_apply {G : Type u} {H : FintypeCat} [Monoid G] [MulAction G ↑H] (g : G) (x : ↑H) :
(Action.FintypeCat.ofMulAction G H).ρ g x = g • x
source
def Action.FintypeCat.«term_⧸ₐ_» :
Lean.TrailingParserDescr

Shorthand notation for the quotient of G by H as a finite G-set.

Equations
  • One or more equations did not get rendered due to their size.
source
def Action.FintypeCat.toEndHom {G : Type u_1} [Group G] (N : Subgroup G) [Fintype (G ⧸ N)] [N.Normal] :
G →* CategoryTheory.End (Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ N)))

If N is a normal subgroup of G, then this is the group homomorphism sending an element g of G to the G-endomorphism of G ⧸ₐ N given by multiplication with g⁻¹ on the right.

Equations
source
@[simp]
theorem Action.FintypeCat.toEndHom_apply {G : Type u_1} [Group G] (N : Subgroup G) [Fintype (G ⧸ N)] [N.Normal] (g : G) (h : G) :
((Action.FintypeCat.toEndHom N) g).hom ⟦h⟧ = ⟦h * g⁻¹⟧
source
theorem Action.FintypeCat.toEndHom_trivial_of_mem {G : Type u_1} [Group G] {N : Subgroup G} [Fintype (G ⧸ N)] [N.Normal] {n : G} (hn : n ∈ N) :
(Action.FintypeCat.toEndHom N) n = CategoryTheory.CategoryStruct.id (Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ N)))
source
def Action.FintypeCat.quotientToEndHom {G : Type u_1} [Group G] (H : Subgroup G) (N : Subgroup G) [Fintype (G ⧸ N)] [N.Normal] :
{ x : G // x ∈ H } ⧸ N.subgroupOf H →* CategoryTheory.End (Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ N)))

If H and N are subgroups of a group G with N normal, there is a canonical group homomorphism H ⧸ N ⊓ H to the G-endomorphisms of G ⧸ N.

Equations
source
@[simp]
theorem Action.FintypeCat.quotientToEndHom_mk {G : Type u_1} [Group G] (H : Subgroup G) (N : Subgroup G) [Fintype (G ⧸ N)] [N.Normal] (x : { x : G // x ∈ H }) (g : G) :
((Action.FintypeCat.quotientToEndHom H N) ⟦x⟧).hom ⟦g⟧ = ⟦g * ↑x⁻¹⟧
source
def Action.FintypeCat.quotientToQuotientOfLE {G : Type u_1} [Group G] (H : Subgroup G) (N : Subgroup G) [Fintype (G ⧸ N)] [Fintype (G ⧸ H)] (h : N ≤ H) :
Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ N)) ⟶ Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ H))

If N and H are subgroups of a group G with N ≤ H, this is the canonical G-morphism G ⧸ N ⟶ G ⧸ H.

Equations
source
@[simp]
theorem Action.FintypeCat.quotientToQuotientOfLE_hom_mk {G : Type u_1} [Group G] (H : Subgroup G) (N : Subgroup G) [Fintype (G ⧸ N)] [Fintype (G ⧸ H)] (h : N ≤ H) (x : G) :
(Action.FintypeCat.quotientToQuotientOfLE H N h).hom ⟦x⟧ = ⟦x⟧
source
instance Action.instMulAction {V : Type (u + 1)} [CategoryTheory.LargeCategory V] [CategoryTheory.ConcreteCategory V] {G : MonCat} (X : Action V G) :
MulAction (↑G) ((CategoryTheory.forget (Action V G)).obj X)
Equations
source
instance Action.instMulActionαMonoidFintypeVFintypeCat {G : MonCat} (X : Action FintypeCat G) :
MulAction ↑G ↑X.V
Equations
  • X.instMulActionαMonoidFintypeVFintypeCat = X.instMulAction
source
instance Action.instMulActionαFintypeVFintypeCat {G : Type u} [Group G] (X : Action FintypeCat (MonCat.of G)) :
MulAction G ↑X.V
Equations
  • X.instMulActionαFintypeVFintypeCat = X.instMulAction