Quotients of torsors by normal subgroups

Let G be a group acting on P and let H be a normal subgroup of G. The space MulAction.orbitRel.Quotient H P of H-orbits in P carries an action of the quotient group G ⧸ H (MulAction.orbitRel.Quotient.instMulActionQuotientGroup), given on representatives by (g : G ⧸ H) • ⟦p⟧ = ⟦g • p⟧. If P is a torsor under G, then the orbit space is a torsor under G ⧸ H, with ⟦p⟧ /ₛ ⟦q⟧ = (p /ₛ q : G ⧸ H).

Additively: if P is an AddTorsor under G and H is a normal additive subgroup, then the space of H-orbits is an AddTorsor under G ⧸ H. This is how a torsor under a group of classes descends to a torsor under a quotient of that group.

Main definitions

• MulAction.orbitRel.Quotient.instTorsorQuotientGroup: the space of H-orbits of a G-torsor is a G ⧸ H-torsor, and its additive version.

Main results

• MulAction.orbitRel.Quotient.mk_eq_mk_iff_sdiv_mem: two points of a torsor lie in the same H-orbit exactly when their difference lies in H.
• MulAction.orbitRel.Quotient.mk_sdiv_mk: the difference on the orbit space is computed on representatives.

theorem MulAction.orbitRel.Quotient.orbitRel_iff_sdiv_mem {G : Type u_1} {P : Type u_2} [Group G] (H : Subgroup G) [Torsor G P] {p q : P} : (orbitRel (↥H) P) p q ↔ p /ₛ q ∈ H

Two points of a torsor lie in the same H-orbit exactly when their difference lies in H.

theorem AddAction.orbitRel.Quotient.orbitRel_iff_vsub_mem {G : Type u_1} {P : Type u_2} [AddGroup G] (H : AddSubgroup G) [AddTorsor G P] {p q : P} : (orbitRel (↥H) P) p q ↔ p -ᵥ q ∈ H

Two points of an additive torsor lie in the same H-orbit exactly when their difference lies in H.

theorem MulAction.orbitRel.Quotient.mk_eq_mk_iff_sdiv_mem {G : Type u_1} {P : Type u_2} [Group G] (H : Subgroup G) [Torsor G P] {p q : P} : Quotient.mk'' p = Quotient.mk'' q ↔ p /ₛ q ∈ H

Two points of a torsor have the same H-orbit exactly when their difference lies in H.

theorem AddAction.orbitRel.Quotient.mk_eq_mk_iff_vsub_mem {G : Type u_1} {P : Type u_2} [AddGroup G] (H : AddSubgroup G) [AddTorsor G P] {p q : P} : Quotient.mk'' p = Quotient.mk'' q ↔ p -ᵥ q ∈ H

Two points of an additive torsor have the same H-orbit exactly when their difference lies in H.

theorem MulAction.orbitRel.Quotient.mk_sdiv_eq_mk_sdiv {G : Type u_1} {P : Type u_2} [Group G] (H : Subgroup G) [Torsor G P] [H.Normal] {p p' q q' : P} (hp : (orbitRel (↥H) P) p p') (hq : (orbitRel (↥H) P) q q') : ↑(p /ₛ q) = ↑(p' /ₛ q')

The class of p /ₛ q in G ⧸ H depends only on the H-orbits of p and q.

theorem AddAction.orbitRel.Quotient.mk_vsub_eq_mk_vsub {G : Type u_1} {P : Type u_2} [AddGroup G] (H : AddSubgroup G) [AddTorsor G P] [H.Normal] {p p' q q' : P} (hp : (orbitRel (↥H) P) p p') (hq : (orbitRel (↥H) P) q q') : ↑(p -ᵥ q) = ↑(p' -ᵥ q')

The class of p -ᵥ q in G ⧸ H depends only on the H-orbits of p and q.

@[instance_reducible]

instance MulAction.orbitRel.Quotient.instSDivQuotientGroup {G : Type u_1} {P : Type u_2} [Group G] (H : Subgroup G) [Torsor G P] [H.Normal] : SDiv (G ⧸ H) (Quotient (↥H) P)

The difference of two H-orbits in a torsor, as an element of G ⧸ H.

@[instance_reducible]

instance AddAction.orbitRel.Quotient.instVSubQuotientAddGroup {G : Type u_1} {P : Type u_2} [AddGroup G] (H : AddSubgroup G) [AddTorsor G P] [H.Normal] : VSub (G ⧸ H) (Quotient (↥H) P)

The difference of two H-orbits in an additive torsor, as an element of G ⧸ H.

@[simp]

theorem MulAction.orbitRel.Quotient.mk_sdiv_mk {G : Type u_1} {P : Type u_2} [Group G] (H : Subgroup G) [Torsor G P] [H.Normal] (p q : P) : Quotient.mk'' p /ₛ Quotient.mk'' q = ↑(p /ₛ q)

The difference of two H-orbits is computed on representatives.

@[simp]

theorem AddAction.orbitRel.Quotient.mk_vsub_mk {G : Type u_1} {P : Type u_2} [AddGroup G] (H : AddSubgroup G) [AddTorsor G P] [H.Normal] (p q : P) : Quotient.mk'' p -ᵥ Quotient.mk'' q = ↑(p -ᵥ q)

The difference of two H-orbits is computed on representatives.

@[instance_reducible]

instance MulAction.orbitRel.Quotient.instTorsorQuotientGroup {G : Type u_1} {P : Type u_2} [Group G] (H : Subgroup G) [Torsor G P] [H.Normal] : Torsor (G ⧸ H) (Quotient (↥H) P)

The space of H-orbits of a G-torsor is a torsor under G ⧸ H.

@[instance_reducible]

instance AddAction.orbitRel.Quotient.instAddTorsorQuotientAddGroup {G : Type u_1} {P : Type u_2} [AddGroup G] (H : AddSubgroup G) [AddTorsor G P] [H.Normal] : AddTorsor (G ⧸ H) (Quotient (↥H) P)

The space of H-orbits of an additive G-torsor is an additive torsor under G ⧸ H.