Diagonal orbits and stabilizer orbits

If G acts transitively on Y, fixing a point y : Y identifies the diagonal orbit space of X × Y with the orbit space of X under the stabilizer of y. This is useful for replacing an object with a moving marked point by an object whose mark is fixed once and for all.

The forward map is canonical: it sends the stabilizer orbit of x to the diagonal orbit of (x, y). Its injectivity does not require transitivity. Transitivity supplies surjectivity; the inverse sends the orbit of (x, g • y) to the stabilizer orbit of g⁻¹ • x.

def TauCeti.MulAction.orbitRelQuotientStabilizerMap {G : Type u_1} {X : Type u_2} {Y : Type u_3} [Group G] [MulAction G X] [MulAction G Y] (y : Y) : MulAction.orbitRel.Quotient (↥(MulAction.stabilizer G y)) X → MulAction.orbitRel.Quotient G (X × Y)

Attach a fixed mark y to a stabilizer orbit, giving a diagonal orbit.

Equations

• TauCeti.MulAction.orbitRelQuotientStabilizerMap y = Quotient.map' (fun (x : X) => (x, y)) ⋯

@[simp]

theorem TauCeti.MulAction.orbitRelQuotientStabilizerMap_mk {G : Type u_1} {X : Type u_2} {Y : Type u_3} [Group G] [MulAction G X] [MulAction G Y] (y : Y) (x : X) : orbitRelQuotientStabilizerMap y (Quotient.mk'' x) = Quotient.mk'' (x, y)

theorem TauCeti.MulAction.orbitRelQuotientStabilizerMap_injective {G : Type u_1} {X : Type u_2} {Y : Type u_3} [Group G] [MulAction G X] [MulAction G Y] (y : Y) : Function.Injective (orbitRelQuotientStabilizerMap y)

Fixing the mark identifies stabilizer orbits faithfully with diagonal orbits.

theorem TauCeti.MulAction.orbitRelQuotientStabilizerMap_surjective {G : Type u_1} {X : Type u_2} {Y : Type u_3} [Group G] [MulAction G X] [MulAction G Y] [MulAction.IsPretransitive G Y] (y : Y) : Function.Surjective (orbitRelQuotientStabilizerMap y)

Every diagonal orbit admits a representative with mark y when the marking action is transitive.

noncomputable def TauCeti.MulAction.orbitRelQuotientStabilizerEquiv {G : Type u_1} {X : Type u_2} {Y : Type u_3} [Group G] [MulAction G X] [MulAction G Y] [MulAction.IsPretransitive G Y] (y : Y) : MulAction.orbitRel.Quotient (↥(MulAction.stabilizer G y)) X ≃ MulAction.orbitRel.Quotient G (X × Y)

Stabilizer orbits with a fixed mark are exactly diagonal orbits with a moving mark.

Equations

• TauCeti.MulAction.orbitRelQuotientStabilizerEquiv y = Equiv.ofBijective (TauCeti.MulAction.orbitRelQuotientStabilizerMap y) ⋯

@[simp]

theorem TauCeti.MulAction.orbitRelQuotientStabilizerEquiv_mk {G : Type u_1} {X : Type u_2} {Y : Type u_3} [Group G] [MulAction G X] [MulAction G Y] [MulAction.IsPretransitive G Y] (y : Y) (x : X) : (orbitRelQuotientStabilizerEquiv y) (Quotient.mk'' x) = Quotient.mk'' (x, y)

@[simp]

theorem TauCeti.MulAction.orbitRelQuotientStabilizerEquiv_symm_mk {G : Type u_1} {X : Type u_2} {Y : Type u_3} [Group G] [MulAction G X] [MulAction G Y] [MulAction.IsPretransitive G Y] (y : Y) (x : X) : (orbitRelQuotientStabilizerEquiv y).symm (Quotient.mk'' (x, y)) = Quotient.mk'' x

@[simp]

theorem TauCeti.MulAction.orbitRelQuotientStabilizerEquiv_symm_mk_smul {G : Type u_1} {X : Type u_2} {Y : Type u_3} [Group G] [MulAction G X] [MulAction G Y] [MulAction.IsPretransitive G Y] (y : Y) (x : X) (g : G) : (orbitRelQuotientStabilizerEquiv y).symm (Quotient.mk'' (x, g • y)) = Quotient.mk'' (g⁻¹ • x)

Move the mark back to y by applying the inverse translator to the object as well.