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). The variable G
is an explicit rather than implicit argument to lemmas because
otherwise the elaborator sometimes has problems inferring appropriate
types and type class instances.
References
- https://en.wikipedia.org/wiki/Principal_homogeneous_space
- https://en.wikipedia.org/wiki/Affine_space
- vadd : G → P → P
Type class for the +ᵥ notation.
Instances
- vsub : P → P → G
Type class for the -ᵥ notation.
Instances
- 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 : 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.
An add_group G is a torsor for itself.
Equations
- add_group_is_add_torsor G = {vadd := has_add.add (add_semigroup.to_has_add G), zero_vadd' := _, vadd_assoc' := _, vsub := has_sub.sub add_group_has_sub, nonempty := _, vsub_vadd' := _, vadd_vsub' := _}
Adding the zero group element to a point gives the same point.
Adding two group elements to a point produces the same result as adding their sum.
Adding two group elements to a point produces the same result in either order.
If the same group element added to two points produces equal results, those points are equal.
Adding the group element g to a point is an injective function.
If the same point added to two group elements produces equal results, those group elements are equal.
Adding a group element to the point p is an injective
function.
Adding a group element to a point, then subtracting another point, produces the same result as subtracting the points then adding the group element.
If subtracting two points produces 0, they are equal.
Subtracting two points produces 0 if and only if they are equal.
Cancellation adding the results of two subtractions.
Subtracting two points in the reverse order produces the negation of subtracting them.
Subtracting the result of adding a group element produces the same result as subtracting the points and subtracting that group element.
Cancellation subtracting the results of two subtractions.
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.
The pairwise differences of a set of points.
Equations
- vsub_set s = set.image2 has_vsub.vsub s s
vsub_set of an empty set.
vsub_set of a single point.
vsub_set of a finite set is finite.
If the same point subtracted from two points produces equal results, those points are equal.
The same point subtracted from two points produces equal results if and only if those points are equal.
Subtracting the point p is an injective function.
If subtracting two points from the same point produces equal results, those points are equal.
Subtracting two points from the same point produces equal results if and only if those points are equal.
Subtracting a point from the point p is an injective
function.
Cancellation subtracting the results of two subtractions.
Equations
- prod.add_torsor = {vadd := λ (v : G × G') (p : P × P'), (v.fst +ᵥ p.fst, v.snd +ᵥ p.snd), zero_vadd' := _, vadd_assoc' := _, vsub := λ (p₁ p₂ : P × P'), (p₁.fst -ᵥ p₂.fst, p₁.snd -ᵥ p₂.snd), nonempty := _, vsub_vadd' := _, vadd_vsub' := _}
A product of add_torsors is an add_torsor.
Equations
- pi.add_torsor = {vadd := λ (g : Π (i : I), fg i) (p : Π (i : I), fp i) (i : I), g i +ᵥ p i, zero_vadd' := _, vadd_assoc' := _, vsub := λ (p₁ p₂ : Π (i : I), fp i) (i : I), p₁ i -ᵥ p₂ i, nonempty := _, vsub_vadd' := _, vadd_vsub' := _}
Addition in a product of add_torsors.
v ↦ v +ᵥ p as an equivalence.
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 := _}
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 v.to_add, map_one' := _, map_mul' := _}