Documentation

Mathlib.Algebra.AddTorsor.Basic

Torsors of additive group actions #

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

source
šŸ“ coverage
theorem Set.singleton_vsub_self {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] (p : P) :
{p} -įµ„ {p} = {0}
source
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.

source
šŸ“ coverage
@[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.

source
šŸ“ coverage
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.

source
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.

source
šŸ“ coverage
@[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.

source
šŸ“ coverage
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.

source
šŸ“ coverage
@[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.

source
šŸ“ coverage
@[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ā‚‚
source
šŸ“ coverage
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ā‚‚)
source
šŸ“ coverage
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ā‚‚)
source
šŸ“ coverage
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ā‚
source
šŸ“ coverage
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ā‚‚
source
šŸ“ coverage
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ā‚„)
source
šŸ“ coverage
@[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
source
šŸ”ø coverage
@[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')
source
šŸ“ coverage
@[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
source
šŸ“ coverage
@[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
source
šŸ“ coverage
@[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')
source
šŸ“ coverage
@[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
source
šŸ“ coverage
@[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
source
šŸ“ coverage
@[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ā‚‚')
source
šŸ”ø coverage
@[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.

source
šŸ“ coverage
@[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
source
šŸ“ coverage
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
source
šŸ“ coverage
@[simp]
theorem Equiv.constVAdd_zero (G : Type u_1) (P : Type u_2) [AddGroup G] [AddTorsor G P] :
constVAdd P 0 = 1
source
šŸ“ coverage
@[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ā‚‚
source
šŸ”ø coverage
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

Instances For
    source
    šŸ“ coverage
    @[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
    source
    šŸ“ coverage
    @[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)
    source
    šŸ“ coverage
    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.

    source
    šŸ“ coverage
    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
    source
    šŸ“ coverage
    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).

    source
    šŸ”ø coverage
    @[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.

    Instances For
      source
      šŸ”ø coverage
      @[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.

      Instances For