Documentation

Mathlib.Algebra.AddTorsor

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 #

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
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.

Instances

instance addGroupIsAddTorsor (G : Type u_1) [AddGroup 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₂

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₁

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} (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} (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) :

(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} (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₂ = 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 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₃

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₁

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 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) (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₂

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₁ v₂ : G} {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₁ 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} (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₂

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} (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₂

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₂

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) :

(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₁

theorem vadd_eq_vadd_iff_sub_eq_vsub {G : Type u_1} {P : Type u_2} [AddCommGroup G] [AddTorsor G 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} [AddCommGroup G] [AddTorsor G 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₂).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₂).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₂')

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 := ⋯ }

Instances For

@[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 := ⋯ }

Instances For

@[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) :

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 := ⋯ }

Instances For

@[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₁ 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 = { toFun := fun (v : Multiplicative G) => Equiv.constVAdd P (Multiplicative.toAdd v), map_one' := ⋯, map_mul' := ⋯ }

Instances For

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

Point reflection in x as a permutation.

Equations

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

Instances For

theorem Equiv.pointReflection_apply {G : Type u_1} {P : Type u_2} [AddGroup G] [AddTorsor G P] (x 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 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 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 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 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.symm (Equiv.pointReflection x) = 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_two_nsmul {G : Type u_1} {P : Type u_2} [AddGroup G] [AddTorsor G P] {x y : P} (h : Function.Injective fun (x : G) => 2 • x) :

(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.

@[deprecated Equiv.pointReflection_fixed_iff_of_injective_two_nsmul (since := "2024-11-18")]

theorem Equiv.pointReflection_fixed_iff_of_injective_bit0 {G : Type u_1} {P : Type u_2} [AddGroup G] [AddTorsor G P] {x y : P} (h : Function.Injective fun (x : G) => 2 • x) :

(Equiv.pointReflection x) y = y ↔ y = x

Alias of Equiv.pointReflection_fixed_iff_of_injective_two_nsmul.

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_two_nsmul {G : Type u_3} {P : Type u_4} [AddCommGroup G] [AddTorsor G P] (h : Function.Injective fun (x : G) => 2 • x) (y : P) :

Function.Injective fun (x : P) => (Equiv.pointReflection x) y

@[deprecated Equiv.injective_pointReflection_left_of_injective_two_nsmul (since := "2024-11-18")]

theorem Equiv.injective_pointReflection_left_of_injective_bit0 {G : Type u_3} {P : Type u_4} [AddCommGroup G] [AddTorsor G P] (h : Function.Injective fun (x : G) => 2 • x) (y : P) :

Function.Injective fun (x : P) => (Equiv.pointReflection x) y

Alias of Equiv.injective_pointReflection_left_of_injective_two_nsmul.

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

Subsingleton G ↔ Subsingleton P