scilib documentation

algebra.add_torsor

Torsors of additive group actions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

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

to_add_action : add_action G P
to_has_vsub : has_vsub G P
nonempty : nonempty P
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 of this typeclass

Instances of other typeclasses for add_torsor

add_torsor.has_sizeof_inst

@[protected, nolint, instance]

def add_group_is_add_torsor (G : Type u_1) [add_group G] :

An add_group G is a torsor for itself.

Equations

add_group_is_add_torsor G = {to_add_action := add_monoid.to_add_action G (sub_neg_monoid.to_add_monoid G), to_has_vsub := {vsub := has_sub.sub (sub_neg_monoid.to_has_sub G)}, nonempty := _, vsub_vadd' := _, vadd_vsub' := _}

@[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 vsub_vadd {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G 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 : add_torsor 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} [add_group G] [T : add_torsor G P] {g1 g2 : G} (p : P) (h : g1 +ᵥ p = g2 +ᵥ p) :

g1 = 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 : add_torsor G 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 : add_torsor G 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 : add_torsor G 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 : add_torsor 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} [add_group G] [T : add_torsor G P] {p1 p2 : P} (h : p1 -ᵥ p2 = 0) :

p1 = 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 : add_torsor G P] {p1 p2 : P} :

p1 -ᵥ p2 = 0 ↔ p1 = p2

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

theorem vsub_ne_zero {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G P] {p q : P} :

p -ᵥ q ≠ 0 ↔ p ≠ q

@[simp]

theorem vsub_add_vsub_cancel {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G 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 : add_torsor G P] (p1 p2 : P) :

-(p1 -ᵥ p2) = p2 -ᵥ p1

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} [add_group G] [T : add_torsor 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} [add_group G] [T : add_torsor G 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 : add_torsor G 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 : add_torsor G 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 : add_torsor G P] {v₁ v₂ : G} {p₁ p₂ : P} :

v₁ +ᵥ p₁ = v₂ +ᵥ p₂ ↔ -v₁ + v₂ = p₁ -ᵥ p₂

@[simp]

theorem set.singleton_vsub_self {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G P] (p : P) :

{p} -ᵥ {p} = {0}

@[simp]

theorem vadd_vsub_vadd_cancel_right {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor 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} [add_group G] [T : add_torsor G P] {p1 p2 p : P} (h : p1 -ᵥ p = p2 -ᵥ p) :

p1 = 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 : add_torsor G 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 : add_torsor G 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 : add_torsor G P] {p1 p2 p : P} (h : p -ᵥ p1 = p -ᵥ p2) :

p1 = 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 : add_torsor G 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 : add_torsor G P] (p : P) :

function.injective (has_vsub.vsub 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} [add_comm_group G] [add_torsor G 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} [add_comm_group G] [add_torsor G P] (v : G) (p1 p2 : P) :

v +ᵥ p1 -ᵥ (v +ᵥ p2) = p1 -ᵥ p2

theorem vsub_vadd_comm {G : Type u_1} {P : Type u_2} [add_comm_group G] [add_torsor G 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} [add_comm_group G] [add_torsor 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} [add_comm_group G] [add_torsor G P] (p₁ p₂ p₃ p₄ : P) :

p₁ -ᵥ p₂ - (p₃ -ᵥ p₄) = p₁ -ᵥ p₃ - (p₂ -ᵥ p₄)

