Theorems · Definition · group theory

MulAction.equivSubgroupOrbits

{G : Type u} →
  (X : Type v) →
    [inst : Group G] →
      [inst_1 : MulAction G X] →
        (H : Subgroup G) →
          MulAction.orbitRel.Quotient (↥H) X ≃
            (ω : Quotient (MulAction.orbitRel G X)) ×
              MulAction.orbitRel.Quotient ↥H ↑(MulAction.orbitRel.Quotient.orbit ω)

A bijection between the orbits under the action of a subgroup H on X, and the orbits under the action of H on each orbit under the action of G.

Defined in

Mathlib.GroupTheory.GroupAction.Quotient

Cited by

0 results in Mathlib

Foundations

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

Assumes

GroupMulAction