Constructors for Action V G for some concrete categories

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

@[implicit_reducible]

instance TypeCat.instCoeFunEndForall (X : Type u) : CoeFun (CategoryTheory.End X) fun (x : CategoryTheory.End X) => X → X

Equations

• TypeCat.instCoeFunEndForall X = inferInstance

def TypeCat.endEquiv (X : Type u) : Function.End X ≃* CategoryTheory.End X

The group isomorphism between Function.End X and CategoryTheory.End X.

Equations

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

@[simp]

theorem TypeCat.endEquiv_symm_apply (X : Type u) (f : CategoryTheory.End X) (a : X) : (endEquiv X).symm f a = (CategoryTheory.ConcreteCategory.hom f) a

@[simp]

theorem TypeCat.endEquiv_apply (X : Type u) (f : Function.End X) : (endEquiv X) f = ofHom f

@[simp]

theorem Action.ρ_inv_self_apply {G : Type u} [Group G] {A : Action (Type u) G} (g : G) (x : A.V) : (CategoryTheory.ConcreteCategory.hom (A.ρ g⁻¹)) ((CategoryTheory.ConcreteCategory.hom (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) : (CategoryTheory.ConcreteCategory.hom (A.ρ g)) ((CategoryTheory.ConcreteCategory.hom (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.

Equations

• Action.ofMulAction G H = { V := H, ρ := (TypeCat.endEquiv H).toMonoidHom.comp MulAction.toEndHom }

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

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

@[simp]

theorem Action.ofMulAction_apply {G : Type u_1} {H : Type u_2} [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.

@[reducible, inline]

abbrev 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

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

Equations

• Action.diagonal G n = Action.ofMulAction G (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 ⋯

@[implicit_reducible]

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

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

Equations

• Action.FintypeCat.instMulActionObjFiniteOf G X = inst✝¹

def Action.FintypeCat.ofMulAction (G : Type u_1) (H : FintypeCat) [Monoid G] [MulAction G H.obj] : 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, ρ := CategoryTheory.InducedCategory.endEquiv.symm.toMonoidHom.comp ((TypeCat.endEquiv H.obj).toMonoidHom.comp MulAction.toEndHom) }

@[simp]

theorem Action.FintypeCat.ofMulAction_apply {G : Type u_1} {H : FintypeCat} [Monoid G] [MulAction G H.obj] (g : G) (x : H.obj) : (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 := FintypeCat.homMk (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) : (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 (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) : (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 (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 := FintypeCat.homMk (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) : (CategoryTheory.ConcreteCategory.hom (quotientToQuotientOfLE H N h).hom) ⟦x⟧ = ⟦x⟧

@[implicit_reducible]

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, mul_smul := ⋯, one_smul := ⋯ }

@[implicit_reducible]

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

Equations

• X.instMulActionObjFiniteVFintypeCat = X.instMulAction