# Torsors of additive group actions

This file defines torsors of additive group actions.

## Notations

The group elements are referred to as acting on points. This file defines the notation +ᵥ for adding a group element to a point and -ᵥ for subtracting two points to produce a group element.

## Implementation notes

Affine spaces are the motivating example of torsors of additive group actions. It may be appropriate to refactor in terms of the general definition of group actions, via to_additive, when there is a use for multiplicative torsors (currently mathlib only develops the theory of group actions for multiplicative group actions).

## Notations

• v +ᵥ p is a notation for has_vadd.vadd, the left action of an additive monoid;

• p₁ -ᵥ p₂ is a notation for has_vsub.vsub, difference between two points in an additive torsor as an element of the corresponding additive group;

## References

• https://en.wikipedia.org/wiki/Principal_homogeneous_space
• https://en.wikipedia.org/wiki/Affine_space
@[class]
Type u_1Type u_2Type (max u_1 u_2)
• vadd : G → P → P

Type class for the +ᵥ notation.

Instances
@[class]
structure has_vsub  :
out_param (Type u_1)Type u_2Type (max u_1 u_2)
• vsub : P → P → G

Type class for the -ᵥ notation.

Instances
@[class]
structure add_action (G : Type u_1) (P : Type u_2) [add_monoid G] :
Type (max u_1 u_2)
• vadd : G → P → P
• zero_vadd' : ∀ (p : P), 0 +ᵥ p = p
• vadd_assoc' : ∀ (g1 g2 : G) (p : P), g1 +ᵥ (g2 +ᵥ p) = g1 + g2 +ᵥ p

Type class for additive monoid actions.

Instances
@[instance]
P

@[class]
structure add_torsor (G : out_param (Type u_1)) (P : Type u_2) [out_param (add_group G)] :
Type (max u_1 u_2)
• vadd : G → P → P
• zero_vadd' : ∀ (p : P), 0 +ᵥ p = p
• vadd_assoc' : ∀ (g1 g2 : G) (p : P), g1 +ᵥ (g2 +ᵥ p) = g1 + g2 +ᵥ p
• vsub : P → P → G
• nonempty :
• vsub_vadd' : ∀ (p1 p2 : P), p1 -ᵥ p2 +ᵥ p2 = p1
• vadd_vsub' : ∀ (g : G) (p : P), g +ᵥ p -ᵥ p = g

An add_torsor G P gives a structure to the nonempty type P, acted on by an add_group 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.

Instances
@[instance]
def add_torsor.to_has_vsub (G : out_param (Type u_1)) (P : Type u_2) [out_param (add_group G)] [s : P] :
P

@[instance]
def add_torsor.to_add_action (G : out_param (Type u_1)) (P : Type u_2) [out_param (add_group G)] [s : P] :
P

@[nolint, instance]
G

An add_group G is a torsor for itself.

Equations
@[simp]
g1 +ᵥ g2 = g1 + g2

Simplify addition for a torsor for an add_group G over itself.

@[simp]
theorem vsub_eq_sub {G : Type u_1} [add_group G] (g1 g2 : G) :
g1 -ᵥ g2 = g1 - g2

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

@[simp]
theorem zero_vadd (G : Type u_1) {P : Type u_2} [add_monoid G] [A : P] (p : P) :
0 +ᵥ p = p

Adding the zero group element to a point gives the same point.

theorem vadd_assoc {G : Type u_1} {P : Type u_2} [add_monoid G] [A : P] (g1 g2 : G) (p : P) :
g1 +ᵥ (g2 +ᵥ p) = g1 + g2 +ᵥ p

Adding two group elements to a point produces the same result as adding their sum.

theorem vadd_comm (G : Type u_1) {P : Type u_2} [A : P] (p : P) (g1 g2 : G) :
g1 +ᵥ (g2 +ᵥ p) = g2 +ᵥ (g1 +ᵥ p)

Adding two group elements to a point produces the same result in either order.

theorem vadd_left_cancel {G : Type u_1} {P : Type u_2} [add_group G] [A : P] {p1 p2 : P} (g : G) :
g +ᵥ p1 = g +ᵥ p2p1 = p2

