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
Instances For
    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.
    Instances For
      source
      @[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
      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
      Instances For
        source
        @[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
        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
        Instances For
          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
          Instances For
            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
            Instances For
              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
              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)).toPrefunctor.obj X)
              Equations
              • One or more equations did not get rendered due to their size.
              source
              instance Action.instMulActionαMonoidFintypeVFintypeCatInstCategoryFintypeCatInstMonoidα {G : MonCat} (X : Action FintypeCat G) :
              MulAction ↑G ↑X.V
              Equations
              source
              instance Action.instMulActionαFintypeVFintypeCatInstCategoryFintypeCatOfToMonoidToDivInvMonoid {G : Type u} [Group G] (X : Action FintypeCat (MonCat.of G)) :
              MulAction G ↑X.V
              Equations