Point stabilisers: their cardinality, and when they are normal

A subgroup inclusion restricts to an injective map on point stabilizers, so the smaller stabilizer order divides the larger one.

A count defined through a point stabiliser is useful only alongside the rules for moving it. Three such rules are recorded here, all consequences of Mathlib machinery rather than new mathematics, and all stated for Nat.card because that is the form a numerical invariant of an orbit is wanted in. The first of them is what lets the count descend to the orbit space, so that descent is recorded here as well, as the definition cardStabilizerOnOrbit.

Along an orbit the stabiliser order does not change: related points have conjugate stabilisers, by MulAction.stabilizerEquivStabilizerOfOrbitRel.

Along an equivariant injection it does not change either: a map α → β carrying the action of G to that of H along a group isomorphism G ≃* H, and separating the point from its translates, identifies the stabilisers. So when the map is an equivalence, the equivalence of orbit spaces it induces, TauCeti.MulAction.orbitRelQuotientCongr, preserves cardStabilizerOnOrbit, and so does the splitting TauCeti.MulAction.orbitRelQuotientSumEquiv of the orbit space of an action on a sum α ⊕ β. These are what move a weighted count of orbits from one action to another.

Along a surjection it divides: if f : G →* H is onto and the two actions agree at the point in question, then the G-order of that point's stabiliser is Nat.card f.ker times its H-order. Taking f to be a quotient map gives the projective case, where the divisor is the subgroup quotiented out.

Finally, a group of prime order acting on its own finite subsets by translation has trivial stabilisers away from the two fixed points ∅ and univ: a stabiliser is a subgroup, so it is trivial or everything, and a subset fixed by every translation is empty or everything.

A point stabiliser of a permutation representation ρ : G →* Equiv.Perm α is a subgroup of the source, namely the comap of the stabiliser in Equiv.Perm α. The last two results say when that subgroup is the kernel — so in particular normal — and, for a transitive representation, that normality of it is equivalent to freeness of the action of the image.

Main results

• TauCeti.stabilizer_finset_eq_bot_of_prime_card: a group of prime order acts freely by translation on its nonempty proper finite subsets.
• TauCeti.card_stabilizer_of_orbitRel: the stabiliser order is an invariant of the orbit, with TauCeti.card_stabilizer_smul the translate-presented corollary.
• TauCeti.cardStabilizerOnOrbit: that order as a function on the orbit space, with TauCeti.cardStabilizerOnOrbit_mk its evaluation lemma.
• TauCeti.card_stabilizer_congr: the stabiliser order is preserved by a map carrying one action to another along a group isomorphism, if it separates the point from its translates.
• TauCeti.cardStabilizerOnOrbit_orbitRelQuotientCongr: the orbit-space equivalence TauCeti.MulAction.orbitRelQuotientCongr induced by an equivariant equivalence preserves the stabiliser orders.
• TauCeti.cardStabilizerOnOrbit_orbitRelQuotientSumEquiv_symm: the splitting TauCeti.MulAction.orbitRelQuotientSumEquiv of the orbit space of an action on α ⊕ β preserves the stabiliser orders.
• TauCeti.card_stabilizer_eq_card_ker_mul_card_stabilizer: the stabiliser order divides by Nat.card f.ker along a surjection f, with TauCeti.card_stabilizer_eq_card_subgroup_mul_card_stabilizer_quotient the quotient-map corollary and TauCeti.card_stabilizer_eq_card_subgroupOf_mul_card_stabilizer_map its relative form, for a subgroup mapped into the quotient.
• TauCeti.card_stabilizer_subgroupOf: the degenerate case of that surjection, where the map is the isomorphism 𝒢.subgroupOf ℋ ≃* 𝒢 and the order is unchanged.
• TauCeti.card_stabilizer_coset_eq_card_stabilizer_inv_smul: the class of g in G ⧸ H has, inside stabilizer G p, a stabiliser of the same order as g⁻¹ • p has inside H — conjugation by g is the bijection.
• MonoidHom.comap_stabilizer_eq_ker: the point stabiliser of a permutation representation is its kernel as soon as the image has trivial stabiliser at that point, and MonoidHom.normal_comap_stabilizer_iff_isCancelSMul: for a transitive representation that happens exactly when the image acts freely, which is exactly when the point stabiliser is normal.

