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.

def CategoryTheory.actionAsFunctor (M : Type u_1) [Monoid M] (X : Type u) [MulAction M X] : Functor (SingleObj M) (Type u)

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.

@[simp]

theorem CategoryTheory.actionAsFunctor_map (M : Type u_1) [Monoid M] (X : Type u) [MulAction M X] {X✝ Y✝ : SingleObj M} (x1✝ : X✝ ⟶ Y✝) (x2✝ : X) : (actionAsFunctor M X).map x1✝ x2✝ = x1✝ • x2✝

@[simp]

theorem CategoryTheory.actionAsFunctor_obj (M : Type u_1) [Monoid M] (X : Type u) [MulAction M X] (x✝ : SingleObj M) : (actionAsFunctor M X).obj x✝ = X

def CategoryTheory.ActionCategory (M : Type u_1) [Monoid M] (X : Type u) [MulAction M X] : Type 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

• CategoryTheory.ActionCategory M X = (CategoryTheory.actionAsFunctor M X).Elements

instance CategoryTheory.instCategoryActionCategory (M : Type u_1) [Monoid M] (X : Type u) [MulAction M X] : Category.{u_1, u} (ActionCategory M X)

Equations

• CategoryTheory.instCategoryActionCategory M X = id inferInstance

def CategoryTheory.ActionCategory.π (M : Type u_1) [Monoid M] (X : Type u) [MulAction M X] : Functor (ActionCategory M X) (SingleObj M)

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

Equations

• CategoryTheory.ActionCategory.π M X = CategoryTheory.CategoryOfElements.π (CategoryTheory.actionAsFunctor M X)

@[simp]

theorem CategoryTheory.ActionCategory.π_map (M : Type u_1) [Monoid M] (X : Type u) [MulAction M X] (p q : ActionCategory M X) (f : p ⟶ q) : (π M X).map f = ↑f

@[simp]

theorem CategoryTheory.ActionCategory.π_obj (M : Type u_1) [Monoid M] (X : Type u) [MulAction M X] (p : ActionCategory M X) : (π M X).obj p = SingleObj.star M

def CategoryTheory.ActionCategory.back {M : Type u_1} [Monoid M] {X : Type u} [MulAction M X] : ActionCategory M X → X

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

instance CategoryTheory.ActionCategory.instCoeTC {M : Type u_1} [Monoid M] {X : Type u} [MulAction M X] : CoeTC X (ActionCategory M X)

Equations

• CategoryTheory.ActionCategory.instCoeTC = { coe := fun (x : X) => ⟨(), x⟩ }

@[simp]

theorem CategoryTheory.ActionCategory.coe_back {M : Type u_1} [Monoid M] {X : Type u} [MulAction M X] (x : X) : ActionCategory.back ⟨(), x⟩ = x

@[simp]

theorem CategoryTheory.ActionCategory.back_coe {M : Type u_1} [Monoid M] {X : Type u} [MulAction M X] (x : ActionCategory M X) : ⟨(), x.back⟩ = x

def CategoryTheory.ActionCategory.objEquiv (M : Type u_1) [Monoid M] (X : Type u) [MulAction M X] : X ≃ ActionCategory M X

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

Equations

• CategoryTheory.ActionCategory.objEquiv M X = { toFun := fun (x : X) => ⟨(), x⟩, invFun := fun (x : CategoryTheory.ActionCategory M X) => x.back, left_inv := ⋯, right_inv := ⋯ }

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

instance CategoryTheory.ActionCategory.instInhabited (M : Type u_1) [Monoid M] (X : Type u) [MulAction M X] [Inhabited X] : Inhabited (ActionCategory M X)

Equations

• CategoryTheory.ActionCategory.instInhabited M X = { default := let_fun this := default; ⟨(), this⟩ }

instance CategoryTheory.ActionCategory.instNonempty (M : Type u_1) [Monoid M] (X : Type u) [MulAction M X] [Nonempty X] : Nonempty (ActionCategory M X)

def CategoryTheory.ActionCategory.stabilizerIsoEnd (M : Type u_1) [Monoid M] {X : Type u} [MulAction M X] (x : X) : ↥(MulAction.stabilizerSubmonoid M x) ≃* End ⟨(), x⟩

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

Equations

• CategoryTheory.ActionCategory.stabilizerIsoEnd M x = MulEquiv.refl ↥(MulAction.stabilizerSubmonoid M x)

@[simp]

