Properties of group actions involving quotient groups

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

• the class formula MulAction.card_eq_sum_card_group_div_card_stabilizer'
• card_comm_eq_card_conjClasses_mul_card

as well as their analogues for additive groups.

See Mathlib/GroupTheory/GroupAction/Quotient.lean for the construction of isomorphisms used to prove these cardinality properties. These lemmas are separate because they require the development of cardinals.

theorem MulAction.card_eq_sum_card_group_div_card_stabilizer' (α : Type u_1) (β : Type u_2) [Group α] [MulAction α β] [Fintype α] [Fintype β] [Fintype (Quotient (orbitRel α β))] [(b : β) → Fintype ↥(stabilizer α b)] {φ : Quotient (orbitRel α β) → β} (hφ : 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_1) (β : Type u_2) [AddGroup α] [AddAction α β] [Fintype α] [Fintype β] [Fintype (Quotient (orbitRel α β))] [(b : β) → Fintype ↥(stabilizer α b)] {φ : Quotient (orbitRel α β) → β} (hφ : 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.

theorem MulAction.card_eq_sum_card_group_div_card_stabilizer (α : Type u_1) (β : Type u_2) [Group α] [MulAction α β] [Fintype α] [Fintype β] [Fintype (Quotient (orbitRel α β))] [(b : β) → Fintype ↥(stabilizer α b)] : Fintype.card β = ∑ ω : Quotient (orbitRel α β), Fintype.card α / Fintype.card ↥(stabilizer α ω.out)

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

theorem AddAction.card_eq_sum_card_addGroup_sub_card_stabilizer (α : Type u_1) (β : Type u_2) [AddGroup α] [AddAction α β] [Fintype α] [Fintype β] [Fintype (Quotient (orbitRel α β))] [(b : β) → Fintype ↥(stabilizer α b)] : Fintype.card β = ∑ ω : Quotient (orbitRel α β), Fintype.card α / Fintype.card ↥(stabilizer α ω.out)

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

instance instInfiniteProdSubtypeCommute {α : Type u_1} [Mul α] [Infinite α] : Infinite { p : α × α // Commute p.1 p.2 }

theorem card_comm_eq_card_conjClasses_mul_card (G : Type u_3) [Group G] : Nat.card { p : G × G // Commute p.1 p.2 } = Nat.card (ConjClasses G) * Nat.card G