def Subgroup.stabilizerInclusion {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {Δ Γ : Subgroup G} (h : Δ ≤ Γ) (x : X) : ↥(MulAction.stabilizer (↥Δ) x) →* ↥(MulAction.stabilizer (↥Γ) x)

Inclusion of groups restricts to an inclusion of their stabilizers at the same point.

Equations

• Subgroup.stabilizerInclusion h x = { toFun := fun (g : ↥(MulAction.stabilizer (↥Δ) x)) => ⟨⟨↑↑g, ⋯⟩, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

theorem Subgroup.stabilizerInclusion_injective {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {Δ Γ : Subgroup G} (h : Δ ≤ Γ) (x : X) : Function.Injective ⇑(stabilizerInclusion h x)

The inclusion of point stabilizers is injective.

theorem Subgroup.card_stabilizer_dvd_card_stabilizer {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {Δ Γ : Subgroup G} (h : Δ ≤ Γ) (x : X) : Nat.card ↥(MulAction.stabilizer (↥Δ) x) ∣ Nat.card ↥(MulAction.stabilizer (↥Γ) x)

The stabilizer order for a subgroup divides that for a larger group.

theorem Subgroup.finite_stabilizer_of_le {G : Type u_3} {X : Type u_4} [Group G] [MulAction G X] {Δ Γ : Subgroup G} (h : Δ ≤ Γ) (x : X) [Finite ↥(MulAction.stabilizer (↥Γ) x)] : Finite ↥(MulAction.stabilizer (↥Δ) x)

Restricting a group action to a smaller subgroup preserves finiteness of a point stabilizer.

theorem TauCeti.card_stabilizer_of_orbitRel {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {a b : α} (h : (MulAction.orbitRel G α) a b) : Nat.card ↥(MulAction.stabilizer G a) = Nat.card ↥(MulAction.stabilizer G b)

The order of a stabiliser is constant along an orbit: points related by the orbit relation have conjugate stabilisers, hence stabilisers of equal cardinality.

This is what lets a count defined through a point stabiliser — the order e_P of an elliptic point of a Fuchsian group, say — be read as an invariant of the orbit. It holds with no finiteness hypothesis: for an infinite stabiliser both sides are 0, by Nat.card's convention.

theorem TauCeti.card_stabilizer_smul {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (g : G) (a : α) : Nat.card ↥(MulAction.stabilizer G (g • a)) = Nat.card ↥(MulAction.stabilizer G a)

The orbit invariance of card_stabilizer_of_orbitRel in the form wanted when the second point is presented as a translate of the first.

Not @[simp]: whether Nat.card (MulAction.stabilizer G (g • a)) is in normal form depends on the action, since a simp lemma for the particular • can rewrite inside it.

noncomputable def TauCeti.cardStabilizerOnOrbit {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (q : MulAction.orbitRel.Quotient G α) : ℕ

The stabiliser order as a function on the orbit space. card_stabilizer_of_orbitRel says the order is constant along an orbit, so it descends to MulAction.orbitRel.Quotient G α, which is the form wanted when the count is summed over orbits rather than over points.

Note this counts the stabiliser in G itself. When the action is not faithful the kernel sits inside every stabiliser and inflates each value by Nat.card of it — so for a group acting through a quotient, this is the order upstairs, not the order of the group that acts effectively. card_stabilizer_eq_card_subgroup_mul_card_stabilizer_quotient is the conversion between the two.

Equations

• TauCeti.cardStabilizerOnOrbit q = Quotient.liftOn' q (fun (a : α) => Nat.card ↥(MulAction.stabilizer G a)) ⋯

@[simp]

theorem TauCeti.cardStabilizerOnOrbit_mk {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (a : α) : cardStabilizerOnOrbit (Quotient.mk'' a) = Nat.card ↥(MulAction.stabilizer G a)

Evaluating cardStabilizerOnOrbit on the orbit of a recovers the stabiliser order at a.

theorem TauCeti.card_stabilizer_congr {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {H : Type u_3} {β : Type u_4} [Group H] [MulAction H β] (φ : G ≃* H) {f : α → β} (a : α) (hφ : ∀ (g : G), f (g • a) = φ g • f a) (hf : ∀ (g : G), f (g • a) = f a → g • a = a) : Nat.card ↥(MulAction.stabilizer H (f a)) = Nat.card ↥(MulAction.stabilizer G a)

Stabiliser orders are preserved by an equivariant injection: if f : α → β carries the G-action at a to the H-action along a group isomorphism φ : G ≃* H, and separates a from its translates, then φ maps the stabiliser of a onto that of f a, so the two have the same order.

Both hypotheses are asked for only at a, as that is all the count needs: a caller holding an equivariant injective f supplies fun g ↦ hφ g a and fun _ h ↦ hf h.

@[simp]

theorem TauCeti.cardStabilizerOnOrbit_orbitRelQuotientCongr {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {H : Type u_3} {β : Type u_4} [Group H] [MulAction H β] (φ : G ≃* H) (e : α ≃ β) (he : ∀ (g : G) (a : α), e (g • a) = φ g • e a) (q : MulAction.orbitRel.Quotient G α) : cardStabilizerOnOrbit ((MulAction.orbitRelQuotientCongr φ e he) q) = cardStabilizerOnOrbit q

MulAction.orbitRelQuotientCongr preserves the stabiliser order of an orbit.

@[simp]

theorem TauCeti.cardStabilizerOnOrbit_orbitRelQuotientSumEquiv_symm {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {β : Type u_3} [MulAction G β] (s : MulAction.orbitRel.Quotient G α ⊕ MulAction.orbitRel.Quotient G β) : cardStabilizerOnOrbit (MulAction.orbitRelQuotientSumEquiv.symm s) = Sum.elim cardStabilizerOnOrbit cardStabilizerOnOrbit s

MulAction.orbitRelQuotientSumEquiv preserves the stabiliser order of an orbit: the orbit it sends to Sum.inl q or to Sum.inr q has the stabiliser order of q.

theorem TauCeti.card_stabilizer_eq_card_ker_mul_card_stabilizer {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {H : Type u_3} [Group H] [MulAction H α] (f : G →* H) (hf : Function.Surjective ⇑f) (a : α) (hcompat : ∀ (g : G), f g • a = g • a) : Nat.card ↥(MulAction.stabilizer G a) = Nat.card ↥f.ker * Nat.card ↥(MulAction.stabilizer H a)

A surjection of acting groups divides stabiliser orders by its kernel: if f : G →* H is surjective and the H-action agrees with the G-action along f at the point a, then the stabiliser of a in G is Nat.card f.ker times its stabiliser in H.

Compatibility is asked for only at a, not globally, since that is all the count needs; a caller holding the global statement supplies fun g ↦ h g a.

theorem TauCeti.card_stabilizer_eq_card_subgroup_mul_card_stabilizer_quotient {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (N : Subgroup G) [N.Normal] [MulAction (G ⧸ N) α] (a : α) (hcompat : ∀ (g : G), ↑g • a = g • a) : Nat.card ↥(MulAction.stabilizer G a) = Nat.card ↥N * Nat.card ↥(MulAction.stabilizer (G ⧸ N) a)

Passing to a quotient group divides stabiliser orders by the subgroup: the case of card_stabilizer_eq_card_ker_mul_card_stabilizer for the quotient map, whose kernel is N.

This is the step from a matrix-group stabiliser order to the projective one. The divisor is Nat.card N in general; for SL(2, ℤ) ↠ PSL(2, ℤ) that is the centre ±1, so there the elliptic orders e_P are the matrix counts halved. For a Fuchsian Γ with -I ∉ Γ the two counts coincide.

theorem TauCeti.card_stabilizer_eq_card_subgroupOf_mul_card_stabilizer_map {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (N : Subgroup G) [N.Normal] [MulAction (G ⧸ N) α] (Γ : Subgroup G) (a : α) (hcompat : ∀ (g : ↥Γ), ↑↑g • a = ↑g • a) : Nat.card ↥(MulAction.stabilizer (↥Γ) a) = Nat.card ↥(N.subgroupOf Γ) * Nat.card ↥(MulAction.stabilizer (↥(Subgroup.map (QuotientGroup.mk' N) Γ)) a)

The relative form: a subgroup, and its image in the quotient. For Γ ≤ G, the stabiliser of a in Γ is Nat.card (N.subgroupOf Γ) — the part of N that Γ actually contains — times the stabiliser of a in the image of Γ in G ⧸ N.

card_stabilizer_eq_card_subgroup_mul_card_stabilizer_quotient is the case Γ = ⊤, where the divisor is all of N. The relative statement is what a Fuchsian group needs, where Γ is a subgroup of SL(2, ℤ) and N the centre: there the divisor measures how much of ±I lies in Γ, and the projective elliptic order e_P is the matrix stabiliser order divided by it. Evaluating that divisor is a fact about the particular Γ and is not proved here.

theorem TauCeti.card_stabilizer_subgroupOf {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {𝒢 ℋ : Subgroup G} (hle : 𝒢 ≤ ℋ) (a : α) : Nat.card ↥(MulAction.stabilizer (↥(𝒢.subgroupOf ℋ)) a) = Nat.card ↥(MulAction.stabilizer (↥𝒢) a)

Stabiliser orders agree across subgroupOf. For 𝒢 ≤ ℋ, a point has the same stabiliser order in 𝒢.subgroupOf ℋ as in 𝒢 itself.

This is the transport wanted whenever an orbit count produced inside ℋ has to be read against the 𝒢-orbit it weights, since cardStabilizerOnOrbit reads the order in 𝒢. Mathlib's stabilizerEquivStabilizer transports between two points of one group, not between two groups at one point, so it does not apply here.

theorem TauCeti.card_stabilizer_coset_eq_card_stabilizer_inv_smul {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (H : Subgroup G) (p : α) (g : G) : Nat.card ↥(MulAction.stabilizer ↥(MulAction.stabilizer G p) ↑g) = Nat.card ↥(MulAction.stabilizer (↥H) (g⁻¹ • p))

The stabiliser of a coset and the stabiliser of the translated point have the same order. The class of g in G ⧸ H is stabilised inside stabilizer G p by exactly as many elements as g⁻¹ • p is stabilised by inside H.

Stated at the level of a single group acting on α; the two-group form used below is the instance G := ↥ℋ, H := 𝒢.subgroupOf ℋ, g := ↑h.

theorem TauCeti.stabilizer_finset_eq_bot_of_prime_card {G : Type u_3} [Group G] [Fintype G] [DecidableEq G] (hG : Nat.Prime (Nat.card G)) {S : Finset G} (hne : S.Nonempty) (hS : S ≠ Finset.univ) : MulAction.stabilizer G S = ⊥

Translation by a group of prime order is free on the nonempty proper subsets. If G has prime order, the stabiliser of a nonempty finset S ≠ univ of G under translation is trivial.

theorem MonoidHom.comap_stabilizer_eq_ker {G : Type u_1} {α : Type u_2} [Group G] (ρ : G →* Equiv.Perm α) (i : α) (hi : MulAction.stabilizer (↥ρ.range) i = ⊥) : Subgroup.comap ρ (MulAction.stabilizer (Equiv.Perm α) i) = ρ.ker

If a point has trivial stabiliser under the image of a permutation representation, then its stabiliser in the source is the kernel of the representation.

theorem MonoidHom.normal_comap_stabilizer_iff_isCancelSMul {G : Type u_1} {α : Type u_2} [Group G] (ρ : G →* Equiv.Perm α) (hρ : MulAction.IsPretransitive (↥ρ.range) α) (i : α) : (Subgroup.comap ρ (MulAction.stabilizer (Equiv.Perm α) i)).Normal ↔ IsCancelSMul (↥ρ.range) α

For a transitive permutation representation, a point stabiliser is normal in the source exactly when the image acts freely.