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.

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

• Action.ofMulAction G H = { V := H, ρ := MulAction.toEndHom }

@[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

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.

@[simp]

theorem Action.leftRegular_ρ_apply (G : Type u) [Monoid G] : ∀ (x : ↑(MonCat.of G)) (x_1 : G), (Action.leftRegular G).ρ x x_1 = x * x_1

@[simp]

theorem Action.leftRegular_V (G : Type u) [Monoid G] : (Action.leftRegular G).V = G

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

• Action.leftRegular G = Action.ofMulAction G G

@[simp]

theorem Action.diagonal_ρ_apply (G : Type u) [Monoid G] (n : ℕ) : ∀ (x : ↑(MonCat.of G)) (x_1 : Fin n → G) (a : Fin n), (Action.diagonal G n).ρ x x_1 a = (x • x_1) a

@[simp]

theorem Action.diagonal_V (G : Type u) [Monoid G] (n : ℕ) : (Action.diagonal G n).V = (Fin n → G)

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

• Action.diagonal G n = Action.ofMulAction G (Fin n → G)

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

• Action.diagonalOneIsoLeftRegular G = Action.mkIso (Equiv.toIso (Equiv.funUnique (Fin 1) G)) ⋯

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

• Action.FintypeCat.ofMulAction G H = { V := H, ρ := MulAction.toEndHom }

@[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

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

• Action.instMulAction X = MulAction.mk ⋯ ⋯

instance Action.instMulActionαMonoidFintypeVFintypeCatInstCategoryFintypeCatInstMonoidα {G : MonCat} (X : Action FintypeCat G) : MulAction ↑G ↑X.V

Equations

• Action.instMulActionαMonoidFintypeVFintypeCatInstCategoryFintypeCatInstMonoidα X = Action.instMulAction X

instance Action.instMulActionαFintypeVFintypeCatInstCategoryFintypeCatOfToMonoidToDivInvMonoid {G : Type u} [Group G] (X : Action FintypeCat (MonCat.of G)) : MulAction G ↑X.V

Equations

• Action.instMulActionαFintypeVFintypeCatInstCategoryFintypeCatOfToMonoidToDivInvMonoid X = Action.instMulAction X