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] : CategoryTheory.Functor (CategoryTheory.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_1 Y : CategoryTheory.SingleObj M} (x1 : X_1 ⟶ Y) (x2 : X), (CategoryTheory.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 : CategoryTheory.SingleObj M), (CategoryTheory.actionAsFunctor M X).obj x = X

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

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

instance CategoryTheory.instCategoryActionCategory (M : Type u_1) [Monoid M] (X : Type u) [MulAction M X] : CategoryTheory.Category.{u_1, u} (CategoryTheory.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] : CategoryTheory.Functor (CategoryTheory.ActionCategory M X) (CategoryTheory.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 : CategoryTheory.ActionCategory M X) (q : CategoryTheory.ActionCategory M X) (f : p ⟶ q) : (CategoryTheory.ActionCategory.π M X).map f = ↑f

@[simp]

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

def CategoryTheory.ActionCategory.back {M : Type u_1} [Monoid M] {X : Type u} [MulAction M X] : CategoryTheory.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 (CategoryTheory.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) : CategoryTheory.ActionCategory.back ⟨(), x⟩ = x

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

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

Equations

• ⋯ = ⋯

def CategoryTheory.ActionCategory.stabilizerIsoEnd (M : Type u_1) [Monoid M] {X : Type u} [MulAction M X] (x : X) : ↥(MulAction.stabilizerSubmonoid M x) ≃* CategoryTheory.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)) : (CategoryTheory.ActionCategory.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 : CategoryTheory.End ⟨(), x⟩) : (CategoryTheory.ActionCategory.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 : CategoryTheory.ActionCategory M X) : ↑(CategoryTheory.CategoryStruct.id x) = 1

@[simp]

theorem CategoryTheory.ActionCategory.comp_val {M : Type u_1} [Monoid M] {X : Type u} [MulAction M X] {x : CategoryTheory.ActionCategory M X} {y : CategoryTheory.ActionCategory M X} {z : CategoryTheory.ActionCategory M X} (f : x ⟶ y) (g : y ⟶ z) : ↑(CategoryTheory.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] : CategoryTheory.IsConnected (CategoryTheory.ActionCategory M X)

Equations

• ⋯ = ⋯

instance CategoryTheory.ActionCategory.instGroupoid {X : Type u} {G : Type u_2} [Group G] [MulAction G X] : CategoryTheory.Groupoid (CategoryTheory.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) : CategoryTheory.End ((CategoryTheory.ActionCategory.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) : ↑(CategoryTheory.ActionCategory.homOfPair t 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

• 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' : 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 ⋯))

def CategoryTheory.ActionCategory.curry {X : Type u} {G : Type u_2} [Group G] [MulAction G X] {H : Type u_3} [Group H] (F : CategoryTheory.Functor (CategoryTheory.ActionCategory G X) (CategoryTheory.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 : CategoryTheory.Functor (CategoryTheory.ActionCategory G X) (CategoryTheory.SingleObj H)) (g : G) : ((CategoryTheory.ActionCategory.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 : CategoryTheory.Functor (CategoryTheory.ActionCategory G X) (CategoryTheory.SingleObj H)) (g : G) (b : X) : ((CategoryTheory.ActionCategory.curry F) g).left b = F.map (CategoryTheory.ActionCategory.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) : CategoryTheory.Functor (CategoryTheory.ActionCategory G X) (CategoryTheory.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 : CategoryTheory.ActionCategory G X} (f : x ⟶ b), (CategoryTheory.ActionCategory.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 : CategoryTheory.ActionCategory G X), (CategoryTheory.ActionCategory.uncurry F sane).obj x = ()