Documentation

Mathlib.GroupTheory.GroupAction.Quotient

Properties of group actions involving quotient groups #

This file proves properties of group actions which use the quotient group construction, notably

as well as their analogues for additive groups.

class MulAction.QuotientAction {α : Type u} (β : Type v) [Group α] [Monoid β] [MulAction β α] (H : Subgroup α) :

A typeclass for when a MulAction β α descends to the quotient α ⧸ H.

  • inv_mul_mem (b : β) {a a' : α} : a⁻¹ * a' H → (b a)⁻¹ * b a' H

    The action fulfils a normality condition on products that lie in H. This ensures that the action descends to an action on the quotient α ⧸ H.

Instances
    class AddAction.QuotientAction {α : Type u} (β : Type v) [AddGroup α] [AddMonoid β] [AddAction β α] (H : AddSubgroup α) :

    A typeclass for when an AddAction β α descends to the quotient α ⧸ H.

    • inv_mul_mem (b : β) {a a' : α} : -a + a' H-(b +ᵥ a) + (b +ᵥ a') H

      The action fulfils a normality condition on summands that lie in H. This ensures that the action descends to an action on the quotient α ⧸ H.

    Instances
      instance MulAction.quotient {α : Type u} (β : Type v) [Group α] [Monoid β] [MulAction β α] (H : Subgroup α) [QuotientAction β H] :
      MulAction β (α H)
      Equations
        instance AddAction.quotient {α : Type u} (β : Type v) [AddGroup α] [AddMonoid β] [AddAction β α] (H : AddSubgroup α) [QuotientAction β H] :
        AddAction β (α H)
        Equations
          @[simp]
          theorem MulAction.Quotient.smul_mk {α : Type u} {β : Type v} [Group α] [Monoid β] [MulAction β α] (H : Subgroup α) [QuotientAction β H] (b : β) (a : α) :
          b a = ↑(b a)
          @[simp]
          theorem AddAction.Quotient.vadd_mk {α : Type u} {β : Type v} [AddGroup α] [AddMonoid β] [AddAction β α] (H : AddSubgroup α) [QuotientAction β H] (b : β) (a : α) :
          b +ᵥ a = ↑(b +ᵥ a)
          @[simp]
          theorem MulAction.Quotient.smul_coe {α : Type u} {β : Type v} [Group α] [Monoid β] [MulAction β α] (H : Subgroup α) [QuotientAction β H] (b : β) (a : α) :
          b a = ↑(b a)
          @[simp]
          theorem AddAction.Quotient.vadd_coe {α : Type u} {β : Type v} [AddGroup α] [AddMonoid β] [AddAction β α] (H : AddSubgroup α) [QuotientAction β H] (b : β) (a : α) :
          b +ᵥ a = ↑(b +ᵥ a)
          @[simp]
          theorem MulAction.Quotient.mk_smul_out {α : Type u} {β : Type v} [Group α] [Monoid β] [MulAction β α] (H : Subgroup α) [QuotientAction β H] (b : β) (q : α H) :
          ↑(b Quotient.out q) = b q
          @[simp]
          theorem AddAction.Quotient.mk_vadd_out {α : Type u} {β : Type v} [AddGroup α] [AddMonoid β] [AddAction β α] (H : AddSubgroup α) [QuotientAction β H] (b : β) (q : α H) :
          ↑(b +ᵥ Quotient.out q) = b +ᵥ q
          theorem MulAction.Quotient.coe_smul_out {α : Type u} {β : Type v} [Group α] [Monoid β] [MulAction β α] (H : Subgroup α) [QuotientAction β H] (b : β) (q : α H) :
          ↑(b Quotient.out q) = b q
          theorem AddAction.Quotient.coe_vadd_out {α : Type u} {β : Type v} [AddGroup α] [AddMonoid β] [AddAction β α] (H : AddSubgroup α) [QuotientAction β H] (b : β) (q : α H) :
          ↑(b +ᵥ Quotient.out q) = b +ᵥ q
          theorem QuotientGroup.out_conj_pow_minimalPeriod_mem {α : Type u} [Group α] (H : Subgroup α) (a : α) (q : α H) :
          (Quotient.out q)⁻¹ * a ^ Function.minimalPeriod (fun (x : α H) => a x) q * Quotient.out q H
          def MulActionHom.toQuotient {α : Type u} [Group α] (H : Subgroup α) :
          α →ₑ[id] α H

          The canonical map to the left cosets.

          Equations
            Instances For
              @[simp]
              theorem MulActionHom.toQuotient_apply {α : Type u} [Group α] (H : Subgroup α) (g : α) :
              (toQuotient H) g = g
              instance MulAction.mulLeftCosetsCompSubtypeVal {α : Type u} [Group α] (H I : Subgroup α) :
              MulAction (↥I) (α H)
              Equations
                instance AddAction.addLeftCosetsCompSubtypeVal {α : Type u} [AddGroup α] (H I : AddSubgroup α) :
                AddAction (↥I) (α H)
                Equations
                  def MulAction.ofQuotientStabilizer (α : Type u) {β : Type v} [Group α] [MulAction α β] (x : β) (g : α stabilizer α x) :
                  β

                  The canonical map from the quotient of the stabilizer to the set.

                  Equations
                    Instances For
                      def AddAction.ofQuotientStabilizer (α : Type u) {β : Type v} [AddGroup α] [AddAction α β] (x : β) (g : α stabilizer α x) :
                      β

                      The canonical map from the quotient of the stabilizer to the set.

                      Equations
                        Instances For
                          @[simp]
                          theorem MulAction.ofQuotientStabilizer_mk (α : Type u) {β : Type v} [Group α] [MulAction α β] (x : β) (g : α) :
                          ofQuotientStabilizer α x g = g x
                          @[simp]
                          theorem AddAction.ofQuotientStabilizer_mk (α : Type u) {β : Type v} [AddGroup α] [AddAction α β] (x : β) (g : α) :
                          theorem MulAction.ofQuotientStabilizer_mem_orbit (α : Type u) {β : Type v} [Group α] [MulAction α β] (x : β) (g : α stabilizer α x) :
                          theorem AddAction.ofQuotientStabilizer_mem_orbit (α : Type u) {β : Type v} [AddGroup α] [AddAction α β] (x : β) (g : α stabilizer α x) :
                          theorem MulAction.ofQuotientStabilizer_smul (α : Type u) {β : Type v} [Group α] [MulAction α β] (x : β) (g : α) (g' : α stabilizer α x) :
                          theorem AddAction.ofQuotientStabilizer_vadd (α : Type u) {β : Type v} [AddGroup α] [AddAction α β] (x : β) (g : α) (g' : α stabilizer α x) :
                          noncomputable def MulAction.orbitEquivQuotientStabilizer (α : Type u) {β : Type v} [Group α] [MulAction α β] (b : β) :
                          (orbit α b) α stabilizer α b

                          Orbit-stabilizer theorem.

                          Equations
                            Instances For
                              noncomputable def AddAction.orbitEquivQuotientStabilizer (α : Type u) {β : Type v} [AddGroup α] [AddAction α β] (b : β) :
                              (orbit α b) α stabilizer α b

                              Orbit-stabilizer theorem.

                              Equations
                                Instances For
                                  noncomputable def MulAction.orbitProdStabilizerEquivGroup (α : Type u) {β : Type v} [Group α] [MulAction α β] (b : β) :
                                  (orbit α b) × (stabilizer α b) α

                                  Orbit-stabilizer theorem.

                                  Equations
                                    Instances For
                                      noncomputable def AddAction.orbitProdStabilizerEquivAddGroup (α : Type u) {β : Type v} [AddGroup α] [AddAction α β] (b : β) :
                                      (orbit α b) × (stabilizer α b) α

                                      Orbit-stabilizer theorem.

                                      Equations
                                        Instances For
                                          theorem MulAction.card_orbit_mul_card_stabilizer_eq_card_group (α : Type u) {β : Type v} [Group α] [MulAction α β] (b : β) [Fintype α] [Fintype (orbit α b)] [Fintype (stabilizer α b)] :

                                          Orbit-stabilizer theorem.

                                          theorem AddAction.card_orbit_mul_card_stabilizer_eq_card_addGroup (α : Type u) {β : Type v} [AddGroup α] [AddAction α β] (b : β) [Fintype α] [Fintype (orbit α b)] [Fintype (stabilizer α b)] :

                                          Orbit-stabilizer theorem.

                                          @[simp]
                                          theorem MulAction.orbitEquivQuotientStabilizer_symm_apply (α : Type u) {β : Type v} [Group α] [MulAction α β] (b : β) (a : α) :
                                          ((orbitEquivQuotientStabilizer α b).symm a) = a b
                                          @[simp]
                                          theorem AddAction.orbitEquivQuotientStabilizer_symm_apply (α : Type u) {β : Type v} [AddGroup α] [AddAction α β] (b : β) (a : α) :
                                          @[simp]
                                          theorem MulAction.stabilizer_quotient {G : Type u_1} [Group G] (H : Subgroup G) :
                                          stabilizer G 1 = H
                                          @[simp]
                                          theorem AddAction.stabilizer_quotient {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                          stabilizer G 0 = H
                                          noncomputable def MulAction.selfEquivSigmaOrbitsQuotientStabilizer' (α : Type u) (β : Type v) [Group α] [MulAction α β] {φ : Quotient (orbitRel α β)β} ( : Function.LeftInverse Quotient.mk'' φ) :
                                          β (ω : Quotient (orbitRel α β)) × α stabilizer α (φ ω)

                                          Class formula : given G a group acting on X and φ a function mapping each orbit of X under this action (that is, each element of the quotient of X by the relation orbitRel G X) to an element in this orbit, this gives a (noncomputable) bijection between X and the disjoint union of G/Stab(φ(ω)) over all orbits ω. In most cases you'll want φ to be Quotient.out, so we provide MulAction.selfEquivSigmaOrbitsQuotientStabilizer' as a special case.

                                          Equations
                                            Instances For
                                              noncomputable def AddAction.selfEquivSigmaOrbitsQuotientStabilizer' (α : Type u) (β : Type v) [AddGroup α] [AddAction α β] {φ : Quotient (orbitRel α β)β} ( : Function.LeftInverse Quotient.mk'' φ) :
                                              β (ω : Quotient (orbitRel α β)) × α stabilizer α (φ ω)

                                              Class formula : given G an additive group acting on X and φ a function mapping each orbit of X under this action (that is, each element of the quotient of X by the relation orbit_rel G X) to an element in this orbit, this gives a (noncomputable) bijection between X and the disjoint union of G/Stab(φ(ω)) over all orbits ω. In most cases you'll want φ to be Quotient.out, so we provide AddAction.selfEquivSigmaOrbitsQuotientStabilizer' as a special case.

                                              Equations
                                                Instances For
                                                  theorem MulAction.card_eq_sum_card_group_div_card_stabilizer' (α : Type u) (β : Type v) [Group α] [MulAction α β] [Fintype α] [Fintype β] [Fintype (Quotient (orbitRel α β))] [(b : β) → Fintype (stabilizer α b)] {φ : Quotient (orbitRel α β)β} ( : Function.LeftInverse Quotient.mk'' φ) :
                                                  Fintype.card β = ω : Quotient (orbitRel α β), Fintype.card α / Fintype.card (stabilizer α (φ ω))

                                                  Class formula for a finite group acting on a finite type. See MulAction.card_eq_sum_card_group_div_card_stabilizer for a specialized version using Quotient.out.

                                                  theorem AddAction.card_eq_sum_card_addGroup_sub_card_stabilizer' (α : Type u) (β : Type v) [AddGroup α] [AddAction α β] [Fintype α] [Fintype β] [Fintype (Quotient (orbitRel α β))] [(b : β) → Fintype (stabilizer α b)] {φ : Quotient (orbitRel α β)β} ( : Function.LeftInverse Quotient.mk'' φ) :
                                                  Fintype.card β = ω : Quotient (orbitRel α β), Fintype.card α / Fintype.card (stabilizer α (φ ω))

                                                  Class formula for a finite group acting on a finite type. See AddAction.card_eq_sum_card_addGroup_div_card_stabilizer for a specialized version using Quotient.out.

                                                  noncomputable def MulAction.selfEquivSigmaOrbitsQuotientStabilizer (α : Type u) (β : Type v) [Group α] [MulAction α β] :
                                                  β (ω : Quotient (orbitRel α β)) × α stabilizer α ω.out

                                                  Class formula. This is a special case of MulAction.self_equiv_sigma_orbits_quotient_stabilizer' with φ = Quotient.out.

                                                  Equations
                                                    Instances For
                                                      noncomputable def AddAction.selfEquivSigmaOrbitsQuotientStabilizer (α : Type u) (β : Type v) [AddGroup α] [AddAction α β] :
                                                      β (ω : Quotient (orbitRel α β)) × α stabilizer α ω.out

                                                      Class formula. This is a special case of AddAction.self_equiv_sigma_orbits_quotient_stabilizer' with φ = Quotient.out.

                                                      Equations
                                                        Instances For
                                                          theorem MulAction.card_eq_sum_card_group_div_card_stabilizer (α : Type u) (β : Type v) [Group α] [MulAction α β] [Fintype α] [Fintype β] [Fintype (Quotient (orbitRel α β))] [(b : β) → Fintype (stabilizer α b)] :

                                                          Class formula for a finite group acting on a finite type.

                                                          theorem AddAction.card_eq_sum_card_addGroup_sub_card_stabilizer (α : Type u) (β : Type v) [AddGroup α] [AddAction α β] [Fintype α] [Fintype β] [Fintype (Quotient (orbitRel α β))] [(b : β) → Fintype (stabilizer α b)] :

                                                          Class formula for a finite group acting on a finite type.

                                                          noncomputable def MulAction.sigmaFixedByEquivOrbitsProdGroup (α : Type u) (β : Type v) [Group α] [MulAction α β] :
                                                          (a : α) × (fixedBy β a) Quotient (orbitRel α β) × α

                                                          Burnside's lemma : a (noncomputable) bijection between the disjoint union of all {x ∈ X | g • x = x} for g ∈ G and the product G × X/G, where G is a group acting on X and X/G denotes the quotient of X by the relation orbitRel G X.

                                                          Equations
                                                            Instances For
                                                              noncomputable def AddAction.sigmaFixedByEquivOrbitsProdAddGroup (α : Type u) (β : Type v) [AddGroup α] [AddAction α β] :
                                                              (a : α) × (fixedBy β a) Quotient (orbitRel α β) × α

                                                              Burnside's lemma : a (noncomputable) bijection between the disjoint union of all {x ∈ X | g • x = x} for g ∈ G and the product G × X/G, where G is an additive group acting on X and X/Gdenotes the quotient of X by the relation orbitRel G X.

                                                              Equations
                                                                Instances For
                                                                  theorem MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group (α : Type u) (β : Type v) [Group α] [MulAction α β] [Fintype α] [(a : α) → Fintype (fixedBy β a)] [Fintype (Quotient (orbitRel α β))] :
                                                                  a : α, Fintype.card (fixedBy β a) = Fintype.card (Quotient (orbitRel α β)) * Fintype.card α

                                                                  Burnside's lemma : given a finite group G acting on a set X, the average number of elements fixed by each g ∈ G is the number of orbits.

                                                                  theorem AddAction.sum_card_fixedBy_eq_card_orbits_mul_card_addGroup (α : Type u) (β : Type v) [AddGroup α] [AddAction α β] [Fintype α] [(a : α) → Fintype (fixedBy β a)] [Fintype (Quotient (orbitRel α β))] :
                                                                  a : α, Fintype.card (fixedBy β a) = Fintype.card (Quotient (orbitRel α β)) * Fintype.card α

                                                                  Burnside's lemma : given a finite additive group G acting on a set X, the average number of elements fixed by each g ∈ G is the number of orbits.

                                                                  noncomputable def MulAction.equivSubgroupOrbitsSetoidComap {α : Type u} {β : Type v} [Group α] [MulAction α β] (H : Subgroup α) (ω : Quotient (orbitRel α β)) :

                                                                  A bijection between the quotient of the action of a subgroup H on an orbit, and a corresponding quotient expressed in terms of Setoid.comap Subtype.val.

                                                                  Equations
                                                                    Instances For

                                                                      A bijection between the quotient of the action of an additive subgroup H on an orbit, and a corresponding quotient expressed in terms of Setoid.comap Subtype.val.

                                                                      Equations
                                                                        Instances For
                                                                          noncomputable def MulAction.equivSubgroupOrbits {α : Type u} (β : Type v) [Group α] [MulAction α β] (H : Subgroup α) :

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

                                                                          Equations
                                                                            Instances For
                                                                              noncomputable def AddAction.equivAddSubgroupOrbits {α : Type u} (β : Type v) [AddGroup α] [AddAction α β] (H : AddSubgroup α) :

                                                                              A bijection between the orbits under the action of an additive subgroup H on β, and the orbits under the action of H on each orbit under the action of G.

                                                                              Equations
                                                                                Instances For
                                                                                  noncomputable def MulAction.equivSubgroupOrbitsQuotientGroup {α : Type u} {β : Type v} [Group α] [MulAction α β] (x : β) [IsPretransitive α β] (free : ∀ (y : β), stabilizer α y = ) (H : Subgroup α) :
                                                                                  orbitRel.Quotient (↥H) β α H

                                                                                  Given a group acting freely and transitively, an equivalence between the orbits under the action of a subgroup and the quotient group.

                                                                                  Equations
                                                                                    Instances For
                                                                                      noncomputable def AddAction.equivAddSubgroupOrbitsQuotientAddGroup {α : Type u} {β : Type v} [AddGroup α] [AddAction α β] (x : β) [IsPretransitive α β] (free : ∀ (y : β), stabilizer α y = ) (H : AddSubgroup α) :
                                                                                      orbitRel.Quotient (↥H) β α H

                                                                                      Given an additive group acting freely and transitively, an equivalence between the orbits under the action of an additive subgroup and the quotient group.

                                                                                      Equations
                                                                                        Instances For
                                                                                          noncomputable def MulAction.selfEquivOrbitsQuotientProd' {α : Type u} {β : Type v} [Group α] [MulAction α β] {φ : Quotient (orbitRel α β)β} ( : Function.LeftInverse Quotient.mk'' φ) (h : ∀ (b : β), stabilizer α b = ) :
                                                                                          β Quotient (orbitRel α β) × α

                                                                                          If α acts on β with trivial stabilizers, β is equivalent to the product of the quotient of β by α and α. See MulAction.selfEquivOrbitsQuotientProd with φ = Quotient.out.

                                                                                          Equations
                                                                                            Instances For
                                                                                              noncomputable def AddAction.selfEquivOrbitsQuotientProd' {α : Type u} {β : Type v} [AddGroup α] [AddAction α β] {φ : Quotient (orbitRel α β)β} ( : Function.LeftInverse Quotient.mk'' φ) (h : ∀ (b : β), stabilizer α b = ) :
                                                                                              β Quotient (orbitRel α β) × α

                                                                                              If α acts freely on β, β is equivalent to the product of the quotient of β by α and α. See AddAction.selfEquivOrbitsQuotientProd with φ = Quotient.out.

                                                                                              Equations
                                                                                                Instances For
                                                                                                  @[deprecated AddAction.selfEquivOrbitsQuotientProd' (since := "2025-03-11")]
                                                                                                  def AddAction.selfEquivOrbitsQuotientSum' {α : Type u} {β : Type v} [AddGroup α] [AddAction α β] {φ : Quotient (orbitRel α β)β} ( : Function.LeftInverse Quotient.mk'' φ) (h : ∀ (b : β), stabilizer α b = ) :
                                                                                                  β Quotient (orbitRel α β) × α

                                                                                                  Alias of AddAction.selfEquivOrbitsQuotientProd'.


                                                                                                  If α acts freely on β, β is equivalent to the product of the quotient of β by α and α. See AddAction.selfEquivOrbitsQuotientProd with φ = Quotient.out.

                                                                                                  Equations
                                                                                                    Instances For
                                                                                                      noncomputable def MulAction.selfEquivOrbitsQuotientProd {α : Type u} {β : Type v} [Group α] [MulAction α β] (h : ∀ (b : β), stabilizer α b = ) :
                                                                                                      β Quotient (orbitRel α β) × α

                                                                                                      If α acts freely on β, β is equivalent to the product of the quotient of β by α and α.

                                                                                                      Equations
                                                                                                        Instances For
                                                                                                          noncomputable def AddAction.selfEquivOrbitsQuotientProd {α : Type u} {β : Type v} [AddGroup α] [AddAction α β] (h : ∀ (b : β), stabilizer α b = ) :
                                                                                                          β Quotient (orbitRel α β) × α

                                                                                                          If α acts freely on β, β is equivalent to the product of the quotient of β by α and α.

                                                                                                          Equations
                                                                                                            Instances For
                                                                                                              @[deprecated AddAction.selfEquivOrbitsQuotientProd (since := "2025-03-11")]
                                                                                                              def AddAction.selfEquivOrbitsQuotientSum {α : Type u} {β : Type v} [AddGroup α] [AddAction α β] (h : ∀ (b : β), stabilizer α b = ) :
                                                                                                              β Quotient (orbitRel α β) × α

                                                                                                              Alias of AddAction.selfEquivOrbitsQuotientProd.


                                                                                                              If α acts freely on β, β is equivalent to the product of the quotient of β by α and α.

                                                                                                              Equations
                                                                                                                Instances For
                                                                                                                  noncomputable def Subgroup.quotientCentralizerEmbedding {G : Type u_1} [Group G] (g : G) :

                                                                                                                  Cosets of the centralizer of an element embed into the set of commutators.

                                                                                                                  Equations
                                                                                                                    Instances For
                                                                                                                      noncomputable def Subgroup.quotientCenterEmbedding {G : Type u_1} [Group G] {S : Set G} (hS : closure S = ) :
                                                                                                                      G center G S(commutatorSet G)

                                                                                                                      If G is generated by S, then the quotient by the center embeds into S-indexed sequences of commutators.

                                                                                                                      Equations
                                                                                                                        Instances For
                                                                                                                          theorem Subgroup.quotientCenterEmbedding_apply {G : Type u_1} [Group G] {S : Set G} (hS : closure S = ) (g : G) (s : S) :
                                                                                                                          (quotientCenterEmbedding hS) (↑g) s = g, s,