Constructors for Action V G for some concrete categories

We construct Action (Type*) G from a [MulAction G X] instance and give some applications.

@[simp]

theorem Action.ρ_inv_self_apply {G : Type u} [Group G] {A : Action (Type u) G} (g : G) (x : A.V) : A.ρ g⁻¹ (A.ρ g x) = x

@[simp]

theorem Action.ρ_self_inv_apply {G : Type u} [Group G] {A : Action (Type u) G} (g : G) (x : A.V) : A.ρ g (A.ρ g⁻¹ x) = x

def Action.ofMulAction (G : Type u_1) (H : Type u) [Monoid G] [MulAction G H] : Action (Type u) G

Bundles a type H with a multiplicative action of G as an Action.

theorem Action.ofMulAction_ρ (G : Type u_1) (H : Type u) [Monoid G] [MulAction G H] : (ofMulAction G H).ρ = MulAction.toEndHom

theorem Action.ofMulAction_V (G : Type u_1) (H : Type u) [Monoid G] [MulAction G H] : (ofMulAction G H).V = H

@[simp]

theorem Action.ofMulAction_apply {G : Type u_1} {H : Type u_2} [Monoid G] [MulAction G H] (g : G) (x : H) : (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.

@[reducible, inline]

abbrev Action.leftRegular (G : Type u) [Monoid G] : Action (Type u) G

The G-set G, acting on itself by left multiplication.

@[reducible, inline]

abbrev Action.diagonal (G : Type u) [Monoid G] (n : ℕ) : Action (Type u) G

The G-set Gⁿ, acting on itself by left multiplication.

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

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

instance Action.FintypeCat.instMulActionCarrierOf (G : Type u_1) (X : Type u_2) [Monoid G] [MulAction G X] [Fintype X] : MulAction G { carrier := X, str := inst✝ }.carrier

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

def Action.FintypeCat.ofMulAction (G : Type u_1) (H : FintypeCat) [Monoid G] [MulAction G H.carrier] : Action FintypeCat G

Bundles a finite type H with a multiplicative action of G as an Action.

@[simp]

theorem Action.FintypeCat.ofMulAction_apply {G : Type u_1} {H : FintypeCat} [Monoid G] [MulAction G H.carrier] (g : G) (x : H.carrier) : (CategoryTheory.ConcreteCategory.hom (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.

def Action.FintypeCat.toEndHom {G : Type u_1} [Group G] (N : Subgroup G) [Fintype (G ⧸ N)] [N.Normal] : G →* CategoryTheory.End (ofMulAction G { carrier := G ⧸ N, str := inst✝ })

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.

@[simp]

theorem Action.FintypeCat.toEndHom_apply {G : Type u_1} [Group G] (N : Subgroup G) [Fintype (G ⧸ N)] [N.Normal] (g h : G) : (CategoryTheory.ConcreteCategory.hom ((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 { carrier := G ⧸ N, str := inst✝ })

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 { carrier := G ⧸ N, str := inst✝ })

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.

@[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) : (CategoryTheory.ConcreteCategory.hom ((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 { carrier := G ⧸ N, str := inst✝ } ⟶ ofMulAction G { carrier := G ⧸ H, str := inst✝¹ }

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

@[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) : (CategoryTheory.ConcreteCategory.hom (quotientToQuotientOfLE H N h).hom) ⟦x⟧ = ⟦x⟧

instance Action.instMulAction {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {FV : V → V → Type u_1} {CV : V → Type u_2} [(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] [CategoryTheory.ConcreteCategory V FV] {G : Type u_3} [Monoid G] (X : Action V G) : MulAction G (CategoryTheory.ToType X)

instance Action.instMulActionCarrierVFintypeCat {G : Type u_3} [Monoid G] (X : Action FintypeCat G) : MulAction G X.V.carrier