Theorems · Definition · category theory

Action.FintypeCat.quotientToEndHom

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

Defined in

Mathlib.CategoryTheory.Action.Concrete

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupFintypeSubgroup.Normal