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

class MulAction.QuotientAction {α : Type u} (β : Type v) [Group α] [Monoid β] [MulAction β α] (H : Subgroup α) :
  • 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.

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

Instances
    class AddAction.QuotientAction {α : Type u_1} (β : Type u_2) [AddGroup α] [AddMonoid β] [AddAction β α] (H : AddSubgroup α) :
    • 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.

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

    Instances
      instance AddAction.quotient {α : Type u} (β : Type v) [AddGroup α] [AddMonoid β] [AddAction β α] (H : AddSubgroup α) [AddAction.QuotientAction β H] :
      AddAction β (α H)
      Equations
      theorem AddAction.quotient.proof_2 {α : Type u_1} (β : Type u_2) [AddGroup α] [AddMonoid β] [AddAction β α] (H : AddSubgroup α) [AddAction.QuotientAction β H] (q : α H) :
      0 +ᵥ q = q
      theorem AddAction.quotient.proof_1 {α : Type u_1} (β : Type u_2) [AddGroup α] [AddMonoid β] [AddAction β α] (H : AddSubgroup α) [AddAction.QuotientAction β H] (b : β) :
      ∀ (x x_1 : α), Setoid.r x x_1Setoid.r ((fun x x_2 => x +ᵥ x_2) b x) ((fun x x_2 => x +ᵥ x_2) b x_1)
      theorem AddAction.quotient.proof_3 {α : Type u_1} (β : Type u_2) [AddGroup α] [AddMonoid β] [AddAction β α] (H : AddSubgroup α) [AddAction.QuotientAction β H] (b : β) (b' : β) (q : α H) :
      b + b' +ᵥ q = b +ᵥ (b' +ᵥ q)
      instance MulAction.quotient {α : Type u} (β : Type v) [Group α] [Monoid β] [MulAction β α] (H : Subgroup α) [MulAction.QuotientAction β H] :
      MulAction β (α H)
      Equations
      @[simp]
      theorem AddAction.Quotient.vadd_mk {α : Type u} {β : Type v} [AddGroup α] [AddMonoid β] [AddAction β α] (H : AddSubgroup α) [AddAction.QuotientAction β H] (b : β) (a : α) :
      b +ᵥ a = ↑(b +ᵥ a)
      @[simp]
      theorem MulAction.Quotient.smul_mk {α : Type u} {β : Type v} [Group α] [Monoid β] [MulAction β α] (H : Subgroup α) [MulAction.QuotientAction β H] (b : β) (a : α) :
      b a = ↑(b a)
      @[simp]
      theorem AddAction.Quotient.vadd_coe {α : Type u} {β : Type v} [AddGroup α] [AddMonoid β] [AddAction β α] (H : AddSubgroup α) [AddAction.QuotientAction β H] (b : β) (a : α) :
      b +ᵥ a = ↑(b +ᵥ a)
      @[simp]
      theorem MulAction.Quotient.smul_coe {α : Type u} {β : Type v} [Group α] [Monoid β] [MulAction β α] (H : Subgroup α) [MulAction.QuotientAction β H] (b : β) (a : α) :
      b a = ↑(b a)
      @[simp]
      theorem AddAction.Quotient.mk_vadd_out' {α : Type u} {β : Type v} [AddGroup α] [AddMonoid β] [AddAction β α] (H : AddSubgroup α) [AddAction.QuotientAction β H] (b : β) (q : α H) :
      ↑(b +ᵥ Quotient.out' q) = b +ᵥ q
      @[simp]
      theorem MulAction.Quotient.mk_smul_out' {α : Type u} {β : Type v} [Group α] [Monoid β] [MulAction β α] (H : Subgroup α) [MulAction.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 α) [AddAction.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 α) [MulAction.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 x_1 => x x_1) a) q * Quotient.out' q H
      def MulActionHom.toQuotient {α : Type u} [Group α] (H : Subgroup α) :
      α →[α] α H

      The canonical map to the left cosets.

      Equations
      Instances For
        @[simp]
        theorem MulActionHom.toQuotient_apply {α : Type u} [Group α] (H : Subgroup α) (g : α) :
        theorem AddAction.ofQuotientStabilizer.proof_1 (α : Type u_1) {β : Type u_2} [AddGroup α] [AddAction α β] (x : β) (g1 : α) (g2 : α) (H : Setoid.r g1 g2) :
        g1 +ᵥ x = g2 +ᵥ x
        def AddAction.ofQuotientStabilizer (α : Type u) {β : Type v} [AddGroup α] [AddAction α β] (x : β) (g : α AddAction.stabilizer α x) :
        β

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

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

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

          Equations
          Instances For
            @[simp]
            theorem AddAction.ofQuotientStabilizer_mk (α : Type u) {β : Type v} [AddGroup α] [AddAction α β] (x : β) (g : α) :
            @[simp]
            theorem MulAction.ofQuotientStabilizer_mk (α : Type u) {β : Type v} [Group α] [MulAction α β] (x : β) (g : α) :
            theorem AddAction.ofQuotientStabilizer_vadd (α : Type u) {β : Type v} [AddGroup α] [AddAction α β] (x : β) (g : α) (g' : α AddAction.stabilizer α x) :
            theorem MulAction.ofQuotientStabilizer_smul (α : Type u) {β : Type v} [Group α] [MulAction α β] (x : β) (g : α) (g' : α MulAction.stabilizer α x) :
            abbrev AddAction.orbitEquivQuotientStabilizer.match_1 (α : Type u_2) {β : Type u_1} [AddGroup α] [AddAction α β] (b : β) (motive : ↑(AddAction.orbit α b)Prop) :
            (x : ↑(AddAction.orbit α b)) → ((b : β) → (g : α) → (hgb : (fun m => m +ᵥ b) g = b) → motive { val := b, property := (_ : y, (fun m => m +ᵥ b) y = b) }) → motive x
            Equations
            Instances For
              theorem AddAction.orbitEquivQuotientStabilizer.proof_1 (α : Type u_1) {β : Type u_2} [AddGroup α] [AddAction α β] (b : β) :
              noncomputable def AddAction.orbitEquivQuotientStabilizer (α : Type u) {β : Type v} [AddGroup α] [AddAction α β] (b : β) :

              Orbit-stabilizer theorem.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                noncomputable def MulAction.orbitEquivQuotientStabilizer (α : Type u) {β : Type v} [Group α] [MulAction α β] (b : β) :

                Orbit-stabilizer theorem.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  noncomputable def AddAction.orbitSumStabilizerEquivAddGroup (α : Type u) {β : Type v} [AddGroup α] [AddAction α β] (b : β) :
                  ↑(AddAction.orbit α b) × { x // x AddAction.stabilizer α b } α

                  Orbit-stabilizer theorem.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    noncomputable def MulAction.orbitProdStabilizerEquivGroup (α : Type u) {β : Type v} [Group α] [MulAction α β] (b : β) :
                    ↑(MulAction.orbit α b) × { x // x MulAction.stabilizer α b } α

                    Orbit-stabilizer theorem.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For

                      Orbit-stabilizer theorem.

                      Orbit-stabilizer theorem.

                      @[simp]
                      theorem AddAction.orbitEquivQuotientStabilizer_symm_apply (α : Type u) {β : Type v} [AddGroup α] [AddAction α β] (b : β) (a : α) :
                      ↑((AddAction.orbitEquivQuotientStabilizer α b).symm a) = a +ᵥ b
                      @[simp]
                      theorem MulAction.orbitEquivQuotientStabilizer_symm_apply (α : Type u) {β : Type v} [Group α] [MulAction α β] (b : β) (a : α) :
                      ↑((MulAction.orbitEquivQuotientStabilizer α b).symm a) = a b
                      @[simp]
                      @[simp]
                      theorem MulAction.stabilizer_quotient {G : Type u_1} [Group G] (H : Subgroup G) :
                      noncomputable def AddAction.selfEquivSigmaOrbitsQuotientStabilizer' (α : Type u) (β : Type v) [AddGroup α] [AddAction α β] {φ : Quotient (AddAction.orbitRel α β)β} (hφ : Function.LeftInverse Quotient.mk'' φ) :
                      β (ω : Quotient (AddAction.orbitRel α β)) × α AddAction.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
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        noncomputable def MulAction.selfEquivSigmaOrbitsQuotientStabilizer' (α : Type u) (β : Type v) [Group α] [MulAction α β] {φ : Quotient (MulAction.orbitRel α β)β} (hφ : Function.LeftInverse Quotient.mk'' φ) :
                        β (ω : Quotient (MulAction.orbitRel α β)) × α MulAction.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
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          theorem AddAction.card_eq_sum_card_addGroup_sub_card_stabilizer' (α : Type u) (β : Type v) [AddGroup α] [AddAction α β] [Fintype α] [Fintype β] [Fintype (Quotient (AddAction.orbitRel α β))] [(b : β) → Fintype { x // x AddAction.stabilizer α b }] {φ : Quotient (AddAction.orbitRel α β)β} (hφ : Function.LeftInverse Quotient.mk'' φ) :
                          Fintype.card β = Finset.sum Finset.univ fun ω => Fintype.card α / Fintype.card { x // x AddAction.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'.

                          theorem MulAction.card_eq_sum_card_group_div_card_stabilizer' (α : Type u) (β : Type v) [Group α] [MulAction α β] [Fintype α] [Fintype β] [Fintype (Quotient (MulAction.orbitRel α β))] [(b : β) → Fintype { x // x MulAction.stabilizer α b }] {φ : Quotient (MulAction.orbitRel α β)β} (hφ : Function.LeftInverse Quotient.mk'' φ) :
                          Fintype.card β = Finset.sum Finset.univ fun ω => Fintype.card α / Fintype.card { x // x MulAction.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'.

                          noncomputable def AddAction.selfEquivSigmaOrbitsQuotientStabilizer (α : Type u) (β : Type v) [AddGroup α] [AddAction α β] :

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

                          Equations
                          Instances For
                            noncomputable def MulAction.selfEquivSigmaOrbitsQuotientStabilizer (α : Type u) (β : Type v) [Group α] [MulAction α β] :

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

                            Equations
                            Instances For
                              theorem AddAction.card_eq_sum_card_addGroup_sub_card_stabilizer (α : Type u) (β : Type v) [AddGroup α] [AddAction α β] [Fintype α] [Fintype β] [Fintype (Quotient (AddAction.orbitRel α β))] [(b : β) → Fintype { x // x AddAction.stabilizer α b }] :

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

                              theorem MulAction.card_eq_sum_card_group_div_card_stabilizer (α : Type u) (β : Type v) [Group α] [MulAction α β] [Fintype α] [Fintype β] [Fintype (Quotient (MulAction.orbitRel α β))] [(b : β) → Fintype { x // x MulAction.stabilizer α b }] :

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

                              theorem AddAction.sigmaFixedByEquivOrbitsSumAddGroup.proof_1 (α : Type u_1) (β : Type u_2) [AddGroup α] [AddAction α β] :
                              ∀ (x : α × β), x.fst +ᵥ x.snd = x.snd x.fst +ᵥ x.snd = x.snd
                              abbrev AddAction.sigmaFixedByEquivOrbitsSumAddGroup.match_1 (α : Type u_2) (β : Type u_1) [AddGroup α] [AddAction α β] :
                              (x : Quotient (AddAction.orbitRel α β)) → (motive : ↑(AddAction.orbit α (Quotient.out' x))Sort u_3) → (x_1 : ↑(AddAction.orbit α (Quotient.out' x))) → ((val : β) → (hb : val AddAction.orbit α (Quotient.out' x)) → motive { val := val, property := hb }) → motive x_1
                              Equations
                              Instances For
                                noncomputable def AddAction.sigmaFixedByEquivOrbitsSumAddGroup (α : Type u) (β : Type v) [AddGroup α] [AddAction α β] :
                                (a : α) × ↑(AddAction.fixedBy α β a) Quotient (AddAction.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
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  noncomputable def MulAction.sigmaFixedByEquivOrbitsProdGroup (α : Type u) (β : Type v) [Group α] [MulAction α β] :
                                  (a : α) × ↑(MulAction.fixedBy α β a) Quotient (MulAction.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
                                  • One or more equations did not get rendered due to their size.
                                  Instances For

                                    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.

                                    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.

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

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      theorem Subgroup.quotientCentralizerEmbedding_apply {G : Type u_1} [Group G] (g : G) (x : G) :
                                      ↑(Subgroup.quotientCentralizerEmbedding g) x = { val := x, g, property := (_ : g₁ g₂, g₁, g₂ = x, g) }
                                      noncomputable def Subgroup.quotientCenterEmbedding {G : Type u_1} [Group G] {S : Set G} (hS : Subgroup.closure S = ) :
                                      G Subgroup.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
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        theorem Subgroup.quotientCenterEmbedding_apply {G : Type u_1} [Group G] {S : Set G} (hS : Subgroup.closure S = ) (g : G) (s : S) :
                                        ↑(Subgroup.quotientCenterEmbedding hS) (g) s = { val := g, s, property := (_ : g₁ g₂, g₁, g₂ = g, s) }