Torsors of group actions

This file defines torsors of additive and multiplicative group actions.

Notation

The group elements are referred to as acting on points. This file uses the notation +ᵥ for adding a group element to a point and -ᵥ for subtracting two points to produce a group element, as well as • and /ₛ for the corresponding operations in multiplicative torsors.

Implementation notes

Affine spaces are a motivating example of additive torsors. Additional simply transitive actions which give rise to torsors include the action of the Weyl group on Weyl chambers, the action of non-zero scalars on the non-vanishing elements of the top exterior power of a finite-dimensional vector space, the action of the general linear group of a vector space on the bases of that space, and the monodromy action of the fundamental group of a space on a fibre of its universal cover. Both the additive and multiplicative notation will be useful to formalise such examples.

Notation

• v +ᵥ p is a notation for VAdd.vadd, the left action of an additive monoid;
• p₁ -ᵥ p₂ is a notation for VSub.vsub, the difference between two points in an additive torsor as an element of the corresponding additive group;
• v • p is a notation for SMul.smul, the left action of a multiplicative monoid;
• p₁ /ₛ p₂ is a notation for SDiv.sdiv, the quotient of two points in a multiplicative torsor as an element of the corresponding multiplicative group;

References

• https://en.wikipedia.org/wiki/Principal_homogeneous_space
• https://en.wikipedia.org/wiki/Affine_space

class AddTorsor (G : outParam (Type u_1)) (P : Type u_2) [AddGroup G] extends AddAction G P, VSub G P : Type (max u_1 u_2)

An AddTorsor G P gives a structure to the nonempty type P, acted on by an AddGroup G with a transitive and free action given by the +ᵥ operation and a corresponding subtraction given by the -ᵥ operation. In the case of a vector space, it is an affine space.

• vadd : G → P → P
• add_vadd (g₁ g₂ : G) (p : P) : (g₁ + g₂) +ᵥ p = g₁ +ᵥ g₂ +ᵥ p
• zero_vadd (p : P) : 0 +ᵥ p = p
• vsub : P → P → G
• nonempty : Nonempty P
• vsub_vadd' (p₁ p₂ : P) : (p₁ -ᵥ p₂) +ᵥ p₂ = p₁

  Torsor subtraction and addition with the same element cancels out.

• vadd_vsub' (g : G) (p : P) : (g +ᵥ p) -ᵥ p = g

  Torsor addition and subtraction with the same element cancels out.

class Torsor (G : outParam (Type u_1)) (P : Type u_2) [Group G] extends MulAction G P, SDiv G P : Type (max u_1 u_2)

A Torsor G P gives a structure to the nonempty type P, acted on by a Group G with a transitive and free action given by the • operation and a corresponding division given by the /ₛ operation.

• smul : G → P → P
• mul_smul (x y : G) (b : P) : (x * y) • b = x • y • b
• one_smul (b : P) : 1 • b = b
• sdiv : P → P → G
• nonempty : Nonempty P
• sdiv_smul' (p₁ p₂ : P) : (p₁ /ₛ p₂) • p₂ = p₁

  Scalar division and multiplication with the same element cancels out.

• smul_sdiv' (g : G) (p : P) : g • p /ₛ p = g

  Scalar multiplication and division with the same element cancels out.

@[implicit_reducible]

instance Group.instTorsor (G : Type u_1) [Group G] : Torsor G G

A Group G is a torsor for itself.

Equations

• Group.instTorsor G = { toMulAction := Monoid.toMulAction G, sdiv := Div.div, nonempty := ⋯, sdiv_smul' := ⋯, smul_sdiv' := ⋯ }

@[implicit_reducible]

instance AddGroup.instAddTorsor (G : Type u_1) [AddGroup G] : AddTorsor G G

An AddGroup G is a torsor for itself.

Equations

• AddGroup.instAddTorsor G = { toAddAction := AddMonoid.toAddAction G, vsub := Sub.sub, nonempty := ⋯, vsub_vadd' := ⋯, vadd_vsub' := ⋯ }

@[deprecated AddGroup.instAddTorsor (since := "2026-05-04")]

