Orbit-stabiliser for a transitive action

Mathlib's MulAction.ofQuotientStabilizer sends the coset of g in G ⧸ stabilizer G b to g • b; it is injective by MulAction.injective_ofQuotientStabilizer, and its image is the orbit of b, which is the orbit-stabiliser theorem. When the action is transitive that orbit is all of X, so the map is a bijection. This file records that specialisation, together with the equivariance -- Mathlib's MulAction.ofQuotientStabilizer_smul -- that makes it an isomorphism of G-sets rather than a bare bijection.

Main definitions

• TauCeti.quotientStabilizerEquiv: for a transitive action of G on X and a point b : X, the equivalence G ⧸ stabilizer G b ≃ X sending the coset of g to g • b.

Main results

• TauCeti.quotientStabilizerEquiv_mk: its value on a coset, and TauCeti.quotientStabilizerEquiv_smul: its equivariance.

Implementation notes

The equivalence is unbundled -- an Equiv of types together with a separate equivariance lemma -- because that is the shape the constructions consuming it take their argument in, for instance TauCeti.ofMulActionEquivCongr, which builds the induced equivalence of permutation representations.

noncomputable def TauCeti.quotientStabilizerEquiv (G : Type u_1) {X : Type u_2} [Group G] [MulAction G X] [MulAction.IsPretransitive G X] (b : X) : G ⧸ MulAction.stabilizer G b ≃ X

Orbit-stabiliser for a transitive action: the coset space of the stabiliser of a point is the set acted on, the coset of g corresponding to g • b. This is MulAction.ofQuotientStabilizer, which transitivity makes surjective.

Equations

• TauCeti.quotientStabilizerEquiv G b = Equiv.ofBijective (MulAction.ofQuotientStabilizer G b) ⋯

@[simp]

theorem TauCeti.quotientStabilizerEquiv_mk (G : Type u_1) {X : Type u_2} [Group G] [MulAction G X] [MulAction.IsPretransitive G X] (b : X) (g : G) : (quotientStabilizerEquiv G b) ↑g = g • b

The computation rule for TauCeti.quotientStabilizerEquiv: on the coset represented by g it takes the value g • b.

@[simp]

theorem TauCeti.quotientStabilizerEquiv_smul (G : Type u_1) {X : Type u_2} [Group G] [MulAction G X] [MulAction.IsPretransitive G X] (b : X) (g : G) (q : G ⧸ MulAction.stabilizer G b) : (quotientStabilizerEquiv G b) (g • q) = g • (quotientStabilizerEquiv G b) q

The identification of the coset space with the set acted on is equivariant.