Mathlib.Algebra.AddTorsor.Defs

AddTorsor structure

(G : outParam Type*) (P : Type*) [AddGroup G] extends AddAction G P,
  VSub G P

Full source

/-- 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. -/
class AddTorsor (G : outParam Type*) (P : Type*) [AddGroup G] extends AddAction G P,
  VSub G P where
  [nonempty : Nonempty P]
  /-- Torsor subtraction and addition with the same element cancels out. -/
  vsub_vadd' : ∀ p₁ p₂ : P, (p₁ -ᵥ p₂ : G) +ᵥ p₂ = p₁
  /-- Torsor addition and subtraction with the same element cancels out. -/
  vadd_vsub' : ∀ (g : G) (p : P), (g +ᵥ p) -ᵥ p = g

Additive Torsor

Informal description

An `AddTorsor G P` is a structure on a nonempty type `P` acted upon by an additive group `G`, where the action is transitive and free. The action is given by the operation `+ᵥ` (adding a group element to a point), and there is a corresponding subtraction operation `-ᵥ` that yields the difference between two points as an element of `G`. In the case where `P` is a vector space, this structure corresponds to an affine space.

addGroupIsAddTorsor instance

(G : Type*) [AddGroup G] : AddTorsor G G

Full source

/-- An `AddGroup G` is a torsor for itself. -/
-- Porting note (https://github.com/leanprover-community/mathlib4/issues/12096): linter not ported yet
--@[nolint instance_priority]
instance addGroupIsAddTorsor (G : Type*) [AddGroup G] : AddTorsor G G where
  vsub := Sub.sub
  vsub_vadd' := sub_add_cancel
  vadd_vsub' := add_sub_cancel_right

Additive Group as a Torsor over Itself

Informal description

For any additive group $G$, $G$ is an additive torsor over itself. This means that $G$ acts on itself transitively and freely via the group addition operation $+$, and the difference between any two elements $g_1, g_2 \in G$ is given by $g_1 - g_2$.

vsub_eq_sub theorem

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

Full source

/-- Simplify subtraction for a torsor for an `AddGroup G` over
itself. -/
@[simp]
theorem vsub_eq_sub {G : Type*} [AddGroup G] (g₁ g₂ : G) : g₁ -ᵥ g₂ = g₁ - g₂ :=
  rfl

Torsor subtraction equals group subtraction in an additive group

Informal description

For any elements $g_1$ and $g_2$ in an additive group $G$, the torsor subtraction $g_1 -ᵥ g_2$ equals the group subtraction $g_1 - g_2$.

vsub_vadd theorem

(p₁ p₂ : P) : (p₁ -ᵥ p₂) +ᵥ p₂ = p₁

Full source

/-- Adding the result of subtracting from another point produces that
point. -/
@[simp]
theorem vsub_vadd (p₁ p₂ : P) : (p₁ -ᵥ p₂) +ᵥ p₂ = p₁ :=
  AddTorsor.vsub_vadd' p₁ p₂

Difference Vector Action Recovers Original Point in Additive Torsor

Informal description

For any two points $p_1$ and $p_2$ in an additive torsor $P$ over an additive group $G$, the action of the difference vector $(p_1 -ᵥ p_2)$ on $p_2$ yields $p_1$, i.e., $(p_1 -ᵥ p_2) +ᵥ p_2 = p_1$.

vadd_vsub theorem

(g : G) (p : P) : (g +ᵥ p) -ᵥ p = g

Full source

/-- Adding a group element then subtracting the original point
produces that group element. -/
@[simp]
theorem vadd_vsub (g : G) (p : P) : (g +ᵥ p) -ᵥ p = g :=
  AddTorsor.vadd_vsub' g p

Translation and Difference Recover Group Element in Additive Torsor

Informal description

For any element $g$ of an additive group $G$ and any point $p$ in an additive torsor $P$ over $G$, the difference between the translated point $g +ᵥ p$ and the original point $p$ is equal to $g$, i.e., $(g +ᵥ p) -ᵥ p = g$.

vadd_right_cancel theorem

{g₁ g₂ : G} (p : P) (h : g₁ +ᵥ p = g₂ +ᵥ p) : g₁ = g₂

Full source

/-- If the same point added to two group elements produces equal
results, those group elements are equal. -/
theorem vadd_right_cancel {g₁ g₂ : G} (p : P) (h : g₁ +ᵥ p = g₂ +ᵥ p) : g₁ = g₂ := by
  rw [← vadd_vsub g₁ p, h, vadd_vsub]

Right Cancellation Property for Additive Group Action on Torsor

Informal description

Let $G$ be an additive group acting on a torsor $P$. For any two group elements $g_1, g_2 \in G$ and any point $p \in P$, if $g_1 +ᵥ p = g_2 +ᵥ p$, then $g_1 = g_2$.

vadd_right_cancel_iff theorem

{g₁ g₂ : G} (p : P) : g₁ +ᵥ p = g₂ +ᵥ p ↔ g₁ = g₂

Full source

@[simp]
theorem vadd_right_cancel_iff {g₁ g₂ : G} (p : P) : g₁ +ᵥ pg₁ +ᵥ p = g₂ +ᵥ p ↔ g₁ = g₂ :=
  ⟨vadd_right_cancel p, fun h => h ▸ rfl⟩

Right Cancellation Equivalence for Additive Group Action on Torsor

Informal description

For any two elements $g_1, g_2$ of an additive group $G$ and any point $p$ in an additive torsor $P$ over $G$, the equality $g_1 +ᵥ p = g_2 +ᵥ p$ holds if and only if $g_1 = g_2$.

vadd_right_injective theorem

(p : P) : Function.Injective ((· +ᵥ p) : G → P)

Full source

/-- Adding a group element to the point `p` is an injective
function. -/
theorem vadd_right_injective (p : P) : Function.Injective ((· +ᵥ p) : G → P) := fun _ _ =>
  vadd_right_cancel p

Injectivity of Group Action on Torsor Points

Informal description

For any point $p$ in an additive torsor $P$ acted upon by an additive group $G$, the function $g \mapsto g +ᵥ p$ from $G$ to $P$ is injective. In other words, if $g_1 +ᵥ p = g_2 +ᵥ p$ for some $g_1, g_2 \in G$, then $g_1 = g_2$.

vadd_vsub_assoc theorem

(g : G) (p₁ p₂ : P) : (g +ᵥ p₁) -ᵥ p₂ = g + (p₁ -ᵥ p₂)

Full source

/-- Adding a group element to a point, then subtracting another point,
produces the same result as subtracting the points then adding the
group element. -/
theorem vadd_vsub_assoc (g : G) (p₁ p₂ : P) : (g +ᵥ p₁) -ᵥ p₂ = g + (p₁ -ᵥ p₂) := by
  apply vadd_right_cancel p₂
  rw [vsub_vadd, add_vadd, vsub_vadd]

Associativity of Group Action and Difference in Additive Torsor: $(g +ᵥ p_1) -ᵥ p_2 = g + (p_1 -ᵥ p_2)$

Informal description

Let $G$ be an additive group acting on a torsor $P$. For any group element $g \in G$ and points $p_1, p_2 \in P$, the difference vector $(g +ᵥ p_1) -ᵥ p_2$ equals $g + (p_1 -ᵥ p_2)$.

vsub_self theorem

(p : P) : p -ᵥ p = (0 : G)

Full source

/-- Subtracting a point from itself produces 0. -/
@[simp]
theorem vsub_self (p : P) : p -ᵥ p = (0 : G) := by
  rw [← zero_add (p -ᵥ p), ← vadd_vsub_assoc, vadd_vsub]

Self-Difference Yields Zero in Additive Torsor

Informal description

For any point $p$ in an additive torsor $P$ over an additive group $G$, the difference between $p$ and itself is the zero element of $G$, i.e., $p -ᵥ p = 0$.

vsub_eq_zero_iff_eq theorem

{p₁ p₂ : P} : p₁ -ᵥ p₂ = (0 : G) ↔ p₁ = p₂

Full source

/-- Subtracting two points produces 0 if and only if they are
equal. -/
@[simp]
theorem vsub_eq_zero_iff_eq {p₁ p₂ : P} : p₁ -ᵥ p₂p₁ -ᵥ p₂ = (0 : G) ↔ p₁ = p₂ :=
  Iff.intro eq_of_vsub_eq_zero fun h => h ▸ vsub_self _

Difference Vector is Zero if and only if Points are Equal

Informal description

For any two points $p_1$ and $p_2$ in an additive torsor $P$ over an additive group $G$, the difference vector $p_1 -ᵥ p_2$ equals the zero element of $G$ if and only if $p_1 = p_2$.

vsub_ne_zero theorem

{p q : P} : p -ᵥ q ≠ (0 : G) ↔ p ≠ q

Full source

theorem vsub_ne_zero {p q : P} : p -ᵥ qp -ᵥ q ≠ (0 : G)p -ᵥ q ≠ (0 : G) ↔ p ≠ q :=
  not_congr vsub_eq_zero_iff_eq

Nonzero Difference Vector Characterizes Distinct Points in Additive Torsor

Informal description

For any two points $p$ and $q$ in an additive torsor $P$ over an additive group $G$, the difference vector $p -ᵥ q$ is nonzero if and only if $p \neq q$.

vsub_add_vsub_cancel theorem

(p₁ p₂ p₃ : P) : p₁ -ᵥ p₂ + (p₂ -ᵥ p₃) = p₁ -ᵥ p₃

Full source

/-- Cancellation adding the results of two subtractions. -/
@[simp]
theorem vsub_add_vsub_cancel (p₁ p₂ p₃ : P) : p₁ -ᵥ p₂ + (p₂ -ᵥ p₃) = p₁ -ᵥ p₃ := by
  apply vadd_right_cancel p₃
  rw [add_vadd, vsub_vadd, vsub_vadd, vsub_vadd]

Chained Difference Vector Cancellation in Additive Torsor

Informal description

For any three points $p_1, p_2, p_3$ in an additive torsor $P$ over an additive group $G$, the sum of the difference vectors $(p_1 -ᵥ p_2)$ and $(p_2 -ᵥ p_3)$ equals the difference vector $(p_1 -ᵥ p_3)$, i.e., $$(p_1 -ᵥ p_2) + (p_2 -ᵥ p_3) = p_1 -ᵥ p_3.$$

neg_vsub_eq_vsub_rev theorem

(p₁ p₂ : P) : -(p₁ -ᵥ p₂) = p₂ -ᵥ p₁

Full source

/-- Subtracting two points in the reverse order produces the negation
of subtracting them. -/
@[simp]
theorem neg_vsub_eq_vsub_rev (p₁ p₂ : P) : -(p₁ -ᵥ p₂) = p₂ -ᵥ p₁ := by
  refine neg_eq_of_add_eq_zero_right (vadd_right_cancel p₁ ?_)
  rw [vsub_add_vsub_cancel, vsub_self]

Negation of Difference Vector Equals Reverse Difference in Additive Torsor

Informal description

For any two points $p_1, p_2$ in an additive torsor $P$ over an additive group $G$, the negation of the difference vector $(p_1 -ᵥ p_2)$ is equal to the difference vector in the reverse order $(p_2 -ᵥ p_1)$, i.e., $$-(p_1 -ᵥ p_2) = p_2 -ᵥ p_1.$$

vadd_vsub_eq_sub_vsub theorem

(g : G) (p q : P) : (g +ᵥ p) -ᵥ q = g - (q -ᵥ p)

Full source

theorem vadd_vsub_eq_sub_vsub (g : G) (p q : P) : (g +ᵥ p) -ᵥ q = g - (q -ᵥ p) := by
  rw [vadd_vsub_assoc, sub_eq_add_neg, neg_vsub_eq_vsub_rev]

Group Action and Difference Vector Relation: $(g +ᵥ p) -ᵥ q = g - (q -ᵥ p)$

Informal description

Let $G$ be an additive group acting on a torsor $P$. For any group element $g \in G$ and points $p, q \in P$, the difference vector $(g +ᵥ p) -ᵥ q$ equals $g - (q -ᵥ p)$.

vsub_vadd_eq_vsub_sub theorem

(p₁ p₂ : P) (g : G) : p₁ -ᵥ (g +ᵥ p₂) = p₁ -ᵥ p₂ - g

Full source

/-- Subtracting the result of adding a group element produces the same result
as subtracting the points and subtracting that group element. -/
theorem vsub_vadd_eq_vsub_sub (p₁ p₂ : P) (g : G) : p₁ -ᵥ (g +ᵥ p₂) = p₁ -ᵥ p₂ - g := by
  rw [← add_right_inj (p₂ -ᵥ p₁ : G), vsub_add_vsub_cancel, ← neg_vsub_eq_vsub_rev, vadd_vsub, ←
    add_sub_assoc, ← neg_vsub_eq_vsub_rev, neg_add_cancel, zero_sub]

Difference Vector of Translated Point Equals Difference Minus Group Element

Informal description

For any points $p_1, p_2$ in an additive torsor $P$ over an additive group $G$, and any group element $g \in G$, the difference vector between $p_1$ and the translated point $g +ᵥ p_2$ is equal to the difference vector $p_1 -ᵥ p_2$ minus $g$, i.e., $$p_1 -ᵥ (g +ᵥ p_2) = (p_1 -ᵥ p_2) - g.$$

vsub_sub_vsub_cancel_right theorem

(p₁ p₂ p₃ : P) : p₁ -ᵥ p₃ - (p₂ -ᵥ p₃) = p₁ -ᵥ p₂

Full source

/-- Cancellation subtracting the results of two subtractions. -/
@[simp]
theorem vsub_sub_vsub_cancel_right (p₁ p₂ p₃ : P) : p₁ -ᵥ p₃ - (p₂ -ᵥ p₃) = p₁ -ᵥ p₂ := by
  rw [← vsub_vadd_eq_vsub_sub, vsub_vadd]

Right Cancellation Law for Difference Vectors in Additive Torsor: $(p_1 -ᵥ p_3) - (p_2 -ᵥ p_3) = p_1 -ᵥ p_2$

Informal description

For any three points $p_1, p_2, p_3$ in an additive torsor $P$ over an additive group $G$, the difference of the vectors $(p_1 -ᵥ p_3)$ and $(p_2 -ᵥ p_3)$ equals the vector $(p_1 -ᵥ p_2)$, i.e., $$(p_1 -ᵥ p_3) - (p_2 -ᵥ p_3) = p_1 -ᵥ p_2.$$

vadd_eq_vadd_iff_neg_add_eq_vsub theorem

{v₁ v₂ : G} {p₁ p₂ : P} : v₁ +ᵥ p₁ = v₂ +ᵥ p₂ ↔ -v₁ + v₂ = p₁ -ᵥ p₂

Full source

theorem vadd_eq_vadd_iff_neg_add_eq_vsub {v₁ v₂ : G} {p₁ p₂ : P} :
    v₁ +ᵥ p₁v₁ +ᵥ p₁ = v₂ +ᵥ p₂ ↔ -v₁ + v₂ = p₁ -ᵥ p₂ := by
  rw [eq_vadd_iff_vsub_eq, vadd_vsub_assoc, ← add_right_inj (-v₁), neg_add_cancel_left, eq_comm]

Equality of Translated Points in Additive Torsor: $v_1 +ᵥ p_1 = v_2 +ᵥ p_2 \leftrightarrow -v_1 + v_2 = p_1 -ᵥ p_2$

Informal description

Let $G$ be an additive group acting on a torsor $P$. For any group elements $v_1, v_2 \in G$ and points $p_1, p_2 \in P$, the equality $v_1 +ᵥ p_1 = v_2 +ᵥ p_2$ holds if and only if $-v_1 + v_2 = p_1 -ᵥ p_2$.

vadd_vsub_vadd_cancel_right theorem

(v₁ v₂ : G) (p : P) : (v₁ +ᵥ p) -ᵥ (v₂ +ᵥ p) = v₁ - v₂

Full source

@[simp]
theorem vadd_vsub_vadd_cancel_right (v₁ v₂ : G) (p : P) : (v₁ +ᵥ p) -ᵥ (v₂ +ᵥ p) = v₁ - v₂ := by
  rw [vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, vsub_self, add_zero]

Difference of Translated Points Equals Group Difference: $(v_1 +ᵥ p) -ᵥ (v_2 +ᵥ p) = v_1 - v_2$

Informal description

For any elements $v_1, v_2$ of an additive group $G$ and any point $p$ in an additive torsor $P$ over $G$, the difference between the translated points $v_1 +ᵥ p$ and $v_2 +ᵥ p$ is equal to the difference $v_1 - v_2$ in $G$, i.e., $$(v_1 +ᵥ p) -ᵥ (v_2 +ᵥ p) = v_1 - v_2.$$

Equiv.vaddConst definition

(p : P) : G ≃ P

Full source

/-- `v ↦ v +ᵥ p` as an equivalence. -/
def vaddConst (p : P) : G ≃ P where
  toFun v := v +ᵥ p
  invFun p' := p' -ᵥ p
  left_inv _ := vadd_vsub _ _
  right_inv _ := vsub_vadd _ _

Equivalence between group and torsor via translation at a point

Informal description

For a point $p$ in an additive torsor $P$ over an additive group $G$, the function $\text{vaddConst}(p)$ is an equivalence (bijection with inverse) between $G$ and $P$, defined by mapping each group element $v$ to the translated point $v +ᵥ p$. The inverse function maps each point $p'$ in $P$ to the difference vector $p' -ᵥ p$ in $G$. This equivalence satisfies $\text{vaddConst}(p)(v) -ᵥ p = v$ for all $v \in G$ and $(p' -ᵥ p) +ᵥ p = p'$ for all $p' \in P$.

Equiv.coe_vaddConst theorem

(p : P) : ⇑(vaddConst p) = fun v => v +ᵥ p

Full source

@[simp]
theorem coe_vaddConst (p : P) : ⇑(vaddConst p) = fun v => v +ᵥ p :=
  rfl

Function Definition of $\text{vaddConst}(p)$ as Group Action on Torsor

Informal description

For any point $p$ in an additive torsor $P$ over an additive group $G$, the function $\text{vaddConst}(p) : G \to P$ is given by $\text{vaddConst}(p)(v) = v +ᵥ p$ for all $v \in G$.

Equiv.coe_vaddConst_symm theorem

(p : P) : ⇑(vaddConst p).symm = fun p' => p' -ᵥ p

Full source

@[simp]
theorem coe_vaddConst_symm (p : P) : ⇑(vaddConst p).symm = fun p' => p' -ᵥ p :=
  rfl

Inverse of Group-to-Torsor Equivalence via Point Subtraction

Informal description

For any point $p$ in an additive torsor $P$ over an additive group $G$, the inverse of the equivalence $\text{vaddConst}(p) : G \simeq P$ is given by the function $p' \mapsto p' -ᵥ p$ for all $p' \in P$.

Equiv.constVSub definition

(p : P) : P ≃ G

Full source

/-- `p' ↦ p -ᵥ p'` as an equivalence. -/
def constVSub (p : P) : P ≃ G where
  toFun := (p -ᵥ ·)
  invFun := (-· +ᵥ p)
  left_inv p' := by simp
  right_inv v := by simp [vsub_vadd_eq_vsub_sub]

Bijection between points and group elements via subtraction from a fixed point

Informal description

For a point $p$ in an additive torsor $P$ over a group $G$, the function $p' \mapsto p -ᵥ p'$ is a bijection between $P$ and $G$, with inverse given by $v \mapsto -v +ᵥ p$.

Equiv.coe_constVSub theorem

(p : P) : ⇑(constVSub p) = (p -ᵥ ·)

Full source

@[simp] lemma coe_constVSub (p : P) : ⇑(constVSub p) = (p -ᵥ ·) := rfl

Function Representation of Point Subtraction in Additive Torsor

Informal description

For any point $p$ in an additive torsor $P$ over a group $G$, the function $\text{constVSub}(p) : P \to G$ is given by $p' \mapsto p -ᵥ p'$.

Equiv.coe_constVSub_symm theorem

(p : P) : ⇑(constVSub p).symm = fun (v : G) => -v +ᵥ p

Full source

@[simp]
theorem coe_constVSub_symm (p : P) : ⇑(constVSub p).symm = fun (v : G) => -v +ᵥ p :=
  rfl

Inverse of Point Subtraction Bijection in Additive Torsor

Informal description

For any point $p$ in an additive torsor $P$ over an additive group $G$, the inverse of the bijection $\text{constVSub}(p) : P \to G$ (given by $p' \mapsto p -ᵥ p'$) is the function $v \mapsto -v +ᵥ p$ from $G$ to $P$.

Equiv.constVAdd definition

(v : G) : Equiv.Perm P

Full source

/-- The permutation given by `p ↦ v +ᵥ p`. -/
def constVAdd (v : G) : Equiv.Perm P where
  toFun := (v +ᵥ ·)
  invFun := (-v +ᵥ ·)
  left_inv p := by simp [vadd_vadd]
  right_inv p := by simp [vadd_vadd]

Permutation by constant vector addition

Informal description

For an element $ v $ of an additive group $ G $ acting on a type $ P $, the function `constVAdd v` is the permutation of $ P $ that maps each point $ p $ to $ v +ᵥ p $, with inverse mapping $ p $ to $ -v +ᵥ p $.

Equiv.coe_constVAdd theorem

(v : G) : ⇑(constVAdd P v) = (v +ᵥ ·)

Full source

@[simp] lemma coe_constVAdd (v : G) : ⇑(constVAdd P v) = (v +ᵥ ·) := rfl

Coefficient of Constant Vector Addition Function

Informal description

For any element $v$ of an additive group $G$ acting on a type $P$, the function `constVAdd P v` is equal to the function that adds $v$ to a point in $P$, i.e., $\text{constVAdd}\, P\, v = (v +ᵥ \cdot)$.

Equiv.pointReflection definition

(x : P) : Perm P

Full source

/-- Point reflection in `x` as a permutation. -/
def pointReflection (x : P) : Perm P :=
  (constVSub x).trans (vaddConst x)

Point reflection permutation in an additive torsor

Informal description

For a point $x$ in an additive torsor $P$ over an additive group $G$, the point reflection at $x$ is the permutation of $P$ that maps each point $y$ to $(x -ᵥ y) +ᵥ x$. This is equivalent to the composition of the bijection $y \mapsto x -ᵥ y$ from $P$ to $G$ followed by the bijection $v \mapsto v +ᵥ x$ from $G$ back to $P$.

Equiv.pointReflection_apply theorem

(x y : P) : pointReflection x y = (x -ᵥ y) +ᵥ x

Full source

theorem pointReflection_apply (x y : P) : pointReflection x y = (x -ᵥ y) +ᵥ x :=
  rfl

Point Reflection Formula in an Additive Torsor: $\text{pointReflection}_x(y) = (x -ᵥ y) +ᵥ x$

Informal description

For any points $x$ and $y$ in an additive torsor $P$ over an additive group $G$, the point reflection of $y$ about $x$ is given by $(x -ᵥ y) +ᵥ x$, where $-ᵥ$ denotes the subtraction operation yielding a group element and $+ᵥ$ denotes the group action on $P$.

Equiv.pointReflection_vsub_left theorem

(x y : P) : pointReflection x y -ᵥ x = x -ᵥ y

Full source

@[simp]
theorem pointReflection_vsub_left (x y : P) : pointReflectionpointReflection x y -ᵥ x = x -ᵥ y :=
  vadd_vsub ..

Point Reflection Difference Identity: $\text{pointReflection}(x, y) -ᵥ x = x -ᵥ y$

Informal description

For any points $x$ and $y$ in an additive torsor $P$ over an additive group $G$, the difference between the point reflection of $y$ about $x$ and $x$ itself equals the difference between $x$ and $y$, i.e., $\text{pointReflection}(x, y) -ᵥ x = x -ᵥ y$.

Equiv.pointReflection_vsub_right theorem

(x y : P) : pointReflection x y -ᵥ y = 2 • (x -ᵥ y)

Full source

@[simp]
theorem pointReflection_vsub_right (x y : P) : pointReflectionpointReflection x y -ᵥ y = 2 • (x -ᵥ y) := by
  simp [pointReflection, two_nsmul, vadd_vsub_assoc]

Point Reflection Difference Identity: $(\text{pointReflection}\, x\, y) -ᵥ y = 2 \cdot (x -ᵥ y)$

Informal description

Let $P$ be an additive torsor over an additive group $G$. For any points $x, y \in P$, the difference between the point reflection of $y$ at $x$ and $y$ itself is equal to twice the difference between $x$ and $y$, i.e., $$(\text{pointReflection}\, x\, y) -ᵥ y = 2 \cdot (x -ᵥ y).$$

Equiv.pointReflection_symm theorem

(x : P) : (pointReflection x).symm = pointReflection x

Full source

@[simp]
theorem pointReflection_symm (x : P) : (pointReflection x).symm = pointReflection x :=
  ext <| by simp [pointReflection]

Point Reflection is Self-Inverse

Informal description

For any point $x$ in an additive torsor $P$ over an additive group $G$, the inverse of the point reflection at $x$ is equal to the point reflection at $x$ itself, i.e., $(\text{pointReflection}\, x)^{-1} = \text{pointReflection}\, x$.

Equiv.pointReflection_self theorem

(x : P) : pointReflection x x = x

Full source

@[simp]
theorem pointReflection_self (x : P) : pointReflection x x = x :=
  vsub_vadd _ _

Fixed Point Property of Point Reflection

Informal description

For any point $x$ in an additive torsor $P$ over an additive group $G$, the point reflection at $x$ maps $x$ to itself, i.e., $\text{pointReflection}(x)(x) = x$.

Equiv.pointReflection_involutive theorem

(x : P) : Involutive (pointReflection x : P → P)

Full source

theorem pointReflection_involutive (x : P) : Involutive (pointReflection x : P → P) := fun y =>
  (Equiv.apply_eq_iff_eq_symm_apply _).2 <| by rw [pointReflection_symm]

Point Reflection is Involutive

Informal description

For any point $x$ in an additive torsor $P$ over an additive group $G$, the point reflection map $\text{pointReflection}\, x : P \to P$ is involutive, meaning that applying it twice returns the original point, i.e., $\text{pointReflection}\, x (\text{pointReflection}\, x (y)) = y$ for all $y \in P$.

AddTorsor.subsingleton_iff theorem

(G P : Type*) [AddGroup G] [AddTorsor G P] : Subsingleton G ↔ Subsingleton P

Full source

theorem AddTorsor.subsingleton_iff (G P : Type*) [AddGroup G] [AddTorsor G P] :
    SubsingletonSubsingleton G ↔ Subsingleton P := by
  inhabit P
  exact (Equiv.vaddConst default).subsingleton_congr

Subsingleton Equivalence between Additive Group and Torsor

Informal description

For an additive group $G$ and an additive torsor $P$ over $G$, the group $G$ is a subsingleton (i.e., has at most one element) if and only if the torsor $P$ is a subsingleton.

Mathlib.Algebra.AddTorsor.Defs

Notations

Implementation notes

Notations

References