Constructors for Action V G for some concrete categories

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

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.

Equations

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

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

Equations

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

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

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

Equations

• Action.leftRegular G = Action.ofMulAction G G

@[simp]

theorem Action.leftRegular_ρ_apply (G : Type u) [Monoid G] (x1✝ x2✝ : G) : (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) 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_ρ_apply (G : Type u) [Monoid G] (n : ℕ) (x1✝ : G) (x2✝ : Fin n → G) (a✝ : Fin n) : (diagonal G n).ρ x1✝ x2✝ a✝ = x1✝ * x2✝ a✝

@[simp]

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

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.

Equations

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

instance Action.FintypeCat.instMulActionCarrierOf (G : Type u_1) (X : Type u_2) [Monoid G] [MulAction G X] [Fintype X] : MulAction G (FintypeCat.of X).carrier

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

Equations

• Action.FintypeCat.instMulActionCarrierOf G X = inferInstanceAs (MulAction G 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.

Equations

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

@[simp]

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

Equations

• X.instMulAction = { smul := fun (g : G) (x : CategoryTheory.ToType X) => (CategoryTheory.ConcreteCategory.hom (X.ρ g)) x, one_smul := ⋯, mul_smul := ⋯ }

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

Equations

• X.instMulActionCarrierVFintypeCat = X.instMulAction