@[protected, 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'] [add_torsor G P] [add_torsor G' P'] :

add_torsor (G × G') (P × P')

Equations

prod.add_torsor = {to_add_action := {to_has_vadd := {vadd := λ (v : G × G') (p : P × P'), (v.fst +ᵥ p.fst, v.snd +ᵥ p.snd)}, zero_vadd := _, add_vadd := _}, to_has_vsub := {vsub := λ (p₁ p₂ : P × P'), (p₁.fst -ᵥ p₂.fst, p₁.snd -ᵥ p₂.snd)}, nonempty := _, vsub_vadd' := _, vadd_vsub' := _}

@[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'] [add_torsor G P] [add_torsor G' 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'] [add_torsor G P] [add_torsor G' 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'] [add_torsor G P] [add_torsor 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} {P : Type u_2} {G' : Type u_3} {P' : Type u_4} [add_group G] [add_group G'] [add_torsor G P] [add_torsor G' 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'] [add_torsor G P] [add_torsor G' 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'] [add_torsor G P] [add_torsor G' P'] (p₁ p₂ : P) (p₁' p₂' : P') :

(p₁, p₁') -ᵥ (p₂, p₂') = (p₁ -ᵥ p₂, p₁' -ᵥ p₂')

@[protected, 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), add_torsor (fg i) (fp i)] :

add_torsor (Π (i : I), fg i) (Π (i : I), fp i)

A product of add_torsors is an add_torsor.

Equations

pi.add_torsor = {to_add_action := {to_has_vadd := {vadd := λ (g : Π (i : I), fg i) (p : Π (i : I), fp i) (i : I), g i +ᵥ p i}, zero_vadd := _, add_vadd := _}, to_has_vsub := {vsub := λ (p₁ p₂ : Π (i : I), fp i) (i : I), p₁ i -ᵥ p₂ i}, nonempty := _, vsub_vadd' := _, vadd_vsub' := _}

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

G ≃ P

v ↦ v +ᵥ p as an equivalence.

Equations

equiv.vadd_const p = {to_fun := λ (v : G), v +ᵥ p, inv_fun := λ (p' : P), p' -ᵥ p, left_inv := _, right_inv := _}

@[simp]

theorem equiv.coe_vadd_const {G : Type u_1} {P : Type u_2} [add_group G] [add_torsor G P] (p : P) :

⇑(equiv.vadd_const p) = λ (v : G), v +ᵥ p

@[simp]

theorem equiv.coe_vadd_const_symm {G : Type u_1} {P : Type u_2} [add_group G] [add_torsor 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] [add_torsor G P] (p : P) :

P ≃ G

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

Equations

equiv.const_vsub p = {to_fun := has_vsub.vsub p, inv_fun := λ (v : G), -v +ᵥ p, left_inv := _, right_inv := _}

@[simp]

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

⇑(equiv.const_vsub p) = has_vsub.vsub p

@[simp]

theorem equiv.coe_const_vsub_symm {G : Type u_1} {P : Type u_2} [add_group G] [add_torsor 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] [add_torsor G P] (v : G) :

The permutation given by p ↦ v +ᵥ p.

Equations

equiv.const_vadd P v = {to_fun := has_vadd.vadd v, inv_fun := has_vadd.vadd (-v), left_inv := _, right_inv := _}

@[simp]

theorem equiv.coe_const_vadd {G : Type u_1} (P : Type u_2) [add_group G] [add_torsor G P] (v : G) :

⇑(equiv.const_vadd P v) = has_vadd.vadd v

@[simp]

theorem equiv.const_vadd_zero (G : Type u_1) (P : Type u_2) [add_group G] [add_torsor G P] :

equiv.const_vadd P 0 = 1

@[simp]

theorem equiv.const_vadd_add {G : Type u_1} (P : Type u_2) [add_group G] [add_torsor G P] (v₁ v₂ : G) :

equiv.const_vadd P (v₁ + v₂) = equiv.const_vadd P v₁ * equiv.const_vadd P v₂

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

multiplicative G →* equiv.perm P

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

Equations

equiv.const_vadd_hom P = {to_fun := λ (v : multiplicative G), equiv.const_vadd P (⇑multiplicative.to_add v), map_one' := _, map_mul' := _}

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

Point reflection in x as a permutation.

Equations

equiv.point_reflection x = (equiv.const_vsub x).trans (equiv.vadd_const x)

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

⇑(equiv.point_reflection x) y = x -ᵥ y +ᵥ x

@[simp]

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

equiv.symm (equiv.point_reflection x) = equiv.point_reflection x

@[simp]

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

⇑(equiv.point_reflection x) x = x

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

function.involutive ⇑(equiv.point_reflection x)

theorem equiv.point_reflection_fixed_iff_of_injective_bit0 {G : Type u_1} {P : Type u_2} [add_group G] [add_torsor G P] {x y : P} (h : function.injective bit0) :

⇑(equiv.point_reflection x) 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} [add_comm_group G] [add_torsor G P] (h : function.injective bit0) (y : P) :

function.injective (λ (x : P), ⇑(equiv.point_reflection x) y)

theorem add_torsor.subsingleton_iff (G : Type u_1) (P : Type u_2) [add_group G] [add_torsor G P] :

subsingleton G ↔ subsingleton P