MulAction.card_eq_sum_card_group_div_card_stabilizer
theorem MulAction.card_eq_sum_card_group_div_card_stabilizer :
∀ (α : Type u) (β : Type v) [inst : Group α] [inst_1 : MulAction α β] [inst_2 : Fintype α] [inst_3 : Fintype β]
[inst_4 : Fintype (Quotient (MulAction.orbitRel α β))] [inst_5 : (b : β) → Fintype ↥(MulAction.stabilizer α b)],
Fintype.card β = Finset.univ.sum fun ω => Fintype.card α / Fintype.card ↥(MulAction.stabilizer α ω.out')
This theorem is the **Class formula** for a finite group acting on a finite type. It states that for any finite group `α`, any finite type `β` on which `α` acts, the total number of elements in `β` is equal to the sum, over all orbits in `β`, of the number of elements in `α` divided by the number of elements in the stabilizer of a representative of each orbit. Here, an orbit is a set of elements in `β` that can be obtained by applying the group action to a particular element, and the stabilizer of an element is the set of group elements that leave the element unchanged under the group action.
More concisely: The total number of elements in a finite group's action on a finite type equals the sum of the element counts in the orbits, where the count in each orbit is the size of the group divided by the size of its stabilizer for a representative element.
|
MulAction.card_orbit_mul_card_stabilizer_eq_card_group
theorem MulAction.card_orbit_mul_card_stabilizer_eq_card_group :
∀ (α : Type u) {β : Type v} [inst : Group α] [inst_1 : MulAction α β] (b : β) [inst_2 : Fintype α]
[inst_3 : Fintype ↑(MulAction.orbit α b)] [inst_4 : Fintype ↥(MulAction.stabilizer α b)],
Fintype.card ↑(MulAction.orbit α b) * Fintype.card ↥(MulAction.stabilizer α b) = Fintype.card α
This is the Orbit-Stabilizer theorem in group theory. It states that for a given group action of a group `α` on a set `β`, and for any element `b` in `β`, the product of the number of elements in the 'orbit' of `b` (the set of elements that `b` can be moved to by the group action) and the number of elements in the 'stabilizer' of `b` (the set of elements in the group that leave `b` unchanged under the group action) is equal to the number of elements in the group `α`. This is a fundamental result in the theory of group actions, and it essentially counts the number of distinct ways the group action can be applied to `b`.
More concisely: The number of elements in the orbit of a point under a group action times the number of elements in its stabilizer equals the order of the group.
|
AddAction.sum_card_fixedBy_eq_card_orbits_add_card_addGroup
theorem AddAction.sum_card_fixedBy_eq_card_orbits_add_card_addGroup :
∀ (α : Type u) (β : Type v) [inst : AddGroup α] [inst_1 : AddAction α β] [inst_2 : Fintype α]
[inst_3 : (a : α) → Fintype ↑(AddAction.fixedBy β a)] [inst_4 : Fintype (Quotient (AddAction.orbitRel α β))],
(Finset.univ.sum fun a => Fintype.card ↑(AddAction.fixedBy β a)) =
Fintype.card (Quotient (AddAction.orbitRel α β)) * Fintype.card α
**Burnside's Lemma**: Given a finite additive group `G` acting on a set `X`, the theorem states that the total number of elements fixed by each group element, averaged over all the group elements, is equal to the total number of distinct orbits under the group action. In other words, the sum of the cardinalities of the fixed-point sets for every element in the group `G` is equal to the product of the cardinality of the set of orbits and the cardinality of the group `G`.
More concisely: The sum of the sizes of the fixed-point sets for every group element in a finite additive group's action on a set equals the product of the number of orbits and the group size.
|
MulAction.card_eq_sum_card_group_div_card_stabilizer'
theorem MulAction.card_eq_sum_card_group_div_card_stabilizer' :
∀ (α : Type u) (β : Type v) [inst : Group α] [inst_1 : MulAction α β] [inst_2 : Fintype α] [inst_3 : Fintype β]
[inst_4 : Fintype (Quotient (MulAction.orbitRel α β))] [inst_5 : (b : β) → Fintype ↥(MulAction.stabilizer α b)]
{φ : Quotient (MulAction.orbitRel α β) → β},
Function.LeftInverse Quotient.mk'' φ →
Fintype.card β = Finset.univ.sum fun ω => Fintype.card α / Fintype.card ↥(MulAction.stabilizer α (φ ω))
This theorem, known as the **Class formula** or the Orbit-Stabilizer theorem, describes the relationship between the size of a finite group, the sizes of its orbits, and the sizes of its stabilizers. Specifically, it asserts that for any finite group `α` acting on a finite type `β`, the total size of `β` is equal to the sum, over all orbits `ω` of `β`, of the size of `α` divided by the size of the stabilizer of any element `φ ω` in the orbit `ω`. This is provided that `φ` is a left inverse to the function that maps an element to its equivalence class in the quotient of `β` by the orbit relation. In other words, the size of a finite group action's set is equal to the sum of the group's size divided by the size of all stabilizers.
More concisely: The size of a finite group's action on a finite type equals the sum of the group's size divided by the size of each stabilizer over all orbits.
|
AddAction.card_eq_sum_card_addGroup_sub_card_stabilizer
theorem AddAction.card_eq_sum_card_addGroup_sub_card_stabilizer :
∀ (α : Type u) (β : Type v) [inst : AddGroup α] [inst_1 : AddAction α β] [inst_2 : Fintype α] [inst_3 : Fintype β]
[inst_4 : Fintype (Quotient (AddAction.orbitRel α β))] [inst_5 : (b : β) → Fintype ↥(AddAction.stabilizer α b)],
Fintype.card β = Finset.univ.sum fun ω => Fintype.card α / Fintype.card ↥(AddAction.stabilizer α ω.out')
This is the Class Formula for a finite group acting on a finite type. The theorem states that, for a finite additive group `α` acting on a finite type `β`, the total number of elements in `β` is equal to the sum, over all orbits (which are equivalence classes under the action of `α`), of the ratio of the number of elements in `α` to the number of elements in the stabilizer of any element in the orbit. The stabilizer of an element is the subgroup of `α` that leaves the element fixed. The numerator of the ratio is the total number of group elements, and the denominator is the number of group elements that fix a particular point in the orbit. Therefore, the ratio represents the number of distinct points that can be reached from a single point by the group action. By summing over all orbits, we get the total number of points in `β`.
More concisely: The total number of elements in a finite type under the action of a finite group equals the sum of the quotient of the group's order by the stabilizer order for each orbit.
|
MulAction.QuotientAction.inv_mul_mem
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
This theorem states that for any two elements `a` and `a'` of a group `α`, and any element `b` of a monoid `β` (with `β` acting on `α`), if the product of the inverse of `a` and `a'` belongs to a subgroup `H` of `α`, then the product of the inverse of the result of `b` acting on `a` and the result of `b` acting on `a'` also belongs to `H`. This property ensures that the action of `β` on `α` can be extended to an action on the quotient group `α ⧸ H`.
More concisely: If `a`, `a'` are elements of a group `α`, `b` is an element of a monoid `β` that acts on `α`, and the inverse of their product `a⁻¹ * a'` belongs to the subgroup `H` of `α`, then the inverse of `b`'s action on `a` and `b`'s action on `a'` have an element in their product in `H`.
|
AddAction.card_eq_sum_card_addGroup_sub_card_stabilizer'
theorem AddAction.card_eq_sum_card_addGroup_sub_card_stabilizer' :
∀ (α : Type u) (β : Type v) [inst : AddGroup α] [inst_1 : AddAction α β] [inst_2 : Fintype α] [inst_3 : Fintype β]
[inst_4 : Fintype (Quotient (AddAction.orbitRel α β))] [inst_5 : (b : β) → Fintype ↥(AddAction.stabilizer α b)]
{φ : Quotient (AddAction.orbitRel α β) → β},
Function.LeftInverse Quotient.mk'' φ →
Fintype.card β = Finset.univ.sum fun ω => Fintype.card α / Fintype.card ↥(AddAction.stabilizer α (φ ω))
This theorem is a version of the **Class formula** for a finite group acting on a finite type. It states that for any two types `α` and `β`, where `α` is an additive group and there is an additive action of `α` on `β`, and both `α` and `β` are finite types, the number of elements in `β` is the sum over all orbits (equivalence classes under the action), of the number of elements in `α` divided by the number of elements in the stabilizer of a representative of the orbit. Here, the stabilizer of an element under the action is the subgroup of elements that send the element to itself. The representative of each orbit is chosen by a function `φ` which is a left inverse to the quotient map, meaning that each orbit is mapped to exactly one representative.
More concisely: The number of elements in a finite type `β` with an additive action of a finite additive group `α` equals the sum of the cardinalities of `α` divided by the stabilizer sizes of representatives from each orbit under the action.
|
AddAction.card_orbit_add_card_stabilizer_eq_card_addGroup
theorem AddAction.card_orbit_add_card_stabilizer_eq_card_addGroup :
∀ (α : Type u) {β : Type v} [inst : AddGroup α] [inst_1 : AddAction α β] (b : β) [inst_2 : Fintype α]
[inst_3 : Fintype ↑(AddAction.orbit α b)] [inst_4 : Fintype ↥(AddAction.stabilizer α b)],
Fintype.card ↑(AddAction.orbit α b) * Fintype.card ↥(AddAction.stabilizer α b) = Fintype.card α
The Orbit-Stabilizer theorem in the context of additive groups states that for any additive group `α` that acts on a set `β` (an action `AddAction α β`) and given an element `b` in set `β`, the product of the size (number of elements) of the orbit of `b` under the action and the size of the stabilizer of `b` under the action, is equal to the size of the group `α`. The orbit of an element under an action is the set of elements resulting from the action of every group element on this element, whereas the stabilizer of an element under an action is the set of group elements that leave the element unchanged. The requirement `[Fintype α]` indicates that the group `α` is finite, and similarly, `[Fintype ↑(AddAction.orbit α b)]` and `[Fintype ↥(AddAction.stabilizer α b)]` indicate that the orbit and stabilizer of `b` are also finite.
More concisely: For any finite additive group `α` acting on a set `β`, the number of elements in the orbit of an element `b` in `β` under the action, multiplied by the number of elements in the stabilizer of `b`, equals the order (number of elements) of the group `α`.
|
AddAction.QuotientAction.inv_mul_mem
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
This theorem states that for any types `α` and `β`, with `α` being an additive group and `β` being an additive monoid with an associated additive action on `α`, along with a specified additive subgroup `H` of `α`, and given the quotient action of `β` on `H`, for any elements `b` in `β` and `a, a'` in `α` such that `-a + a'` belongs to `H`, it ensures that the additive inverse of the element resulting from the vector addition of `b` and `a` plus the element resulting from the vector addition of `b` and `a'` also belongs to `H`. This theorem is a normality condition for the additive action which guarantees that the action can descend to an action on the quotient of `α` by `H`.
More concisely: For any additive group `α`, additive monoid `β` with an additive action on `α`, and subgroup `H` of `α`, if for all `b ∈ β` and `a, a' ∈ α` such that `-a + a' ∈ H`, we have `-(b + a) + (b + a') ∈ H`, then the additive action of `β` on `α` descends to a well-defined additive action on the quotient `α/H`.
|
MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group
theorem MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group :
∀ (α : Type u) (β : Type v) [inst : Group α] [inst_1 : MulAction α β] [inst_2 : Fintype α]
[inst_3 : (a : α) → Fintype ↑(MulAction.fixedBy β a)] [inst_4 : Fintype (Quotient (MulAction.orbitRel α β))],
(Finset.univ.sum fun a => Fintype.card ↑(MulAction.fixedBy β a)) =
Fintype.card (Quotient (MulAction.orbitRel α β)) * Fintype.card α
**Burnside's Lemma**: This theorem states that for a finite group `G` acting on a set `X`, the average number of elements in `X` that remain unchanged by each group action (i.e., fixed by each group element `g` in `G`) equals the total number of orbits (i.e., equivalence classes of elements in `X` under the group action) times the size of the group `G`. This is also known as the orbit-counting theorem. The action of the group is considered through the `MulAction` typeclass, orbits are defined in terms of the `MulAction.orbitRel` relation, and the sizes of the sets are computed using the `Fintype.card` function, which counts the number of elements in a finite set.
More concisely: The average number of fixed points of a finite group's actions on a set equals the product of the number of orbits and the group's size.
|