Documentation

Mathlib.Algebra.AddTorsor

Torsors of additive group actions #

This file defines torsors of additive group actions.

Notations #

The group elements are referred to as acting on points. This file defines the notation +ᵥ for adding a group element to a point and -ᵥ for subtracting two points to produce a group element.

Implementation notes #

Affine spaces are the motivating example of torsors of additive group actions. It may be appropriate to refactor in terms of the general definition of group actions, via to_additive, when there is a use for multiplicative torsors (currently mathlib only develops the theory of group actions for multiplicative group actions).

Notations #

References #

class AddTorsor (G : outParam (Type u_1)) (P : Type u_2) [outParam (AddGroup G)] extends AddAction , VSub :
Type (max u_1 u_2)
  • vadd : GPP
  • zero_vadd : ∀ (p : P), 0 +ᵥ p = p
  • add_vadd : ∀ (g₁ g₂ : G) (p : P), g₁ + g₂ +ᵥ p = g₁ +ᵥ (g₂ +ᵥ p)
  • vsub : PPG
  • Nonempty : Nonempty P
  • vsub_vadd' : ∀ (p1 p2 : P), p1 -ᵥ p2 +ᵥ p2 = p1

    Torsor subtraction and addition with the same element cancels out.

  • vadd_vsub' : ∀ (g : G) (p : P), g +ᵥ p -ᵥ p = g

    Torsor addition and subtraction with the same element cancels out.

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.

Instances
    instance addGroupIsAddTorsor (G : Type u_1) [AddGroup G] :

    An AddGroup G is a torsor for itself.

    Equations
    @[simp]
    theorem vsub_eq_sub {G : Type u_1} [AddGroup G] (g1 : G) (g2 : G) :
    g1 -ᵥ g2 = g1 - g2

    Simplify subtraction for a torsor for an AddGroup G over itself.

    @[simp]
    theorem vsub_vadd {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] (p1 : P) (p2 : P) :
    p1 -ᵥ p2 +ᵥ p2 = p1

    Adding the result of subtracting from another point produces that point.

    @[simp]
    theorem vadd_vsub {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] (g : G) (p : P) :
    g +ᵥ p -ᵥ p = g

    Adding a group element then subtracting the original point produces that group element.

    theorem vadd_right_cancel {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] {g1 : G} {g2 : G} (p : P) (h : g1 +ᵥ p = g2 +ᵥ p) :
    g1 = g2

    If the same point added to two group elements produces equal results, those group elements are equal.

    @[simp]
    theorem vadd_right_cancel_iff {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] {g1 : G} {g2 : G} (p : P) :
    g1 +ᵥ p = g2 +ᵥ p g1 = g2
    theorem vadd_right_injective {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] (p : P) :

    Adding a group element to the point p is an injective function.

    theorem vadd_vsub_assoc {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] (g : G) (p1 : P) (p2 : P) :
    g +ᵥ p1 -ᵥ p2 = g + (p1 -ᵥ p2)

    Adding a group element to a point, then subtracting another point, produces the same result as subtracting the points then adding the group element.

    @[simp]
    theorem vsub_self {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] (p : P) :
    p -ᵥ p = 0

    Subtracting a point from itself produces 0.

    theorem eq_of_vsub_eq_zero {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] {p1 : P} {p2 : P} (h : p1 -ᵥ p2 = 0) :
    p1 = p2

    If subtracting two points produces 0, they are equal.

    @[simp]
    theorem vsub_eq_zero_iff_eq {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] {p1 : P} {p2 : P} :
    p1 -ᵥ p2 = 0 p1 = p2

    Subtracting two points produces 0 if and only if they are equal.

    theorem vsub_ne_zero {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] {p : P} {q : P} :
    p -ᵥ q 0 p q
    @[simp]
    theorem vsub_add_vsub_cancel {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] (p1 : P) (p2 : P) (p3 : P) :
    p1 -ᵥ p2 + (p2 -ᵥ p3) = p1 -ᵥ p3

    Cancellation adding the results of two subtractions.

    @[simp]
    theorem neg_vsub_eq_vsub_rev {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] (p1 : P) (p2 : P) :
    -(p1 -ᵥ p2) = p2 -ᵥ p1

    Subtracting two points in the reverse order produces the negation of subtracting them.

    theorem vadd_vsub_eq_sub_vsub {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] (g : G) (p : P) (q : P) :
    g +ᵥ p -ᵥ q = g - (q -ᵥ p)
    theorem vsub_vadd_eq_vsub_sub {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] (p1 : P) (p2 : P) (g : G) :
    p1 -ᵥ (g +ᵥ p2) = p1 -ᵥ p2 - g

    Subtracting the result of adding a group element produces the same result as subtracting the points and subtracting that group element.

    @[simp]
    theorem vsub_sub_vsub_cancel_right {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] (p1 : P) (p2 : P) (p3 : P) :
    p1 -ᵥ p3 - (p2 -ᵥ p3) = p1 -ᵥ p2

    Cancellation subtracting the results of two subtractions.

    theorem eq_vadd_iff_vsub_eq {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] (p1 : P) (g : G) (p2 : P) :
    p1 = g +ᵥ p2 p1 -ᵥ p2 = g

    Convert between an equality with adding a group element to a point and an equality of a subtraction of two points with a group element.

    theorem vadd_eq_vadd_iff_neg_add_eq_vsub {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] {v₁ : G} {v₂ : G} {p₁ : P} {p₂ : P} :
    v₁ +ᵥ p₁ = v₂ +ᵥ p₂ -v₁ + v₂ = p₁ -ᵥ p₂
    theorem Set.singleton_vsub_self {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] (p : P) :
    {p} -ᵥ {p} = {0}
    @[simp]
    theorem vadd_vsub_vadd_cancel_right {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] (v₁ : G) (v₂ : G) (p : P) :
    v₁ +ᵥ p -ᵥ (v₂ +ᵥ p) = v₁ - v₂
    theorem vsub_left_cancel {G : Type u_1} {P : Type u_2} [AddGroup G] [T : AddTorsor G P] {p1 : P} {p2 : P} {p : P} (h : p1 -ᵥ p = p2 -ᵥ p) :
    p1 = p2

    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] {p1 : P} {p2 : P} {p : P} :
    p1 -ᵥ p = p2 -ᵥ p p1 = p2

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

    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] {p1 : P} {p2 : P} {p : P} (h : p -ᵥ p1 = p -ᵥ p2) :
    p1 = p2

    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] {p1 : P} {p2 : P} {p : P} :
    p -ᵥ p1 = p -ᵥ p2 p1 = p2

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

    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] (p1 : P) (p2 : P) (p3 : P) :
    p3 -ᵥ p2 - (p3 -ᵥ p1) = p1 -ᵥ p2

    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) (p1 : P) (p2 : P) :
    v +ᵥ p1 -ᵥ (v +ᵥ p2) = p1 -ᵥ p2
    theorem vsub_vadd_comm {G : Type u_1} {P : Type u_2} [AddCommGroup G] [AddTorsor G P] (p1 : P) (p2 : P) (p3 : P) :
    p1 -ᵥ p2 +ᵥ p3 = p3 -ᵥ p2 +ᵥ p1
    theorem vadd_eq_vadd_iff_sub_eq_vsub {G : Type u_1} {P : Type u_2} [AddCommGroup G] [AddTorsor G P] {v₁ : G} {v₂ : G} {p₁ : 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₁ -ᵥ p₃ - (p₂ -ᵥ p₄)
    instance Prod.instAddTorsor {G' : Type u_2} {P : Type u_3} {P' : Type u_4} {G : Type u_1} [AddGroup G] [AddGroup G'] [AddTorsor G P] [AddTorsor G' P'] :
    AddTorsor (G × G') (P × P')
    Equations
    @[simp]
    theorem Prod.fst_vadd {G' : Type u_2} {P : Type u_3} {P' : Type u_4} {G : Type u_1} [AddGroup G] [AddGroup G'] [AddTorsor G P] [AddTorsor G' P'] (v : G × G') (p : P × P') :
    (v +ᵥ p).fst = v.fst +ᵥ p.fst
    @[simp]
    theorem Prod.snd_vadd {G' : Type u_2} {P : Type u_3} {P' : Type u_4} {G : Type u_1} [AddGroup G] [AddGroup G'] [AddTorsor G P] [AddTorsor G' P'] (v : G × G') (p : P × P') :
    (v +ᵥ p).snd = v.snd +ᵥ p.snd
    @[simp]
    theorem Prod.mk_vadd_mk {G' : Type u_4} {P : Type u_2} {P' : Type u_3} {G : Type u_1} [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_4} {P : Type u_2} {P' : Type u_3} {G : Type u_1} [AddGroup G] [AddGroup G'] [AddTorsor G P] [AddTorsor G' P'] (p₁ : P × P') (p₂ : P × P') :
    (p₁ -ᵥ p₂).fst = p₁.fst -ᵥ p₂.fst
    @[simp]
    theorem Prod.snd_vsub {G' : Type u_4} {P : Type u_2} {P' : Type u_3} {G : Type u_1} [AddGroup G] [AddGroup G'] [AddTorsor G P] [AddTorsor G' P'] (p₁ : P × P') (p₂ : P × P') :
    (p₁ -ᵥ p₂).snd = p₁.snd -ᵥ p₂.snd
    @[simp]
    theorem Prod.mk_vsub_mk {G' : Type u_2} {P : Type u_4} {P' : Type u_3} {G : Type u_1} [AddGroup G] [AddGroup G'] [AddTorsor G P] [AddTorsor G' P'] (p₁ : P) (p₂ : P) (p₁' : P') (p₂' : P') :
    (p₁, p₁') -ᵥ (p₂, p₂') = (p₁ -ᵥ p₂, p₁' -ᵥ p₂')
    instance Pi.instAddTorsor {I : Type u} {fg : IType v} [(i : I) → AddGroup (fg i)] {fp : IType w} [T : (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 = AddTorsor.mk (_ : ∀ (p₁ p₂ : (i : I) → fp i), p₁ -ᵥ p₂ +ᵥ p₂ = p₁) (_ : ∀ (g : (i : I) → fg i) (p : (i : I) → fp i), g +ᵥ p -ᵥ p = g)
    def Equiv.vaddConst {G : Type u_1} {P : Type u_2} [AddGroup G] [AddTorsor G P] (p : P) :
    G P

    v ↦ v +ᵥ p as an equivalence.

    Equations
    Instances For
      @[simp]
      theorem Equiv.coe_vaddConst {G : Type u_1} {P : Type u_2} [AddGroup G] [AddTorsor G P] (p : P) :
      ↑(Equiv.vaddConst p) = fun v => v +ᵥ p
      @[simp]
      theorem Equiv.coe_vaddConst_symm {G : Type u_1} {P : Type u_2} [AddGroup G] [AddTorsor G P] (p : P) :
      (Equiv.vaddConst p).symm = fun p' => p' -ᵥ p
      def Equiv.constVSub {G : Type u_1} {P : Type u_2} [AddGroup G] [AddTorsor G P] (p : P) :
      P G

      p' ↦ p -ᵥ p' as an equivalence.

      Equations
      Instances For
        @[simp]
        theorem Equiv.coe_constVSub {G : Type u_1} {P : Type u_2} [AddGroup G] [AddTorsor G P] (p : P) :
        ↑(Equiv.constVSub p) = (fun x x_1 => x -ᵥ x_1) p
        @[simp]
        theorem Equiv.coe_constVSub_symm {G : Type u_1} {P : Type u_2} [AddGroup G] [AddTorsor G P] (p : P) :
        (Equiv.constVSub p).symm = fun v => -v +ᵥ p
        def Equiv.constVAdd {G : Type u_1} (P : Type u_2) [AddGroup G] [AddTorsor G P] (v : G) :

        The permutation given by p ↦ v +ᵥ p.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem Equiv.coe_constVAdd {G : Type u_1} (P : Type u_2) [AddGroup G] [AddTorsor G P] (v : G) :
          ↑(Equiv.constVAdd P v) = (fun x x_1 => x +ᵥ x_1) v
          @[simp]
          theorem Equiv.constVAdd_zero (G : Type u_1) (P : Type u_2) [AddGroup G] [AddTorsor G P] :
          @[simp]
          theorem Equiv.constVAdd_add {G : Type u_1} (P : Type u_2) [AddGroup G] [AddTorsor G P] (v₁ : G) (v₂ : G) :
          Equiv.constVAdd P (v₁ + v₂) = Equiv.constVAdd P v₁ * Equiv.constVAdd P v₂

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

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            def Equiv.pointReflection {G : Type u_1} {P : Type u_2} [AddGroup G] [AddTorsor G P] (x : P) :

            Point reflection in x as a permutation.

            Equations
            Instances For
              theorem Equiv.pointReflection_apply {G : Type u_1} {P : Type u_2} [AddGroup G] [AddTorsor G P] (x : P) (y : P) :
              @[simp]
              theorem Equiv.pointReflection_vsub_left {G : Type u_1} {P : Type u_2} [AddGroup G] [AddTorsor G P] (x : P) (y : P) :
              @[simp]
              theorem Equiv.left_vsub_pointReflection {G : Type u_1} {P : Type u_2} [AddGroup G] [AddTorsor G P] (x : P) (y : P) :
              @[simp]
              theorem Equiv.pointReflection_vsub_right {G : Type u_1} {P : Type u_2} [AddGroup G] [AddTorsor G P] (x : P) (y : P) :
              ↑(Equiv.pointReflection x) y -ᵥ y = 2 (x -ᵥ y)
              @[simp]
              theorem Equiv.right_vsub_pointReflection {G : Type u_1} {P : Type u_2} [AddGroup G] [AddTorsor G P] (x : P) (y : P) :
              y -ᵥ ↑(Equiv.pointReflection x) y = 2 (y -ᵥ x)
              @[simp]
              theorem Equiv.pointReflection_symm {G : Type u_1} {P : Type u_2} [AddGroup G] [AddTorsor G P] (x : P) :
              @[simp]
              theorem Equiv.pointReflection_self {G : Type u_1} {P : Type u_2} [AddGroup G] [AddTorsor G P] (x : P) :
              theorem Equiv.pointReflection_fixed_iff_of_injective_bit0 {G : Type u_1} {P : Type u_2} [AddGroup G] [AddTorsor G P] {x : P} {y : P} (h : Function.Injective bit0) :
              ↑(Equiv.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.