Theorems · Definition · category theory

Action.FintypeCat.toEndHom

{G : Type u_1} →
  [inst : Group G] →
    (N : Subgroup G) →
      [inst_1 : Fintype (G ⧸ N)] →
        [N.Normal] → G →* CategoryTheory.End (Action.FintypeCat.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.

Defined in

Mathlib.CategoryTheory.Action.Concrete

Cited by

2 results in Mathlib

Foundations

Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupFintypeSubgroup.Normal