Torsion-freeness of P

This file contains a proof that the group P defined is in fact torsion-free.

Roughly, the steps are as follows (further details can be found in the corresponding .md file):

1. Define a function sq : P -> K taking a group element (q, k) to its square. This element lies in the kernel as the group ℤ/2 × ℤ/2 has exponent 2.
2. Show that elements in K, which are integer triples of the form (a, b, c), do not have torsion. This requires the fact that the group ℤ, and hence ℤ³, is torsion-free.
3. Show that no element of P has order precisely 2. This is an argument by cases on the Q part of a general element of P.
4. Finally, show that if an element g : G of a group G satisfies g ^ n = (1 : G), then it also satisfies (g ^ 2) ^ n = (1 : G).
5. Together, these statements show that P is torsion-free.

Torsion-free groups

class LeanPool.Polylean.TorsionFree (G : Type u_1) [Group G] : Prop

The definition of a torsion-free group.

• torsionFree (g : G) (n : ℕ) : g ^ n.succ = 1 → g = 1

  A group is torsion-free if the only element with non-trivial torsion is the identity element.

class LeanPool.Polylean.AddTorsionFree (A : Type u_1) [AddGroup A] : Prop

The definition of torsion-free additive groups.

• torsionFree (a : A) (n : ℕ) : n.succ • a = 0 → a = 0

  An additive group is torsion-free if the only element with non-trivial torsion is the identity element.

instance LeanPool.Polylean.instAddTorsionFreeInt : AddTorsionFree ℤ

ℤ is torsion-free, since it is an integral domain.

instance LeanPool.Polylean.instAddTorsionFreeProd {A : Type u_1} {B : Type u_2} [AddGroup A] [AddGroup B] [AddTorsionFree A] [AddTorsionFree B] : AddTorsionFree (A × B)

The product of torsion-free additive groups is torsion-free.

Step 1: Defining the square of an element of P.

@[reducible]

def LeanPool.Polylean.P.sq : P → K

The function taking an element of P to its square, which lies in the kernel K.

Equations

• LeanPool.Polylean.P.sq ((p, q, r), ⟨0, ⋯⟩, ⟨0, ⋯⟩) = (p + p, q + q, r + r)
• LeanPool.Polylean.P.sq ((fst, q, snd), ⟨0, ⋯⟩, ⟨1, ⋯⟩) = (0, q + q + 1, 0)
• LeanPool.Polylean.P.sq ((p, fst, snd), ⟨1, ⋯⟩, ⟨0, ⋯⟩) = (p + p + 1, 0, 0)
• LeanPool.Polylean.P.sq ((fst, fst_1, r), ⟨1, ⋯⟩, ⟨1, ⋯⟩) = (0, 0, r + r + 1)

@[simp]

theorem LeanPool.Polylean.sq_square (g : P) : g * g = (g.sq, Q.e)

A proof that the function sq indeed takes an element of P to its square in K.

Step 2: Proving that K (= ℤ³) is torsion-free.

instance LeanPool.Polylean.K.torsionFree : AddTorsionFree K

The kernel ℤ³ is torsion-free.

Step 3: Showing that no element of P has order precisely two.

Some basic lemmas about integers needed to prove facts about P.

theorem LeanPool.Polylean.Int.add_twice_eq_mul_two {a : ℤ} : a + a = a * 2

theorem LeanPool.Polylean.Int.odd_ne_zero (a : ℤ) : ¬a + a + 1 = 0

No odd integer is zero.

theorem LeanPool.Polylean.Int.zero_of_twice_zero (a : ℤ) : a + a = 0 → a = 0

If the sum of an integer with itself is zero, then the integer is itself zero.

theorem LeanPool.Polylean.square_free {g : P} : g * g = 1 → g = 1

The only element of P with order dividing 2 is the identity.

Step 4: Showing square powers of torsion elements are trivial.

theorem LeanPool.Polylean.torsion_implies_square_torsion {G : Type u_1} [Group G] (g : G) (n : ℕ) (g_tor : g ^ n = 1) : (g ^ 2) ^ n = 1

If g is a torsion element of a group, then so is g ^ 2.

Step 5: Putting the facts together.

instance LeanPool.Polylean.P.torsionFree : TorsionFree P

P is torsion-free.