def addGroupIsAddTorsor (G : Type u_1) [AddGroup G] : AddTorsor G G

Alias of AddGroup.instAddTorsor.

---

An AddGroup G is a torsor for itself.

Equations

• addGroupIsAddTorsor = AddGroup.instAddTorsor

@[simp]

theorem sdiv_eq_div {G : Type u_1} [Group G] (g₁ g₂ : G) : g₁ /ₛ g₂ = g₁ / g₂

Simplify division for a torsor for a Group G over itself.

@[simp]

theorem vsub_eq_sub {G : Type u_1} [AddGroup G] (g₁ g₂ : G) : g₁ -ᵥ g₂ = g₁ - g₂

Simplify subtraction for a torsor for an AddGroup G over itself.

@[simp]

theorem sdiv_smul {G : Type u_1} {P : Type u_2} [Group G] [T : Torsor G P] (p₁ p₂ : P) : (p₁ /ₛ p₂) • p₂ = p₁

Scalar multiplying the result of dividing another point produces that point.

@[simp]

theorem vsub_vadd {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] (p₁ p₂ : P) : (p₁ -ᵥ p₂) +ᵥ p₂ = p₁

Adding the result of subtracting from another point produces that point.

@[simp]

theorem smul_sdiv {G : Type u_1} {P : Type u_2} [Group G] [T : Torsor G P] (g : G) (p : P) : g • p /ₛ p = g

Multiplying by a group element then dividing by the original point produces that group element.

@[simp]

theorem vadd_vsub {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] (g : G) (p : P) : (g +ᵥ p) -ᵥ p = g

Adding a group element then subtracting the original point produces that group element.

theorem smul_right_cancel {G : Type u_1} {P : Type u_2} [Group G] [T : Torsor G P] {g₁ g₂ : G} (p : P) (h : g₁ • p = g₂ • p) : g₁ = g₂

If the same point multiplied with two group elements produces equal results, those group elements are equal.

theorem vadd_right_cancel {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] {g₁ g₂ : G} (p : P) (h : g₁ +ᵥ p = g₂ +ᵥ p) : g₁ = g₂

If the same point added to two group elements produces equal results, those group elements are equal.

@[simp]

theorem smul_right_cancel_iff {G : Type u_1} {P : Type u_2} [Group G] [T : Torsor G P] {g₁ g₂ : G} (p : P) : g₁ • p = g₂ • p ↔ g₁ = g₂

@[simp]

theorem vadd_right_cancel_iff {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] {g₁ g₂ : G} (p : P) : g₁ +ᵥ p = g₂ +ᵥ p ↔ g₁ = g₂

theorem smul_right_injective' {G : Type u_1} {P : Type u_2} [Group G] [T : Torsor G P] (p : P) : Function.Injective fun (x : G) => x • p

Multiplying a group element with the point p is an injective function.

theorem vadd_right_injective {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] (p : P) : Function.Injective fun (x : G) => x +ᵥ p

Adding a group element to the point p is an injective function.

theorem smul_sdiv_assoc {G : Type u_1} {P : Type u_2} [Group G] [T : Torsor G P] (g : G) (p₁ p₂ : P) : g • p₁ /ₛ p₂ = g * (p₁ /ₛ p₂)

Multiplying a group element with a point, then dividing by another point, produces the same result as dividing the points then multiplying the group element.

theorem vadd_vsub_assoc {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] (g : G) (p₁ p₂ : P) : (g +ᵥ p₁) -ᵥ p₂ = g + (p₁ -ᵥ p₂)

Adding a group element to a point, then subtracting another point, produces the same result as subtracting the points then adding the group element.

@[simp]

theorem sdiv_self {G : Type u_1} {P : Type u_2} [Group G] [T : Torsor G P] (p : P) : p /ₛ p = 1

Dividing a point by itself produces 1.

@[simp]

theorem vsub_self {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] (p : P) : p -ᵥ p = 0

Subtracting a point from itself produces 0.

