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

• Action.ofMulAction G H = { V := H, ρ := MonCat.ofHom MulAction.toEndHom }

@[simp]

theorem Action.ofMulAction_apply {G H : Type u} [Monoid G] [MulAction G H] (g : G) (x : H) : (CategoryTheory.ConcreteCategory.hom (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)] : CategoryTheory.Limits.LimitCone (CategoryTheory.Discrete.functor fun (i : ι) => 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.

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

• Action.leftRegular G = Action.ofMulAction G G

@[simp]

theorem Action.leftRegular_ρ_hom_apply (G : Type u) [Monoid G] (x1✝ x2✝ : G) : (MonCat.Hom.hom (leftRegular G).ρ) x1✝ x2✝ = x1✝ * x2✝

@[simp]

theorem Action.leftRegular_V (G : Type u) [Monoid G] : (leftRegular G).V = G

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

• Action.diagonal G n = Action.ofMulAction G (Fin n → G)

@[simp]

theorem Action.diagonal_V (G : Type u) [Monoid G] (n : ℕ) : (diagonal G n).V = (Fin n → G)

@[simp]

theorem Action.diagonal_ρ_hom_apply (G : Type u) [Monoid G] (n : ℕ) (x1✝ : G) (x2✝ : Fin n → G) (a✝ : Fin n) : (MonCat.Hom.hom (diagonal G n).ρ) x1✝ x2✝ a✝ = x1✝ * x2✝ a✝

def Action.diagonalOneIsoLeftRegular (G : Type u) [Monoid G] : diagonal G 1 ≅ leftRegular G

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

Equations

• Action.diagonalOneIsoLeftRegular G = Action.mkIso (Equiv.funUnique (Fin 1) G).toIso ⋯

instance Action.FintypeCat.instMulActionαFintypeOf (G : Type u_1) (X : Type u_2) [Monoid G] [MulAction G X] [Fintype X] : MulAction G ↑(FintypeCat.of X)

If X is a type with [Fintype X] and G acts on X, then G also acts on FintypeCat.of X.

Equations

• Action.FintypeCat.instMulActionαFintypeOf G X = inferInstanceAs (MulAction G X)

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

• Action.FintypeCat.ofMulAction G H = { V := H, ρ := MonCat.ofHom MulAction.toEndHom }

@[simp]

theorem Action.FintypeCat.ofMulAction_apply {G : Type u} {H : FintypeCat} [Monoid G] [MulAction G ↑H] (g : G) (x : ↑H) : (CategoryTheory.ConcreteCategory.hom (ofMulAction G H).ρ) g x = g • x

def Action.FintypeCat.«term_⧸ₐ_» : Lean.TrailingParserDescr

Shorthand notation for the quotient of G by H as a finite G-set.

Equations

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

def Action.FintypeCat.toEndHom {G : Type u_1} [Group G] (N : Subgroup G) [Fintype (G ⧸ N)] [N.Normal] : G →* CategoryTheory.End (ofMulAction G (FintypeCat.of (G ⧸ N)))

If N is a normal subgroup of G, then this is the group homomorphism sending an element g of G to the G-endomorphism of G ⧸ₐ N given by multiplication with g⁻¹ on the right.

Equations

• Action.FintypeCat.toEndHom N = { toFun := fun (v : G) => { hom := Quotient.lift (fun (σ : G) => ⟦σ * v⁻¹⟧) ⋯, comm := ⋯ }, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Action.FintypeCat.toEndHom_apply {G : Type u_1} [Group G] (N : Subgroup G) [Fintype (G ⧸ N)] [N.Normal] (g h : G) : ((toEndHom N) g).hom ⟦h⟧ = ⟦h * g⁻¹⟧

theorem Action.FintypeCat.toEndHom_trivial_of_mem {G : Type u_1} [Group G] {N : Subgroup G} [Fintype (G ⧸ N)] [N.Normal] {n : G} (hn : n ∈ N) : (toEndHom N) n = CategoryTheory.CategoryStruct.id (ofMulAction G (FintypeCat.of (G ⧸ N)))

def Action.FintypeCat.quotientToEndHom {G : Type u_1} [Group G] (H N : Subgroup G) [Fintype (G ⧸ N)] [N.Normal] : ↥H ⧸ N.subgroupOf H →* CategoryTheory.End (ofMulAction G (FintypeCat.of (G ⧸ N)))

If H and N are subgroups of a group G with N normal, there is a canonical group homomorphism H ⧸ N ⊓ H to the G-endomorphisms of G ⧸ N.

Equations

• Action.FintypeCat.quotientToEndHom H N = QuotientGroup.lift (N.subgroupOf H) ((Action.FintypeCat.toEndHom N).comp H.subtype) ⋯

@[simp]

theorem Action.FintypeCat.quotientToEndHom_mk {G : Type u_1} [Group G] (H N : Subgroup G) [Fintype (G ⧸ N)] [N.Normal] (x : ↥H) (g : G) : ((quotientToEndHom H N) ⟦x⟧).hom ⟦g⟧ = ⟦g * ↑x⁻¹⟧

def Action.FintypeCat.quotientToQuotientOfLE {G : Type u_1} [Group G] (H N : Subgroup G) [Fintype (G ⧸ N)] [Fintype (G ⧸ H)] (h : N ≤ H) : ofMulAction G (FintypeCat.of (G ⧸ N)) ⟶ ofMulAction G (FintypeCat.of (G ⧸ H))

If N and H are subgroups of a group G with N ≤ H, this is the canonical G-morphism G ⧸ N ⟶ G ⧸ H.

Equations

• Action.FintypeCat.quotientToQuotientOfLE H N h = { hom := Quotient.lift (fun (x : G) => ⟦x⟧) ⋯, comm := ⋯ }

@[simp]

theorem Action.FintypeCat.quotientToQuotientOfLE_hom_mk {G : Type u_1} [Group G] (H N : Subgroup G) [Fintype (G ⧸ N)] [Fintype (G ⧸ H)] (h : N ≤ H) (x : G) : (quotientToQuotientOfLE H N h).hom ⟦x⟧ = ⟦x⟧

instance Action.instMulAction {V : Type (u + 1)} [CategoryTheory.LargeCategory V] [CategoryTheory.HasForget V] {G : MonCat} (X : Action V G) : MulAction (↑G) ((CategoryTheory.forget (Action V G)).obj X)

Equations

• X.instMulAction = MulAction.mk ⋯ ⋯

instance Action.instMulActionCarrierαFintypeVFintypeCat {G : MonCat} (X : Action FintypeCat G) : MulAction ↑G ↑X.V

Equations

• X.instMulActionCarrierαFintypeVFintypeCat = X.instMulAction

instance Action.instMulActionαFintypeVFintypeCat {G : Type u} [Group G] (X : Action FintypeCat (MonCat.of G)) : MulAction G ↑X.V

Equations

• X.instMulActionαFintypeVFintypeCat = X.instMulAction