class IsTorsor (G : Type u_1) (T : Type u_2) [AddCommGroup G] extends AddTorsor G T : Type (max u_1 u_2)

A G-torsor (principal homogeneous space) is a type T equipped with a free and transitive action of the additive commutative group G. This is packaged as a Mixin-style class over AddTorsor G T.

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

@[implicit_reducible]

instance IsTorsor.self (G : Type u_1) [AddCommGroup G] : IsTorsor G G

Every additive commutative group G is a torsor over itself, with action given by addition.

noncomputable def IsTorsor.equivOfBasePoint {G : Type u_1} {T : Type u_2} [AddCommGroup G] [IsTorsor G T] (t₀ : T) : G ≃ T

Choosing a base point $t_0 \in T$ of a $G$-torsor $T$ yields an equivalence $G \simeq T$ sending $g \mapsto g +_v t_0$.