Torsors of group actions

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

theorem Set.singleton_sdiv_self {G : Type u_1} {P : Type u_2} [Group G] [T : Torsor G P] (p : P) : {p} /ₛ {p} = {1}

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 sdiv_left_cancel {G : Type u_1} {P : Type u_2} [Group G] [T : Torsor G P] {p₁ p₂ p : P} (h : p₁ /ₛ p = p₂ /ₛ p) : p₁ = p₂

If dividing two points by the same point produces equal results, those points are equal.

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 sdiv_left_cancel_iff {G : Type u_1} {P : Type u_2} [Group G] [T : Torsor G P] {p₁ p₂ p : P} : p₁ /ₛ p = p₂ /ₛ p ↔ p₁ = p₂

Dividing two points by the same point produces equal results if and only if 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 sdiv_left_injective {G : Type u_1} {P : Type u_2} [Group G] [T : Torsor G P] (p : P) : Function.Injective fun (x : P) => x /ₛ p

Dividing by the point p is an injective function.

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 sdiv_right_cancel {G : Type u_1} {P : Type u_2} [Group G] [T : Torsor G P] {p₁ p₂ p : P} (h : p /ₛ p₁ = p /ₛ p₂) : p₁ = p₂

If dividing the same point by two points produces equal results, those points are equal.

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 sdiv_right_cancel_iff {G : Type u_1} {P : Type u_2} [Group G] [T : Torsor 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.

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

theorem sdiv_right_injective {G : Type u_1} {P : Type u_2} [Group G] [T : Torsor G P] (p : P) : Function.Injective fun (x : P) => p /ₛ x

Dividing the point p by other points is an injective function.

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 sdiv_div_sdiv_cancel_left {G : Type u_1} {P : Type u_2} [CommGroup G] [Torsor G P] (p₁ p₂ p₃ : P) : (p₃ /ₛ p₂) / (p₃ /ₛ p₁) = p₁ /ₛ p₂

Cancellation dividing the results of two divisions.

@[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 smul_sdiv_smul_cancel_left {G : Type u_1} {P : Type u_2} [CommGroup G] [Torsor G P] (v : G) (p₁ p₂ : P) : v • p₁ /ₛ v • p₂ = p₁ /ₛ p₂

@[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 smul_sdiv_smul_comm {G : Type u_1} {P : Type u_2} [CommGroup G] [Torsor G P] (v₁ v₂ : G) (p₁ p₂ : P) : v₁ • p₁ /ₛ v₂ • p₂ = v₁ / v₂ * (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 div_mul_sdiv_comm {G : Type u_1} {P : Type u_2} [CommGroup G] [Torsor G P] (v₁ v₂ : G) (p₁ p₂ : P) : v₁ / v₂ * (p₁ /ₛ p₂) = v₁ • p₁ /ₛ v₂ • 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 sdiv_smul_comm {G : Type u_1} {P : Type u_2} [CommGroup G] [Torsor G P] (p₁ p₂ p₃ : P) : (p₁ /ₛ p₂) • p₃ = (p₃ /ₛ p₂) • 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 smul_eq_smul_iff_div_eq_sdiv {G : Type u_1} {P : Type u_2} [CommGroup G] [Torsor G P] {v₁ v₂ : G} {p₁ p₂ : P} : v₁ • p₁ = v₂ • p₂ ↔ v₂ / v₁ = 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 sdiv_div_sdiv_comm {G : Type u_1} {P : Type u_2} [CommGroup G] [Torsor G P] (p₁ p₂ p₃ p₄ : P) : (p₁ /ₛ p₂) / (p₃ /ₛ p₄) = (p₁ /ₛ p₃) / (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.smul_set_sdiv_smul_set {G : Type u_1} {P : Type u_2} [CommGroup G] [Torsor G P] (v : G) (s t : Set P) : v • s /ₛ v • t = s /ₛ t

@[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.instTorsor {G : Type u_1} {G' : Type u_2} {P : Type u_3} {P' : Type u_4} [Group G] [Group G'] [Torsor G P] [Torsor G' P'] : Torsor (G × G') (P × P')

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

@[simp]

theorem Prod.fst_smul {G : Type u_1} {G' : Type u_2} {P : Type u_3} {P' : Type u_4} [Group G] [Group G'] [Torsor G P] [Torsor G' P'] (v : G × G') (p : P × P') : (v • p).1 = v.1 • p.1

@[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_smul {G : Type u_1} {G' : Type u_2} {P : Type u_3} {P' : Type u_4} [Group G] [Group G'] [Torsor G P] [Torsor G' P'] (v : G × G') (p : P × P') : (v • p).2 = v.2 • p.2

@[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_smul_mk {G : Type u_1} {G' : Type u_2} {P : Type u_3} {P' : Type u_4} [Group G] [Group G'] [Torsor G P] [Torsor G' P'] (v : G) (v' : G') (p : P) (p' : P') : (v, v') • (p, p') = (v • p, v' • p')

@[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_sdiv {G : Type u_1} {G' : Type u_2} {P : Type u_3} {P' : Type u_4} [Group G] [Group G'] [Torsor G P] [Torsor G' P'] (p₁ p₂ : P × P') : (p₁ /ₛ p₂).1 = p₁.1 /ₛ p₂.1

@[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_sdiv {G : Type u_1} {G' : Type u_2} {P : Type u_3} {P' : Type u_4} [Group G] [Group G'] [Torsor G P] [Torsor G' P'] (p₁ p₂ : P × P') : (p₁ /ₛ p₂).2 = p₁.2 /ₛ p₂.2

@[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_sdiv_mk {G : Type u_1} {G' : Type u_2} {P : Type u_3} {P' : Type u_4} [Group G] [Group G'] [Torsor G P] [Torsor G' P'] (p₁ p₂ : P) (p₁' p₂' : P') : (p₁, p₁') /ₛ (p₂, p₂') = (p₁ /ₛ p₂, p₁' /ₛ p₂')

@[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.instTorsor {I : Type u} {fg : I → Type v} [(i : I) → Group (fg i)] {fp : I → Type w} [(i : I) → Torsor (fg i) (fp i)] : Torsor ((i : I) → fg i) ((i : I) → fp i)

A product of Torsors is a Torsor.

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

@[simp]

theorem Pi.sdiv_apply {I : Type u} {fg : I → Type v} [(i : I) → Group (fg i)] {fp : I → Type w} [(i : I) → Torsor (fg i) (fp i)] (p q : (i : I) → fp i) (i : I) : (p /ₛ q) i = p i /ₛ q i

@[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.sdiv_def {I : Type u} {fg : I → Type v} [(i : I) → Group (fg i)] {fp : I → Type w} [(i : I) → Torsor (fg i) (fp i)] (p q : (i : I) → fp i) : p /ₛ q = fun (i : 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.constSMul_one (G : Type u_1) (P : Type u_2) [Group G] [Torsor G P] : constSMul P 1 = 1

@[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.constSMul_mul {G : Type u_1} (P : Type u_2) [Group G] [Torsor G P] (v₁ v₂ : G) : constSMul P (v₁ * v₂) = constSMul P v₁ * constSMul P v₂

@[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_3) (P : Type u_4) [AddGroup G] [AddTorsor G P] : Multiplicative G →* Perm P

Equiv.constVAdd as a homomorphism from Multiplicative G to Equiv.perm P

def Equiv.constSMulHom {G : Type u_1} (P : Type u_2) [Group G] [Torsor G P] : G →* Perm P

Equiv.constSMul as a homomorphism from G to Equiv.perm P

@[simp]

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

@[simp]

theorem Equiv.right_vsub_pointReflection {G : Type u_3} {P : Type u_4} [AddGroup G] [T : 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_3} {P : Type u_4} [AddGroup G] [T : 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_5} {P : Type u_6} [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_5} [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.torsor {G : Type u_1} {P : Type u_2} {Q : Type u_3} [Group G] [Torsor G P] [SMul G Q] [SDiv G Q] [Nonempty Q] (f : Q → P) (hf : Injective f) (smul : ∀ (c : G) (x : Q), f (c • x) = c • f x) (sdiv : ∀ (x y : Q), x /ₛ y = f x /ₛ f y) : Torsor G Q

Pullback of a torsor along an injective map.

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

@[reducible, inline]

abbrev Function.Surjective.torsor {G : Type u_1} {P : Type u_2} {Q : Type u_3} [Group G] [Torsor G P] [SMul G Q] [SDiv G Q] (f : P → Q) (hf : Surjective f) (smul : ∀ (c : G) (x : P), f (c • x) = c • f x) (sdiv : ∀ (x y : P), x /ₛ y = f x /ₛ f y) : Torsor G Q

Pushforward of a torsor along a surjective map.

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