If the same group element added to two points produces equal results, those points are equal.

@[simp]
theorem vadd_left_cancel_iff {G : Type u_1} {P : Type u_2} [add_group G] [A : P] {p₁ p₂ : P} (g : G) :
g +ᵥ p₁ = g +ᵥ p₂ p₁ = p₂

theorem vadd_left_injective {G : Type u_1} (P : Type u_2) [add_group G] [A : P] (g : G) :

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

@[simp]
theorem vsub_vadd {G : Type u_1} {P : Type u_2} [add_group G] [T : P] (p1 p2 : P) :
p1 -ᵥ p2 +ᵥ p2 = p1

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

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

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

theorem vadd_right_cancel {G : Type u_1} {P : Type u_2} [add_group G] [T : P] {g1 g2 : G} (p : P) :
g1 +ᵥ p = g2 +ᵥ pg1 = g2

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

@[simp]
theorem vadd_right_cancel_iff {G : Type u_1} {P : Type u_2} [add_group G] [T : P] {g1 g2 : G} (p : P) :
g1 +ᵥ p = g2 +ᵥ p g1 = g2

theorem vadd_right_injective {G : Type u_1} {P : Type u_2} [add_group G] [T : P] (p : P) :
function.injective (λ (_x : G), _x +ᵥ p)

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

theorem vadd_vsub_assoc {G : Type u_1} {P : Type u_2} [add_group G] [T : P] (g : G) (p1 p2 : P) :
g +ᵥ p1 -ᵥ p2 = g + (p1 -ᵥ p2)

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 vsub_self {G : Type u_1} {P : Type u_2} [add_group G] [T : P] (p : P) :
p -ᵥ p = 0

Subtracting a point from itself produces 0.

theorem eq_of_vsub_eq_zero {G : Type u_1} {P : Type u_2} [add_group G] [T : P] {p1 p2 : P} :
p1 -ᵥ p2 = 0p1 = p2

If subtracting two points produces 0, they are equal.

@[simp]
theorem vsub_eq_zero_iff_eq {G : Type u_1} {P : Type u_2} [add_group G] [T : P] {p1 p2 : P} :
p1 -ᵥ p2 = 0 p1 = p2

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

@[simp]
theorem vsub_add_vsub_cancel {G : Type u_1} {P : Type u_2} [add_group G] [T : P] (p1 p2 p3 : P) :
p1 -ᵥ p2 + (p2 -ᵥ p3) = p1 -ᵥ p3

Cancellation adding the results of two subtractions.

@[simp]
theorem neg_vsub_eq_vsub_rev {G : Type u_1} {P : Type u_2} [add_group G] [T : P] (p1 p2 : P) :
-(p1 -ᵥ p2) = p2 -ᵥ p1

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

theorem vsub_vadd_eq_vsub_sub {G : Type u_1} {P : Type u_2} [add_group G] [T : P] (p1 p2 : P) (g : G) :
p1 -ᵥ (g +ᵥ p2) = p1 -ᵥ p2 - g

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

@[simp]
theorem vsub_sub_vsub_cancel_right {G : Type u_1} {P : Type u_2} [add_group G] [T : P] (p1 p2 p3 : P) :
p1 -ᵥ p3 - (p2 -ᵥ p3) = p1 -ᵥ p2

Cancellation subtracting the results of two subtractions.

theorem eq_vadd_iff_vsub_eq {G : Type u_1} {P : Type u_2} [add_group G] [T : P] (p1 : P) (g : G) (p2 : P) :
p1 = g +ᵥ p2 p1 -ᵥ p2 = 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 vadd_eq_vadd_iff_neg_add_eq_vsub {G : Type u_1} {P : Type u_2} [add_group G] [T : P] {v₁ v₂ : G} {p₁ p₂ : P} :
v₁ +ᵥ p₁ = v₂ +ᵥ p₂ -v₁ + v₂ = p₁ -ᵥ p₂

@[instance]
def set.has_vsub {G : Type u_1} {P : Type u_2} [add_group G] [T : P] :
has_vsub (set G) (set P)

