Theorems · Definition · category theory

Action.FintypeCat.quotientToQuotientOfLE

{G : Type u_1} →
  [inst : Group G] →
    (H N : Subgroup G) →
      [inst_1 : Fintype (G ⧸ N)] →
        [inst_2 : Fintype (G ⧸ H)] →
          N ≤ H →
            (Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ N)) ⟶
              Action.FintypeCat.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.

Defined in

Mathlib.CategoryTheory.Action.Concrete

Cited by

2 results in Mathlib

Foundations

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

Assumes

GroupFintypeFintype