The multiset of orbit sizes

For a group G acting on a finite type X, the multiset of the sizes of the orbits of G on X is a basic invariant of the action. This file records two ways in which it is preserved: by a change of the acting group that does not change the orbits, and by an equivariant bijection of the underlying types. It also bounds the length of a list of group elements with distinct images of a point by the size of the orbit of that point.

Main results

• MulAction.orbitRel.Quotient.card_orbit_ne_zero: an orbit in a finite action has nonzero natural cardinality.

• MulAction.orbitRel.Quotient.card_filter_quotient_mk: the fiber of the orbit quotient map has the cardinality of the corresponding orbit.

• Equiv.map_card_orbit_eq_of_image_orbit_eq: a bijection carrying the orbits of one action onto the orbits of another preserves the multiset of orbit sizes.

• Equiv.map_card_orbit_eq_of_map_smul: an equivariant bijection preserves the multiset of orbit sizes.

• TauCeti.map_card_orbit_eq_of_orbit_eq: two actions on the same finite type with the same orbits have the same multiset of orbit sizes.

• Subgroup.length_le_ncard_orbit: a list of elements of a subgroup K with distinct images of x is no longer than the orbit of x under K, if that orbit is finite.

theorem MulAction.orbitRel.Quotient.card_orbit_ne_zero {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [Finite X] (O : Quotient G X) : Nat.card ↑O.orbit ≠ 0

Every orbit in an action on a finite type has nonzero natural cardinality.

theorem MulAction.orbitRel.Quotient.card_filter_quotient_mk {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [Fintype X] (O : Quotient G X) : {x : X | ⟦x⟧ = O}.card = Nat.card ↑O.orbit

The fiber of the orbit quotient map has the natural cardinality of that orbit.

theorem Equiv.map_card_orbit_eq_of_image_orbit_eq {G : Type u_1} {G' : Type u_2} {X : Type u_3} {Y : Type u_4} [Group G] [Group G'] [MulAction G X] [MulAction G' Y] [Fintype X] [Fintype Y] (e : X ≃ Y) (h : ∀ (x : X), ⇑e '' MulAction.orbit G x = MulAction.orbit G' (e x)) : Multiset.map (fun (ω : MulAction.orbitRel.Quotient G X) => Nat.card ↑ω.orbit) Finset.univ.val = Multiset.map (fun (ω : MulAction.orbitRel.Quotient G' Y) => Nat.card ↑ω.orbit) Finset.univ.val

A bijection matching the orbits preserves the orbit sizes. If e : X ≃ Y carries every orbit of G on X onto an orbit of G' on Y, then the multisets of orbit sizes of the two actions agree.

theorem Equiv.map_card_orbit_eq_of_map_smul {G : Type u_1} {X : Type u_2} {Y : Type u_3} [Group G] [MulAction G X] [MulAction G Y] [Fintype X] [Fintype Y] (e : X ≃ Y) (he : ∀ (g : G) (x : X), e (g • x) = g • e x) : Multiset.map (fun (ω : MulAction.orbitRel.Quotient G X) => Nat.card ↑ω.orbit) Finset.univ.val = Multiset.map (fun (ω : MulAction.orbitRel.Quotient G Y) => Nat.card ↑ω.orbit) Finset.univ.val

Equivariant bijections preserve orbit sizes. If e : X ≃ Y is a bijection between finite G-sets commuting with the action, then the multisets of orbit sizes of X and of Y agree.

theorem TauCeti.map_card_orbit_eq_of_orbit_eq {G : Type u_1} {G' : Type u_2} {X : Type u_3} [Group G] [Group G'] [MulAction G X] [MulAction G' X] [Fintype X] (h : ∀ (x : X), MulAction.orbit G x = MulAction.orbit G' x) : Multiset.map (fun (ω : MulAction.orbitRel.Quotient G X) => Nat.card ↑ω.orbit) Finset.univ.val = Multiset.map (fun (ω : MulAction.orbitRel.Quotient G' X) => Nat.card ↑ω.orbit) Finset.univ.val

Same orbits, same orbit sizes. If two group actions on a finite type have the same orbits, then they have the same multiset of orbit sizes.

theorem Subgroup.length_le_ncard_orbit {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {K : Subgroup G} {x : α} {R : List G} (hR : ∀ r ∈ R, r ∈ K) (hnodup : (List.map (fun (x_1 : G) => x_1 • x) R).Nodup) (horbit : (MulAction.orbit (↥K) x).Finite := by toFinite_tac) : R.length ≤ (MulAction.orbit (↥K) x).ncard

The images of x under a list of elements of a subgroup K lie in the orbit of x under K, so if that orbit is finite, a list with distinct images of x is no longer than it.