Documentation

Mathlib.GroupTheory.GroupAction.CardCommute

Properties of group actions involving quotient groups #

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

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 α β)β} ( : 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 α β)β} ( : 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)] :

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

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 }