theorem eq_of_sdiv_eq_one {G : Type u_1} {P : Type u_2} [Group G] [T : Torsor G P] {p₁ p₂ : P} (h : p₁ /ₛ p₂ = 1) : p₁ = p₂

If dividing two points produces 1, they are equal.

theorem eq_of_vsub_eq_zero {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] {p₁ p₂ : P} (h : p₁ -ᵥ p₂ = 0) : p₁ = p₂

If subtracting two points produces 0, they are equal.

@[simp]

theorem sdiv_eq_one_iff_eq {G : Type u_1} {P : Type u_2} [Group G] [T : Torsor G P] {p₁ p₂ : P} : p₁ /ₛ p₂ = 1 ↔ p₁ = p₂

Dividing two points produces 1 if and only if they are equal.

@[simp]

theorem vsub_eq_zero_iff_eq {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] {p₁ p₂ : P} : p₁ -ᵥ p₂ = 0 ↔ p₁ = p₂

Subtracting two points produces 0 if and only if they are equal.

theorem sdiv_ne_one {G : Type u_1} {P : Type u_2} [Group G] [T : Torsor G P] {p q : P} : p /ₛ q ≠ 1 ↔ p ≠ q

theorem vsub_ne_zero {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] {p q : P} : p -ᵥ q ≠ 0 ↔ p ≠ q

@[simp]

theorem sdiv_mul_sdiv_cancel {G : Type u_1} {P : Type u_2} [Group G] [T : Torsor G P] (p₁ p₂ p₃ : P) : (p₁ /ₛ p₂) * (p₂ /ₛ p₃) = p₁ /ₛ p₃

Cancellation multiplying the results of two divisions.

@[simp]

theorem vsub_add_vsub_cancel {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] (p₁ p₂ p₃ : P) : p₁ -ᵥ p₂ + (p₂ -ᵥ p₃) = p₁ -ᵥ p₃

Cancellation adding the results of two subtractions.

@[simp]

theorem inv_sdiv_eq_sdiv_rev {G : Type u_1} {P : Type u_2} [Group G] [T : Torsor G P] (p₁ p₂ : P) : (p₁ /ₛ p₂)⁻¹ = p₂ /ₛ p₁

Dividing two points in the reverse order produces the inverse of dividing them.

@[simp]

theorem neg_vsub_eq_vsub_rev {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] (p₁ p₂ : P) : -(p₁ -ᵥ p₂) = p₂ -ᵥ p₁

Subtracting two points in the reverse order produces the negation of subtracting them.

theorem smul_sdiv_eq_div_sdiv {G : Type u_1} {P : Type u_2} [Group G] [T : Torsor G P] (g : G) (p q : P) : g • p /ₛ q = g / (q /ₛ p)

theorem vadd_vsub_eq_sub_vsub {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] (g : G) (p q : P) : (g +ᵥ p) -ᵥ q = g - (q -ᵥ p)

theorem sdiv_smul_eq_sdiv_div {G : Type u_1} {P : Type u_2} [Group G] [T : Torsor G P] (p₁ p₂ : P) (g : G) : p₁ /ₛ g • p₂ = (p₁ /ₛ p₂) / g

Dividing by the result of multiplying with a group element produces the same result as dividing the points and dividing by that group element.

theorem vsub_vadd_eq_vsub_sub {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] (p₁ p₂ : P) (g : G) : p₁ -ᵥ (g +ᵥ p₂) = p₁ -ᵥ p₂ - g

Subtracting the result of adding a group element produces the same result as subtracting the points and subtracting that group element.

@[simp]

theorem sdiv_div_sdiv_cancel_right {G : Type u_1} {P : Type u_2} [Group G] [T : Torsor G P] (p₁ p₂ p₃ : P) : (p₁ /ₛ p₃) / (p₂ /ₛ p₃) = p₁ /ₛ p₂

Cancellation dividing the results of two divisions.

@[simp]

theorem vsub_sub_vsub_cancel_right {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] (p₁ p₂ p₃ : P) : p₁ -ᵥ p₃ - (p₂ -ᵥ p₃) = p₁ -ᵥ p₂

Cancellation subtracting the results of two subtractions.

