Theorems · Definition · group theory

AddAction.equivAddSubgroupOrbits

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

A bijection between the orbits under the action of an additive 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 78 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddGroupAddAction