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

      Equations
        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).