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

ink

class TorsionFree (G : Type u_1) [inst : Group G] : Type

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

  torsionFree : ∀ (g : G) (n : ℕ), g ^ Nat.succ n = 1 → g = 1

The definition of a torsion-free group.

ink

class AddTorsionFree (A : Type u_1) [inst : AddGroup A] : Type

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

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

The definition of torsion-free additive groups.

ink

instance instAddTorsionFreeIntInstAddGroupInt : AddTorsionFree ℤ

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

Equations

• instAddTorsionFreeIntInstAddGroupInt = { torsionFree := instAddTorsionFreeIntInstAddGroupInt.proof_1 }

ink

instance instAddTorsionFreeProdInstAddGroupSum {A : Type u_1} {B : Type u_2} [inst : AddGroup A] [inst : AddGroup B] [inst : AddTorsionFree A] [inst : AddTorsionFree B] : AddTorsionFree (A × B)

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

Equations

• instAddTorsionFreeProdInstAddGroupSum = { torsionFree := (_ : ∀ (h : A × B) (n : ℕ), Nat.succ n • h = 0 → h = 0) }

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

ink

def P.sq : P → K

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

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem sq_square (g : P) : g * g = (P.sq g, 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.

ink

instance K.torsionFree : AddTorsionFree K

The kernel ℤ³ is torsion-free.

Equations

• K.torsionFree = inferInstance

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

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

ink

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

ink

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

No odd integer is zero.

ink

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

ink

theorem square_free {g : P} : g * g = 1 → g = 1

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

Step 4: Showing that if the n-th power of a group element is trivial, then so is that of its square.

ink

theorem torsion_implies_square_torsion {G : Type u_1} [inst : 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.

ink

instance P.torsionFree : TorsionFree P

P is torsion-free.

Equations

• P.torsionFree = { torsionFree := P.torsionFree.proof_1 }