Equations
@[simp]
theorem set.vsub_empty {G : Type u_1} {P : Type u_2} [add_group G] [T : P] (s : set P) :

@[simp]
theorem set.empty_vsub {G : Type u_1} {P : Type u_2} [add_group G] [T : P] (s : set P) :

@[simp]
theorem set.singleton_vsub {G : Type u_1} {P : Type u_2} [add_group G] [T : P] (s : set P) (p : P) :
{p} -ᵥ s =

@[simp]
theorem set.vsub_singleton {G : Type u_1} {P : Type u_2} [add_group G] [T : P] (s : set P) (p : P) :
s -ᵥ {p} = (λ (_x : P), _x -ᵥ p) '' s

@[simp]
theorem set.singleton_vsub_self {G : Type u_1} {P : Type u_2} [add_group G] [T : P] (p : P) :
{p} -ᵥ {p} = {0}

theorem set.finite.vsub {G : Type u_1} {P : Type u_2} [add_group G] [T : P] {s t : set P} :
s.finitet.finite(s -ᵥ t).finite

vsub of a finite set is finite.

theorem set.vsub_mem_vsub {G : Type u_1} {P : Type u_2} [add_group G] [T : P] {s t : set P} {ps pt : P} :
ps spt tps -ᵥ pt s -ᵥ t

Each pairwise difference is in the vsub set.

theorem set.vsub_subset_vsub {G : Type u_1} {P : Type u_2} [add_group G] [T : P] {s t s' t' : set P} :
s s't t's -ᵥ t s' -ᵥ t'

s -ᵥ t is monotone in both arguments.

theorem set.vsub_self_mono {G : Type u_1} {P : Type u_2} [add_group G] [T : P] {s t : set P} :
s ts -ᵥ s t -ᵥ t

theorem set.vsub_subset_iff {G : Type u_1} {P : Type u_2} [add_group G] [T : P] {s t : set P} {u : set G} :
s -ᵥ t u ∀ (x : P), x s∀ (y : P), y tx -ᵥ y u

@[instance]
def set.add_action {G : Type u_1} {P : Type u_2} [add_group G] [T : P] :

Equations
theorem set.vadd_subset_vadd {G : Type u_1} {P : Type u_2} [add_group G] [T : P] {s s' : set G} {t t' : set P} :
s s't t's +ᵥ t s' +ᵥ t'

@[simp]
theorem set.vadd_singleton {G : Type u_1} {P : Type u_2} [add_group G] [T : P] (s : set G) (p : P) :
s +ᵥ {p} = (λ (_x : G), _x +ᵥ p) '' s

@[simp]
theorem set.singleton_vadd {G : Type u_1} {P : Type u_2} [add_group G] [T : P] (v : G) (s : set P) :
{v} +ᵥ s =

theorem set.finite.vadd {G : Type u_1} {P : Type u_2} [add_group G] [T : P] {s : set G} {t : set P} :
s.finitet.finite(s +ᵥ t).finite

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

theorem vsub_left_cancel {G : Type u_1} {P : Type u_2} [add_group G] [T : P] {p1 p2 p : P} :
p1 -ᵥ p = p2 -ᵥ pp1 = p2

If the same point subtracted from two points produces equal results, those points are equal.

@[simp]
theorem vsub_left_cancel_iff {G : Type u_1} {P : Type u_2} [add_group G] [T : P] {p1 p2 p : P} :
p1 -ᵥ p = p2 -ᵥ p p1 = p2

The same point subtracted from two points produces equal results if and only if those points are equal.

theorem vsub_left_injective {G : Type u_1} {P : Type u_2} [add_group G] [T : P] (p : P) :
function.injective (λ (_x : P), _x -ᵥ p)

Subtracting the point p is an injective function.

theorem vsub_right_cancel {G : Type u_1} {P : Type u_2} [add_group G] [T : P] {p1 p2 p : P} :
p -ᵥ p1 = p -ᵥ p2p1 = p2

If subtracting two points from the same point produces equal results, those points are equal.

