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 α) :

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
    theorem MulAction.QuotientAction.inv_mul_mem {α : Type u} {β : Type v} :
    ∀ {inst : Group α} {inst_1 : Monoid β} {inst_2 : MulAction β α} {H : Subgroup α} [self : MulAction.QuotientAction β H] (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.

    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
      theorem AddAction.QuotientAction.inv_mul_mem {α : Type u} {β : Type v} :
      ∀ {inst : AddGroup α} {inst_1 : AddMonoid β} {inst_2 : AddAction β α} {H : AddSubgroup α} [self : AddAction.QuotientAction β H] (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.

      Equations
      • =
      Equations
      • =
      instance AddAction.right_quotientAction {α : Type u} [AddGroup α] (H : AddSubgroup α) :
      AddAction.QuotientAction (↥H.normalizer.op) H
      Equations
      • =
      instance MulAction.right_quotientAction {α : Type u} [Group α] (H : Subgroup α) :
      MulAction.QuotientAction (↥H.normalizer.op) H
      Equations
      • =
      instance AddAction.right_quotientAction' {α : Type u} [AddGroup α] (H : AddSubgroup α) [hH : H.Normal] :
      Equations
      • =
      instance MulAction.right_quotientAction' {α : Type u} [Group α] (H : Subgroup α) [hH : H.Normal] :
      Equations
      • =
      instance AddAction.quotient {α : Type u} (β : Type v) [AddGroup α] [AddMonoid β] [AddAction β α] (H : AddSubgroup α) [AddAction.QuotientAction β H] :
      AddAction β (α H)
      Equations
      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 : α 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
      @[simp]
      theorem MulActionHom.toQuotient_apply {α : Type u} [Group α] (H : Subgroup α) (g : α) :
      instance MulAction.mulLeftCosetsCompSubtypeVal {α : Type u} [Group α] (H : Subgroup α) (I : Subgroup α) :
      MulAction (↥I) (α H)
      Equations
      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
      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
      @[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) :
      noncomputable def AddAction.orbitEquivQuotientStabilizer (α : Type u) {β : Type v} [AddGroup α] [AddAction α β] (b : β) :

      Orbit-stabilizer theorem.

      Equations
      noncomputable def MulAction.orbitEquivQuotientStabilizer (α : Type u) {β : Type v} [Group α] [MulAction α β] (b : β) :

      Orbit-stabilizer theorem.

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

      Orbit-stabilizer theorem.

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

      Orbit-stabilizer theorem.

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

      Orbit-stabilizer theorem.

      @[simp]
      theorem AddAction.orbitEquivQuotientStabilizer_symm_apply (α : Type u) {β : Type v} [AddGroup α] [AddAction α β] (b : β) (a : α) :
      @[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.
      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.
      theorem AddAction.card_eq_sum_card_addGroup_sub_card_stabilizer' (α : Type u) (β : Type v) [AddGroup α] [AddAction α β] [Fintype α] [Fintype β] [Fintype (Quotient (AddAction.orbitRel α β))] [(b : β) → Fintype (AddAction.stabilizer α b)] {φ : Quotient (AddAction.orbitRel α β)β} (hφ : Function.LeftInverse Quotient.mk'' φ) :

      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 (MulAction.stabilizer α b)] {φ : Quotient (MulAction.orbitRel α β)β} (hφ : Function.LeftInverse Quotient.mk'' φ) :

      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 α β] :
      β (ω : Quotient (AddAction.orbitRel α β)) × α AddAction.stabilizer α ω.out'

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

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

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

      Equations

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

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

      noncomputable def AddAction.sigmaFixedByEquivOrbitsProdAddGroup (α : 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.
      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.

      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.

      Equations
      • =
      Equations
      • =

      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
      • One or more equations did not get rendered due to their size.

      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
      • One or more equations did not get rendered due to their size.

      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
      • One or more equations did not get rendered due to their size.

      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
      • One or more equations did not get rendered due to their size.
      noncomputable def AddAction.equivAddSubgroupOrbitsQuotientAddGroup {α : Type u} {β : Type v} [AddGroup α] [AddAction α β] (x : β) [AddAction.IsPretransitive α β] (free : ∀ (y : β), AddAction.stabilizer α y = ) (H : AddSubgroup α) :

      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
      • One or more equations did not get rendered due to their size.
      noncomputable def MulAction.equivSubgroupOrbitsQuotientGroup {α : Type u} {β : Type v} [Group α] [MulAction α β] (x : β) [MulAction.IsPretransitive α β] (free : ∀ (y : β), MulAction.stabilizer α y = ) (H : Subgroup α) :

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

      Equations
      • One or more equations did not get rendered due to their size.
      theorem Subgroup.normalCore_eq_ker {G : Type u_1} [Group G] (H : Subgroup G) :
      H.normalCore = (MulAction.toPermHom G (G H)).ker

      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.
      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.
      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 = g, s,