Torsors of additive group actions #
This file defines torsors of additive group actions.
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).
v +ᵥ pis 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;
- 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
add_torsor G P gives a structure to the nonempty type
acted on by an
add_group G with a transitive and free action given
+ᵥ operation and a corresponding subtraction given by the
-ᵥ operation. In the case of a vector space, it is an affine
add_group G is a torsor for itself.
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.