@[simp]
theorem vsub_right_cancel_iff {G : Type u_1} {P : Type u_2} [add_group G] [T : P] {p1 p2 p : P} :
p -ᵥ p1 = p -ᵥ p2 p1 = p2

Subtracting two points from the same point produces equal results if and only if those points are equal.

theorem vsub_right_injective {G : Type u_1} {P : Type u_2} [add_group G] [T : P] (p : P) :

Subtracting a point from the point p is an injective function.

@[simp]
theorem vsub_sub_vsub_cancel_left {G : Type u_1} {P : Type u_2} [ P] (p1 p2 p3 : P) :
p3 -ᵥ p2 - (p3 -ᵥ p1) = p1 -ᵥ p2

Cancellation subtracting the results of two subtractions.

@[simp]
theorem vadd_vsub_vadd_cancel_left {G : Type u_1} {P : Type u_2} [ P] (v : G) (p1 p2 : P) :
v +ᵥ p1 -ᵥ (v +ᵥ p2) = p1 -ᵥ p2

theorem vsub_vadd_comm {G : Type u_1} {P : Type u_2} [ P] (p1 p2 p3 : P) :
p1 -ᵥ p2 +ᵥ p3 = p3 -ᵥ p2 +ᵥ p1

theorem vadd_eq_vadd_iff_sub_eq_vsub {G : Type u_1} {P : Type u_2} [ P] {v₁ v₂ : G} {p₁ p₂ : P} :
v₁ +ᵥ p₁ = v₂ +ᵥ p₂ v₂ - v₁ = p₁ -ᵥ p₂

theorem vsub_sub_vsub_comm {G : Type u_1} {P : Type u_2} [ P] (p₁ p₂ p₃ p₄ : P) :
p₁ -ᵥ p₂ - (p₃ -ᵥ p₄) = p₁ -ᵥ p₃ - (p₂ -ᵥ p₄)

@[instance]
def prod.add_torsor {G : Type u_1} {P : Type u_2} {G' : Type u_3} {P' : Type u_4} [add_group G] [add_group G'] [ P] [ P'] :
affine_space (G × G') (P × P')

Equations
@[simp]
theorem prod.fst_vadd {G : Type u_1} {P : Type u_2} {G' : Type u_3} {P' : Type u_4} [add_group G] [add_group G'] [ P] [ P'] (v : G × G') (p : P × P') :
(v +ᵥ p).fst = v.fst +ᵥ p.fst

@[simp]
theorem prod.snd_vadd {G : Type u_1} {P : Type u_2} {G' : Type u_3} {P' : Type u_4} [add_group G] [add_group G'] [ P] [ P'] (v : G × G') (p : P × P') :
(v +ᵥ p).snd = v.snd +ᵥ p.snd

@[simp]
theorem prod.mk_vadd_mk {G : Type u_1} {P : Type u_2} {G' : Type u_3} {P' : Type u_4} [add_group G] [add_group G'] [ P] [ P'] (v : G) (v' : G') (p : P) (p' : P') :
(v, v') +ᵥ (p, p') = (v +ᵥ p, v' +ᵥ p')