theorem eq_smul_iff_sdiv_eq {G : Type u_1} {P : Type u_2} [Group G] [T : Torsor G P] (p₁ : P) (g : G) (p₂ : P) : p₁ = g • p₂ ↔ p₁ /ₛ p₂ = g

Convert between an equality with multiplying a group element with a point and an equality of a division of two points with a group element.

theorem eq_vadd_iff_vsub_eq {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] (p₁ : P) (g : G) (p₂ : P) : p₁ = g +ᵥ p₂ ↔ p₁ -ᵥ p₂ = g

Convert between an equality with adding a group element to a point and an equality of a subtraction of two points with a group element.

theorem smul_eq_smul_iff_inv_mul_eq_sdiv {G : Type u_1} {P : Type u_2} [Group G] [T : Torsor G P] {v₁ v₂ : G} {p₁ p₂ : P} : v₁ • p₁ = v₂ • p₂ ↔ v₁⁻¹ * v₂ = p₁ /ₛ p₂

theorem vadd_eq_vadd_iff_neg_add_eq_vsub {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] {v₁ v₂ : G} {p₁ p₂ : P} : v₁ +ᵥ p₁ = v₂ +ᵥ p₂ ↔ -v₁ + v₂ = p₁ -ᵥ p₂

@[simp]

theorem smul_sdiv_smul_cancel_right {G : Type u_1} {P : Type u_2} [Group G] [T : Torsor G P] (v₁ v₂ : G) (p : P) : v₁ • p /ₛ v₂ • p = v₁ / v₂

@[simp]

theorem vadd_vsub_vadd_cancel_right {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] (v₁ v₂ : G) (p : P) : (v₁ +ᵥ p) -ᵥ (v₂ +ᵥ p) = v₁ - v₂

def Equiv.smulConst {G : Type u_1} {P : Type u_2} [Group G] [Torsor G P] (p : P) : G ≃ P

v ↦ v • p as an equivalence.

Equations

