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 VAdd.vadd, the left action of an additive monoid;

• p₁ -ᵥ p₂ is a notation for 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 AddTorsor (G : outParam (Type u_1)) (P : Type u_2) [outParam (AddGroup G)] extends AddAction , VSub : 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
• zero_vadd : ∀ (p : P), 0 +ᵥ p = p
• add_vadd : ∀ (g₁ g₂ : G) (p : P), g₁ + g₂ +ᵥ p = g₁ +ᵥ (g₂ +ᵥ 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.

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

An AddGroup G is a torsor for itself.

Equations

• addGroupIsAddTorsor G = AddTorsor.mk ⋯ ⋯

@[simp]

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

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

@[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₂ = p₁

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

@[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 vadd_right_cancel {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] {g₁ : 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 vadd_right_cancel_iff {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] {g₁ : G} {g₂ : G} (p : P) : g₁ +ᵥ p = g₂ +ᵥ p ↔ g₁ = g₂

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 vadd_vsub_assoc {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] (g : G) (p₁ : 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 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_vsub_eq_zero {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] {p₁ : P} {p₂ : P} (h : p₁ -ᵥ p₂ = 0) : p₁ = p₂

If subtracting two points produces 0, 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₁ -ᵥ p₂ = 0 ↔ p₁ = p₂

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

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

@[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₃) = p₁ -ᵥ p₃

Cancellation adding the results of two subtractions.

@[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₂ -ᵥ p₁

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

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

theorem vsub_vadd_eq_vsub_sub {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] (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 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₃) = p₁ -ᵥ p₂

Cancellation subtracting the results of two subtractions.

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 vadd_eq_vadd_iff_neg_add_eq_vsub {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] {v₁ : G} {v₂ : G} {p₁ : P} {p₂ : P} : v₁ +ᵥ p₁ = v₂ +ᵥ p₂ ↔ -v₁ + v₂ = p₁ -ᵥ p₂

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

@[simp]

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

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

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} [AddGroup G] [T : AddTorsor G P] {p₁ : P} {p₂ : P} {p : P} : p₁ -ᵥ p = p₂ -ᵥ p ↔ p₁ = p₂

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} [AddGroup G] [T : AddTorsor G P] (p : P) : Function.Injective fun (x : P) => x -ᵥ p

Subtracting the point p is an injective function.

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

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} [AddGroup G] [T : AddTorsor G P] {p₁ : P} {p₂ : P} {p : P} : p -ᵥ p₁ = p -ᵥ p₂ ↔ p₁ = p₂

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} [AddGroup G] [T : AddTorsor G P] (p : P) : Function.Injective fun (x : P) => p -ᵥ x

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} [AddCommGroup G] [AddTorsor G P] (p₁ : P) (p₂ : P) (p₃ : P) : p₃ -ᵥ p₂ - (p₃ -ᵥ p₁) = p₁ -ᵥ p₂

Cancellation subtracting the results of two subtractions.

@[simp]

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

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

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

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

instance Prod.instAddTorsor {G : Type u_1} {G' : Type u_2} {P : Type u_3} {P' : Type u_4} [AddGroup G] [AddGroup G'] [AddTorsor G P] [AddTorsor G' P'] : AddTorsor (G × G') (P × P')

Equations

• Prod.instAddTorsor = AddTorsor.mk ⋯ ⋯

@[simp]

theorem Prod.fst_vadd {G : Type u_1} {G' : Type u_2} {P : Type u_3} {P' : Type u_4} [AddGroup G] [AddGroup G'] [AddTorsor G P] [AddTorsor G' P'] (v : G × G') (p : P × P') : (v +ᵥ p).1 = v.1 +ᵥ p.1

@[simp]

theorem Prod.snd_vadd {G : Type u_1} {G' : Type u_2} {P : Type u_3} {P' : Type u_4} [AddGroup G] [AddGroup G'] [AddTorsor G P] [AddTorsor G' P'] (v : G × G') (p : P × P') : (v +ᵥ p).2 = v.2 +ᵥ p.2

@[simp]

theorem Prod.mk_vadd_mk {G : Type u_1} {G' : Type u_2} {P : Type u_3} {P' : Type u_4} [AddGroup G] [AddGroup G'] [AddTorsor G P] [AddTorsor G' 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} {G' : Type u_2} {P : Type u_3} {P' : Type u_4} [AddGroup G] [AddGroup G'] [AddTorsor G P] [AddTorsor G' P'] (p₁ : P × P') (p₂ : P × P') : (p₁ -ᵥ p₂).1 = p₁.1 -ᵥ p₂.1

@[simp]

theorem Prod.snd_vsub {G : Type u_1} {G' : Type u_2} {P : Type u_3} {P' : Type u_4} [AddGroup G] [AddGroup G'] [AddTorsor G P] [AddTorsor G' P'] (p₁ : P × P') (p₂ : P × P') : (p₁ -ᵥ p₂).2 = p₁.2 -ᵥ p₂.2

@[simp]

theorem Prod.mk_vsub_mk {G : Type u_1} {G' : Type u_2} {P : Type u_3} {P' : Type u_4} [AddGroup G] [AddGroup G'] [AddTorsor G P] [AddTorsor G' P'] (p₁ : P) (p₂ : P) (p₁' : P') (p₂' : P') : (p₁, p₁') -ᵥ (p₂, p₂') = (p₁ -ᵥ p₂, p₁' -ᵥ p₂')

instance Pi.instAddTorsor {I : Type u} {fg : I → Type v} [(i : I) → AddGroup (fg i)] {fp : I → Type w} [(i : I) → AddTorsor (fg i) (fp i)] : AddTorsor ((i : I) → fg i) ((i : I) → fp i)

A product of AddTorsors is an AddTorsor.

Equations

• Pi.instAddTorsor = AddTorsor.mk ⋯ ⋯

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_vaddConst {G : Type u_1} {P : Type u_2} [AddGroup G] [AddTorsor G P] (p : P) : ⇑(Equiv.vaddConst p) = fun (v : G) => v +ᵥ p

@[simp]

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

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_constVSub {G : Type u_1} {P : Type u_2} [AddGroup G] [AddTorsor G P] (p : P) : ⇑(Equiv.constVSub p) = fun (x : P) => p -ᵥ x

@[simp]

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

def Equiv.constVAdd {G : Type u_1} (P : Type u_2) [AddGroup G] [AddTorsor G P] (v : G) : Equiv.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_constVAdd {G : Type u_1} (P : Type u_2) [AddGroup G] [AddTorsor G P] (v : G) : ⇑(Equiv.constVAdd P v) = fun (x : P) => v +ᵥ x

@[simp]

theorem Equiv.constVAdd_zero (G : Type u_1) (P : Type u_2) [AddGroup G] [AddTorsor G P] : Equiv.constVAdd P 0 = 1

@[simp]

theorem Equiv.constVAdd_add {G : Type u_1} (P : Type u_2) [AddGroup G] [AddTorsor G P] (v₁ : G) (v₂ : G) : Equiv.constVAdd P (v₁ + v₂) = Equiv.constVAdd P v₁ * Equiv.constVAdd P v₂

def Equiv.constVAddHom {G : Type u_1} (P : Type u_2) [AddGroup G] [AddTorsor G P] : Multiplicative G →* Equiv.Perm P

Equiv.constVAdd as a homomorphism from Multiplicative G to Equiv.perm P

Equations

• Equiv.constVAddHom P = { toOneHom := { toFun := fun (v : Multiplicative G) => Equiv.constVAdd P (Multiplicative.toAdd v), map_one' := ⋯ }, map_mul' := ⋯ }

def Equiv.pointReflection {G : Type u_1} {P : Type u_2} [AddGroup G] [AddTorsor G P] (x : P) : Equiv.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_1} {P : Type u_2} [AddGroup G] [AddTorsor G P] (x : P) (y : P) : (Equiv.pointReflection x) y = x -ᵥ y +ᵥ x

@[simp]

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

@[simp]

theorem Equiv.left_vsub_pointReflection {G : Type u_1} {P : Type u_2} [AddGroup G] [AddTorsor G P] (x : P) (y : P) : x -ᵥ (Equiv.pointReflection x) y = y -ᵥ x

@[simp]

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

@[simp]

theorem Equiv.right_vsub_pointReflection {G : Type u_1} {P : Type u_2} [AddGroup G] [AddTorsor G P] (x : P) (y : P) : y -ᵥ (Equiv.pointReflection x) y = 2 • (y -ᵥ x)

@[simp]

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

@[simp]

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

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

theorem Equiv.pointReflection_fixed_iff_of_injective_bit0 {G : Type u_1} {P : Type u_2} [AddGroup G] [AddTorsor G P] {x : P} {y : P} (h : Function.Injective bit0) : (Equiv.pointReflection x) y = y ↔ y = x

x is the only fixed point of pointReflection 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_pointReflection_left_of_injective_bit0 {G : Type u_3} {P : Type u_4} [AddCommGroup G] [AddTorsor G P] (h : Function.Injective bit0) (y : P) : Function.Injective fun (x : P) => (Equiv.pointReflection x) y

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