@[simp]
theorem prod.fst_vsub {G : Type u_1} {P : Type u_2} {G' : Type u_3} {P' : Type u_4} [add_group G] [add_group G'] [ P] [ P'] (p₁ p₂ : P × P') :
(p₁ -ᵥ p₂).fst = p₁.fst -ᵥ p₂.fst

@[simp]
theorem prod.snd_vsub {G : Type u_1} {P : Type u_2} {G' : Type u_3} {P' : Type u_4} [add_group G] [add_group G'] [ P] [ P'] (p₁ p₂ : P × P') :
(p₁ -ᵥ p₂).snd = p₁.snd -ᵥ p₂.snd

@[simp]
theorem prod.mk_vsub_mk {G : Type u_1} {P : Type u_2} {G' : Type u_3} {P' : Type u_4} [add_group G] [add_group G'] [ P] [ P'] (p₁ p₂ : P) (p₁' p₂' : P') :
(p₁, p₁') -ᵥ (p₂, p₂') = (p₁ -ᵥ p₂, p₁' -ᵥ p₂')

@[instance]
def pi.add_torsor {I : Type u} {fg : I → Type v} [Π (i : I), add_group (fg i)] {fp : I → Type w} [T : Π (i : I), affine_space (fg i) (fp i)] :
affine_space (Π (i : I), fg i) (Π (i : I), fp i)

A product of add_torsors is an add_torsor.

Equations
@[simp]
theorem pi.vadd_apply {I : Type u} {fg : I → Type v} [Π (i : I), add_group (fg i)] {fp : I → Type w} [T : Π (i : I), affine_space (fg i) (fp i)] (x : Π (i : I), fg i) (y : Π (i : I), fp i) {i : I} :
(x +ᵥ y) i = x i +ᵥ y i

Addition in a product of add_torsors.

def equiv.vadd_const {G : Type u_1} {P : Type u_2} [add_group G] [ P] :
P → G P

v ↦ v +ᵥ p as an equivalence.

Equations
@[simp]
theorem equiv.coe_vadd_const {G : Type u_1} {P : Type u_2} [add_group G] [ P] (p : P) :
= λ (v : G), v +ᵥ p

@[simp]
theorem equiv.coe_vadd_const_symm {G : Type u_1} {P : Type u_2} [add_group G] [ P] (p : P) :
((equiv.vadd_const p).symm) = λ (p' : P), p' -ᵥ p

def equiv.const_vsub {G : Type u_1} {P : Type u_2} [add_group G] [ P] :
P → P G

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

Equations
@[simp]
theorem equiv.coe_const_vsub {G : Type u_1} {P : Type u_2} [add_group G] [ P] (p : P) :

@[simp]
theorem equiv.coe_const_vsub_symm {G : Type u_1} {P : Type u_2} [add_group G] [ P] (p : P) :
((equiv.const_vsub p).symm) = λ (v : G), -v +ᵥ p

def equiv.const_vadd {G : Type u_1} (P : Type u_2) [add_group G] [ P] :
G →

The permutation given by p ↦ v +ᵥ p.

Equations
@[simp]
theorem equiv.coe_const_vadd {G : Type u_1} (P : Type u_2) [add_group G] [ P] (v : G) :
v) =

@[simp]
theorem equiv.const_vadd_zero (G : Type u_1) (P : Type u_2) [add_group G] [ P] :
= 1

@[simp]
theorem equiv.const_vadd_add {G : Type u_1} (P : Type u_2) [add_group G] [ P] (v₁ v₂ : G) :
(v₁ + v₂) = v₁) * v₂

def equiv.const_vadd_hom {G : Type u_1} (P : Type u_2) [add_group G] [ P] :

equiv.const_vadd as a homomorphism from multiplicative G to equiv.perm P

Equations
def equiv.point_reflection {G : Type u_1} {P : Type u_2} [add_group G] [ P] :
P →

Point reflection in x as a permutation.

Equations
theorem equiv.point_reflection_apply {G : Type u_1} {P : Type u_2} [add_group G] [ P] (x y : P) :
= x -ᵥ y +ᵥ x

@[simp]
theorem equiv.point_reflection_symm {G : Type u_1} {P : Type u_2} [add_group G] [ P] (x : P) :

@[simp]
theorem equiv.point_reflection_self {G : Type u_1} {P : Type u_2} [add_group G] [ P] (x : P) :
= x

theorem equiv.point_reflection_involutive {G : Type u_1} {P : Type u_2} [add_group G] [ P] (x : P) :

theorem equiv.point_reflection_fixed_iff_of_injective_bit0 {G : Type u_1} {P : Type u_2} [add_group G] [ P] {x y : P} :
y = y y = x)

x is the only fixed point of point_reflection x. This lemma requires x + x = y + y ↔ x = y. There is no typeclass to use here, so we add it as an explicit argument.

theorem equiv.injective_point_reflection_left_of_injective_bit0 {G : Type u_1} {P : Type u_2} [ P] (y : P) :
function.injective (λ (x : P), y)