• Equiv.smulConst p = { toFun := fun (v : G) => v • p, invFun := fun (p' : P) => p' /ₛ p, left_inv := ⋯, right_inv := ⋯ }

def Equiv.vaddConst {G : Type u_1} {P : Type u_2} [AddGroup G] [AddTorsor G P] (p : P) : G ≃ P

v ↦ v +ᵥ p as an equivalence.

Equations

• Equiv.vaddConst p = { toFun := fun (v : G) => v +ᵥ p, invFun := fun (p' : P) => p' -ᵥ p, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.coe_smulConst {G : Type u_1} {P : Type u_2} [Group G] [Torsor G P] (p : P) : ⇑(smulConst p) = fun (v : G) => v • p

@[simp]

theorem Equiv.coe_vaddConst {G : Type u_1} {P : Type u_2} [AddGroup G] [AddTorsor G P] (p : P) : ⇑(vaddConst p) = fun (v : G) => v +ᵥ p

@[simp]

theorem Equiv.coe_smulConst_symm {G : Type u_1} {P : Type u_2} [Group G] [Torsor G P] (p : P) : ⇑(smulConst p).symm = fun (p' : P) => p' /ₛ p

@[simp]

theorem Equiv.coe_vaddConst_symm {G : Type u_1} {P : Type u_2} [AddGroup G] [AddTorsor G P] (p : P) : ⇑(vaddConst p).symm = fun (p' : P) => p' -ᵥ p

def Equiv.constSDiv {G : Type u_1} {P : Type u_2} [Group G] [Torsor G P] (p : P) : P ≃ G

p' ↦ p /ₛ p' as an equivalence.

Equations

• Equiv.constSDiv p = { toFun := fun (x : P) => p /ₛ x, invFun := fun (x : G) => x⁻¹ • p, left_inv := ⋯, right_inv := ⋯ }

def Equiv.constVSub {G : Type u_1} {P : Type u_2} [AddGroup G] [AddTorsor G P] (p : P) : P ≃ G

p' ↦ p -ᵥ p' as an equivalence.

Equations

• Equiv.constVSub p = { toFun := fun (x : P) => p -ᵥ x, invFun := fun (x : G) => -x +ᵥ p, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.coe_constSDiv {G : Type u_1} {P : Type u_2} [Group G] [Torsor G P] (p : P) : ⇑(constSDiv p) = fun (x : P) => p /ₛ x

@[simp]

theorem Equiv.coe_constVSub {G : Type u_1} {P : Type u_2} [AddGroup G] [AddTorsor G P] (p : P) : ⇑(constVSub p) = fun (x : P) => p -ᵥ x

@[simp]

theorem Equiv.coe_constSDiv_symm {G : Type u_1} {P : Type u_2} [Group G] [Torsor G P] (p : P) : ⇑(constSDiv p).symm = fun (v : G) => v⁻¹ • p

@[simp]

theorem Equiv.coe_constVSub_symm {G : Type u_1} {P : Type u_2} [AddGroup G] [AddTorsor G P] (p : P) : ⇑(constVSub p).symm = fun (v : G) => -v +ᵥ p

def Equiv.constSMul {G : Type u_1} (P : Type u_2) [Group G] [Torsor G P] (v : G) : Perm P

The permutation given by p ↦ v • p.

Equations

• Equiv.constSMul P v = { toFun := fun (x : P) => v • x, invFun := fun (x : P) => v⁻¹ • x, left_inv := ⋯, right_inv := ⋯ }

def Equiv.constVAdd {G : Type u_1} (P : Type u_2) [AddGroup G] [AddTorsor G P] (v : G) : Perm P

The permutation given by p ↦ v +ᵥ p.

Equations

• Equiv.constVAdd P v = { toFun := fun (x : P) => v +ᵥ x, invFun := fun (x : P) => -v +ᵥ x, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.coe_constSMul {G : Type u_1} (P : Type u_2) [Group G] [Torsor G P] (v : G) : ⇑(constSMul P v) = fun (x : P) => v • x

@[simp]

theorem Equiv.coe_constVAdd {G : Type u_1} (P : Type u_2) [AddGroup G] [AddTorsor G P] (v : G) : ⇑(constVAdd P v) = fun (x : P) => v +ᵥ x

def Equiv.pointReflection {G : Type u_3} {P : Type u_4} [AddGroup G] [AddTorsor G P] (x : P) : Perm P

Point reflection in x as a permutation.

Equations

• Equiv.pointReflection x = (Equiv.constVSub x).trans (Equiv.vaddConst x)

theorem Equiv.pointReflection_apply {G : Type u_3} {P : Type u_4} [AddGroup G] [AddTorsor G P] (x y : P) : (pointReflection x) y = (x -ᵥ y) +ᵥ x

@[simp]

theorem Equiv.pointReflection_vsub_left {G : Type u_3} {P : Type u_4} [AddGroup G] [AddTorsor G P] (x y : P) : (pointReflection x) y -ᵥ x = x -ᵥ y

@[simp]

theorem Equiv.pointReflection_vsub_right {G : Type u_3} {P : Type u_4} [AddGroup G] [AddTorsor G P] (x y : P) : (pointReflection x) y -ᵥ y = 2 • (x -ᵥ y)

@[simp]

theorem Equiv.pointReflection_symm {G : Type u_3} {P : Type u_4} [AddGroup G] [AddTorsor G P] (x : P) : Equiv.symm (pointReflection x) = pointReflection x

@[simp]

theorem Equiv.pointReflection_self {G : Type u_3} {P : Type u_4} [AddGroup G] [AddTorsor G P] (x : P) : (pointReflection x) x = x

theorem Equiv.pointReflection_involutive {G : Type u_3} {P : Type u_4} [AddGroup G] [AddTorsor G P] (x : P) : Function.Involutive ⇑(pointReflection x)

theorem Torsor.subsingleton_iff (G : Type u_1) (P : Type u_2) [Group G] [Torsor G P] : Subsingleton G ↔ Subsingleton P

theorem AddTorsor.subsingleton_iff (G : Type u_1) (P : Type u_2) [AddGroup G] [AddTorsor G P] : Subsingleton G ↔ Subsingleton P