Torsors of additive group actions

Further results for torsors, that are not in Mathlib/Algebra/AddTorsor/Defs.lean to avoid increasing imports there.

theorem Set.singleton_vsub_self {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] (p : P) : {p} -ᵥ {p} = {0}

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 vadd_vsub_vadd_comm {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 sub_add_vsub_comm {G : Type u_1} {P : Type u_2} [AddCommGroup G] [AddTorsor G P] (v₁ v₂ : G) (p₁ p₂ : P) : v₁ - v₂ + (p₁ -ᵥ p₂) = (v₁ +ᵥ p₁) -ᵥ (v₂ +ᵥ 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₄)

@[simp]

theorem Set.vadd_set_vsub_vadd_set {G : Type u_1} {P : Type u_2} [AddCommGroup G] [AddTorsor G P] (v : G) (s t : Set P) : (v +ᵥ s) -ᵥ (v +ᵥ t) = s -ᵥ t

@[implicit_reducible]

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

• One or more equations did not get rendered due to their size.

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

@[implicit_reducible]

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 = { toAddAction := Pi.addAction', vsub := fun (p₁ p₂ : (i : I) → fp i) (i : I) => p₁ i -ᵥ p₂ i, nonempty := ⋯, vsub_vadd' := ⋯, vadd_vsub' := ⋯ }

@[simp]

theorem Pi.vsub_apply {I : Type u} {fg : I → Type v} [(i : I) → AddGroup (fg i)] {fp : I → Type w} [(i : I) → AddTorsor (fg i) (fp i)] (p q : (i : I) → fp i) (i : I) : (p -ᵥ q) i = p i -ᵥ q i

theorem Pi.vsub_def {I : Type u} {fg : I → Type v} [(i : I) → AddGroup (fg i)] {fp : I → Type w} [(i : I) → AddTorsor (fg i) (fp i)] (p q : (i : I) → fp i) : p -ᵥ q = fun (i : I) => p i -ᵥ q i

@[simp]

theorem Equiv.constVAdd_zero (G : Type u_1) (P : Type u_2) [AddGroup G] [AddTorsor G P] : 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) : constVAdd P (v₁ + v₂) = constVAdd P v₁ * constVAdd P v₂

def Equiv.constVAddHom {G : Type u_1} (P : Type u_2) [AddGroup G] [AddTorsor G P] : Multiplicative G →* 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' := ⋯ }

@[simp]

theorem Equiv.left_vsub_pointReflection {G : Type u_1} {P : Type u_2} [AddGroup G] [AddTorsor G P] (x y : P) : x -ᵥ (pointReflection x) y = y -ᵥ x

@[simp]

theorem Equiv.right_vsub_pointReflection {G : Type u_1} {P : Type u_2} [AddGroup G] [AddTorsor G P] (x y : P) : y -ᵥ (pointReflection x) y = 2 • (y -ᵥ 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) : (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.

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) => (pointReflection x) y

theorem Equiv.pointReflection_eq_subLeft {G : Type u_3} [AddCommGroup G] (x : G) : pointReflection x = Equiv.subLeft (2 • x)

In the special case of additive commutative groups (as opposed to just additive torsors), Equiv.pointReflection x coincides with Equiv.subLeft (2 • x).

@[reducible, inline]

abbrev Function.Injective.addTorsor {G : Type u_1} {P : Type u_2} {Q : Type u_3} [AddGroup G] [AddTorsor G P] [VAdd G Q] [VSub G Q] [Nonempty Q] (f : Q → P) (hf : Injective f) (vadd : ∀ (c : G) (x : Q), f (c +ᵥ x) = c +ᵥ f x) (vsub : ∀ (x y : Q), x -ᵥ y = f x -ᵥ f y) : AddTorsor G Q

Pullback of an add torsor along an injective map.

Equations

• Function.Injective.addTorsor f hf vadd vsub = { toAddAction := Function.Injective.addAction f hf vadd, toVSub := inst✝¹, nonempty := inst✝, vsub_vadd' := ⋯, vadd_vsub' := ⋯ }

@[reducible, inline]

abbrev Function.Surjective.addTorsor {G : Type u_1} {P : Type u_2} {Q : Type u_3} [AddGroup G] [AddTorsor G P] [VAdd G Q] [VSub G Q] (f : P → Q) (hf : Surjective f) (vadd : ∀ (c : G) (x : P), f (c +ᵥ x) = c +ᵥ f x) (vsub : ∀ (x y : P), x -ᵥ y = f x -ᵥ f y) : AddTorsor G Q

Pushforward of an add torsor along a surjective map.

Equations

• Function.Surjective.addTorsor f hf vadd vsub = { toAddAction := Function.Surjective.addAction f hf vadd, toVSub := inst✝, nonempty := ⋯, vsub_vadd' := ⋯, vadd_vsub' := ⋯ }