theorem CategoryTheory.ActionCategory.stabilizerIsoEnd_apply (M : Type u_1) [Monoid M] {X : Type u} [MulAction M X] (x : X) (f : ↥(MulAction.stabilizerSubmonoid M x)) : (stabilizerIsoEnd M x) f = f

@[simp]

theorem CategoryTheory.ActionCategory.stabilizerIsoEnd_symm_apply (M : Type u_1) [Monoid M] {X : Type u} [MulAction M X] (x : X) (f : End ⟨(), x⟩) : (stabilizerIsoEnd M x).symm f = f

@[simp]

theorem CategoryTheory.ActionCategory.id_val {M : Type u_1} [Monoid M] {X : Type u} [MulAction M X] (x : ActionCategory M X) : ↑(CategoryStruct.id x) = 1

@[simp]

theorem CategoryTheory.ActionCategory.comp_val {M : Type u_1} [Monoid M] {X : Type u} [MulAction M X] {x y z : ActionCategory M X} (f : x ⟶ y) (g : y ⟶ z) : ↑(CategoryStruct.comp f g) = ↑g * ↑f

instance CategoryTheory.ActionCategory.instIsConnectedOfIsPretransitiveOfNonempty {M : Type u_1} [Monoid M] {X : Type u} [MulAction M X] [MulAction.IsPretransitive M X] [Nonempty X] : IsConnected (ActionCategory M X)

instance CategoryTheory.ActionCategory.instGroupoid {X : Type u} {G : Type u_2} [Group G] [MulAction G X] : Groupoid (ActionCategory G X)

Equations

• CategoryTheory.ActionCategory.instGroupoid = CategoryTheory.groupoidOfElements (CategoryTheory.actionAsFunctor G X)

def CategoryTheory.ActionCategory.endMulEquivSubgroup {G : Type u_2} [Group G] (H : Subgroup G) : End ((objEquiv G (G ⧸ H)) ↑1) ≃* ↥H

Any subgroup of G is a vertex group in its action groupoid.

Equations

• CategoryTheory.ActionCategory.endMulEquivSubgroup H = (CategoryTheory.ActionCategory.stabilizerIsoEnd G ↑1).symm.trans (MulEquiv.subgroupCongr ⋯)

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

• CategoryTheory.ActionCategory.homOfPair t g = ⟨g, ⋯⟩

@[simp]

theorem CategoryTheory.ActionCategory.homOfPair.val {X : Type u} {G : Type u_2} [Group G] [MulAction G X] (t : X) (g : G) : ↑(homOfPair t g) = g

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

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

Equations

• CategoryTheory.ActionCategory.cases hyp f = cast ⋯ (hyp b.back ↑f)

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

def CategoryTheory.ActionCategory.curry {X : Type u} {G : Type u_2} [Group G] [MulAction G X] {H : Type u_3} [Group H] (F : Functor (ActionCategory G X) (SingleObj H)) : G →* (X → H) ⋊[mulAutArrow] G

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

• CategoryTheory.ActionCategory.curry F = { toFun := fun (g : G) => { left := fun (b : X) => F.map (CategoryTheory.ActionCategory.homOfPair b g), right := g }, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem CategoryTheory.ActionCategory.curry_apply_right {X : Type u} {G : Type u_2} [Group G] [MulAction G X] {H : Type u_3} [Group H] (F : Functor (ActionCategory G X) (SingleObj H)) (g : G) : ((curry F) g).right = g

@[simp]

theorem CategoryTheory.ActionCategory.curry_apply_left {X : Type u} {G : Type u_2} [Group G] [MulAction G X] {H : Type u_3} [Group H] (F : Functor (ActionCategory G X) (SingleObj H)) (g : G) (b : X) : ((curry F) g).left b = F.map (homOfPair b g)

def CategoryTheory.ActionCategory.uncurry {X : Type u} {G : Type u_2} [Group G] [MulAction G X] {H : Type u_3} [Group H] (F : G →* (X → H) ⋊[mulAutArrow] G) (sane : ∀ (g : G), (F g).right = g) : Functor (ActionCategory G X) (SingleObj H)

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.

@[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 →* (X → H) ⋊[mulAutArrow] G) (sane : ∀ (g : G), (F g).right = g) {x✝ b : ActionCategory G X} (f : x✝ ⟶ b) : (uncurry F sane).map f = (F ↑f).left b.back

@[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 →* (X → H) ⋊[mulAutArrow] G) (sane : ∀ (g : G), (F g).right = g) (x✝ : ActionCategory G X) : (uncurry F sane).obj x✝ = ()