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.

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

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

Equations
Instances For
    @[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)] :

    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.
    Instances For
      @[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] :

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

      Equations
      Instances For
        @[simp]
        theorem Action.diagonal_V (G : Type u) [Monoid G] (n : ) :
        (Action.diagonal G n).V = (Fin nG)
        @[simp]
        theorem Action.diagonal_ρ_apply (G : Type u) [Monoid G] (n : ) :
        ∀ (x : (MonCat.of G)) (x_1 : Fin nG) (a : Fin n), (Action.diagonal G n) x x_1 a = (x x_1) a
        def Action.diagonal (G : Type u) [Monoid G] (n : ) :

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

        Equations
        Instances For

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

          Equations
          Instances For

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

            Equations
            Instances For
              @[simp]
              theorem Action.FintypeCat.ofMulAction_apply {G : Type u} {H : FintypeCat} [Monoid G] [MulAction G H] (g : G) (x : H) :
              Equations
              Equations
              • X.instMulActionαMonoidFintypeVFintypeCat = X.instMulAction
              Equations
              • X.instMulActionαFintypeVFintypeCat = X.instMulAction