Documentation

TauCeti.GroupTheory.GroupAction.Transitive

Transitive actions #

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.

It also records one closure property of pretransitivity, TauCeti.isPretransitive_prod_left, which needs no group and no action laws and so comes first, before any of the above structure is assumed.

Main definitions #

Main results #

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.

source
theorem TauCeti.isPretransitive_prod_left {G : Type u_1} (X : Type u_2) (Y : Type u_3) [SMul G X] [SMul G Y] [MulAction.IsPretransitive G X] [Subsingleton Y] :
MulAction.IsPretransitive G (X × Y)

Pairing a pretransitive action with a subsingleton leaves it pretransitive. A scalar carrying p.1 to q.1 carries p to q outright, the second coordinates being equal for want of anywhere else to be, so neither a monoid nor any action law enters.

Y is allowed to be empty, in which case X × Y is empty and the statement is vacuous. Counting the orbits of such a product -- via TauCeti.MulAction.card_orbitRelQuotient_eq_one, which is the value Burnside's lemma takes on it -- needs more than this: a genuine MulAction of a group, and Nonempty to rule the empty case back out.

source
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
Instances For
    source
    @[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.

    source
    @[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.

    source
    theorem TauCeti.natCard_dvd_natCard_of_isPretransitive (G : Type u_1) {X : Type u_2} [Group G] [MulAction G X] [MulAction.IsPretransitive G X] [Nonempty X] :
    Nat.card X ∣ Nat.card G

    If G acts transitively on a nonempty set X, then the number of points of X divides the order of G: it is the index of a point stabiliser, by MulAction.index_stabilizer_of_transitive. Both cardinalities are Nat.card, so the statement also holds, trivially, for infinite G.

    source
    theorem TauCeti.stabilizer_eq_bot_of_natCard_eq {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [MulAction.IsPretransitive G X] [Finite X] (h : Nat.card G = Nat.card X) (x : X) :
    MulAction.stabilizer G x = ⊥

    A transitive action of a group with as many elements as the finite set acted on is regular: every point stabiliser is trivial. The index of a point stabiliser is the number of points, by MulAction.index_stabilizer_of_transitive, so the stabiliser has one element.

    source
    theorem TauCeti.eq_one_of_natCard_eq_of_smul_eq_self {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [MulAction.IsPretransitive G X] [Finite X] (h : Nat.card G = Nat.card X) {g : G} {x : X} (hgx : g • x = x) :
    g = 1

    In a transitive action of a group with as many elements as the finite set acted on, an element fixing a point is the identity.

    source
    noncomputable def MonoidHom.quotientComapStabilizerEquiv {G : Type u_1} {X : Type u_2} [Group G] (ρ : G →* Equiv.Perm X) (hρ : MulAction.IsPretransitive (↥ρ.range) X) (x : X) :
    G ⧸ Subgroup.comap ρ (MulAction.stabilizer (Equiv.Perm X) x) ≃ X

    Orbit-stabiliser for a transitive permutation representation ρ : G →* Perm X: the coset space of the point stabiliser ρ⁻¹ (stabilizer x) is X, the coset of g corresponding to ρ g x. This is TauCeti.quotientStabilizerEquiv for the action of G on X through ρ.

    Equations
    Instances For
      source
      @[simp]
      theorem MonoidHom.quotientComapStabilizerEquiv_mk {G : Type u_1} {X : Type u_2} [Group G] (ρ : G →* Equiv.Perm X) (hρ : MulAction.IsPretransitive (↥ρ.range) X) (x : X) (g : G) :
      (ρ.quotientComapStabilizerEquiv hρ x) ↑g = (ρ g) x

      The computation rule for MonoidHom.quotientComapStabilizerEquiv: the coset of g goes to ρ g x.

      source
      @[simp]
      theorem MonoidHom.quotientComapStabilizerEquiv_smul {G : Type u_1} {X : Type u_2} [Group G] (ρ : G →* Equiv.Perm X) (hρ : MulAction.IsPretransitive (↥ρ.range) X) (x : X) (g : G) (q : G ⧸ Subgroup.comap ρ (MulAction.stabilizer (Equiv.Perm X) x)) :
      (ρ.quotientComapStabilizerEquiv hρ x) (g • q) = (ρ g) ((ρ.quotientComapStabilizerEquiv hρ x) q)

      The identification of the coset space with X carries left multiplication by g to ρ g.