Documentation

Mathlib.CategoryTheory.Action

Actions as functors and as categories #

From a multiplicative action M ↻ X, we can construct a functor from M to the category of types, mapping the single object of M to X and an element m : M to map X → X given by multiplication by m. This functor induces a category structure on X -- a special case of the category of elements. A morphism x ⟶ y in this category is simply a scalar m : M such that m • x = y. In the case where M is a group, this category is a groupoid -- the action groupoid.

@[simp]
theorem CategoryTheory.actionAsFunctor_map (M : Type u_1) [Monoid M] (X : Type u) [MulAction M X] :
∀ {X_1 Y : CategoryTheory.SingleObj M} (x1 : X_1 Y) (x2 : X), (CategoryTheory.actionAsFunctor M X).map x1 x2 = x1 x2
@[simp]

A multiplicative action M ↻ X viewed as a functor mapping the single object of M to X and an element m : M to the map X → X given by multiplication by m.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    def CategoryTheory.ActionCategory (M : Type u_1) [Monoid M] (X : Type u) [MulAction M X] :
    Type (max 0 u)

    A multiplicative action M ↻ X induces a category structure on X, where a morphism from x to y is a scalar taking x to y. Due to implementation details, the object type of this category is not equal to X, but is in bijection with X.

    Equations
    Instances For

      The projection from the action category to the monoid, mapping a morphism to its label.

      Equations
      Instances For

        The canonical map ActionCategory M X → X. It is given by fun x => x.snd, but has a more explicit type.

        Equations
        • x.back = x.snd
        Instances For
          Equations
          • CategoryTheory.ActionCategory.instCoeTC = { coe := fun (x : X) => (), x }
          @[simp]
          @[simp]
          theorem CategoryTheory.ActionCategory.back_coe {M : Type u_1} [Monoid M] {X : Type u} [MulAction M X] (x : CategoryTheory.ActionCategory M X) :
          (), x.back = x

          An object of the action category given by M ↻ X corresponds to an element of X.

          Equations
          Instances For
            theorem CategoryTheory.ActionCategory.hom_as_subtype (M : Type u_1) [Monoid M] (X : Type u) [MulAction M X] (p : CategoryTheory.ActionCategory M X) (q : CategoryTheory.ActionCategory M X) :
            (p q) = { m : M // m p.back = q.back }
            Equations

            The stabilizer of a point is isomorphic to the endomorphism monoid at the corresponding point. In fact they are definitionally equivalent.

            Equations
            Instances For
              def CategoryTheory.ActionCategory.homOfPair {X : Type u} {G : Type u_2} [Group G] [MulAction G X] (t : X) (g : G) :
              (), g⁻¹ t (), t

              A target vertex t and a scalar g determine a morphism in the action groupoid.

              Equations
              Instances For
                @[simp]
                theorem CategoryTheory.ActionCategory.homOfPair.val {X : Type u} {G : Type u_2} [Group G] [MulAction G X] (t : X) (g : G) :
                def CategoryTheory.ActionCategory.cases {X : Type u} {G : Type u_2} [Group G] [MulAction G X] {P : a b : CategoryTheory.ActionCategory G X⦄ → (a b)Sort u_3} (hyp : (t : X) → (g : G) → P (CategoryTheory.ActionCategory.homOfPair t g)) ⦃a : CategoryTheory.ActionCategory G X ⦃b : CategoryTheory.ActionCategory G X (f : a b) :
                P f

                Any morphism in the action groupoid is given by some pair.

                Equations
                Instances For
                  theorem CategoryTheory.ActionCategory.cases' {X : Type u} {G : Type u_2} [Group G] [MulAction G X] ⦃a' : CategoryTheory.ActionCategory G X ⦃b' : CategoryTheory.ActionCategory G X (f : a' b') :
                  ∃ (a : X) (b : X) (g : G) (ha : a' = (), a) (hb : b' = (), b) (hg : a = g⁻¹ b), f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ActionCategory.homOfPair b g) (CategoryTheory.eqToHom ))

                  Given G acting on X, a functor from the corresponding action groupoid to a group H can be curried to a group homomorphism G →* (X → H) ⋊ G.

                  Equations
                  Instances For
                    @[simp]
                    theorem CategoryTheory.ActionCategory.uncurry_obj {X : Type u} {G : Type u_2} [Group G] [MulAction G X] {H : Type u_3} [Group H] (F : G →* (XH) ⋊[mulAutArrow] G) (sane : ∀ (g : G), (F g).right = g) :
                    @[simp]
                    theorem CategoryTheory.ActionCategory.uncurry_map {X : Type u} {G : Type u_2} [Group G] [MulAction G X] {H : Type u_3} [Group H] (F : G →* (XH) ⋊[mulAutArrow] G) (sane : ∀ (g : G), (F g).right = g) :
                    ∀ {x b : CategoryTheory.ActionCategory G X} (f : x b), (CategoryTheory.ActionCategory.uncurry F sane).map f = (F f).left b.back
                    def CategoryTheory.ActionCategory.uncurry {X : Type u} {G : Type u_2} [Group G] [MulAction G X] {H : Type u_3} [Group H] (F : G →* (XH) ⋊[mulAutArrow] G) (sane : ∀ (g : G), (F g).right = g) :

                    Given G acting on X, a group homomorphism φ : G →* (X → H) ⋊ G can be uncurried to a functor from the action groupoid to H, provided that φ g = (_, g) for all g.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For