Source: ProCGroups.ReidemeisterSchreier.Schreier
1import Mathlib.Data.Nat.Basic
3/-!
4# Reidemeister Schreier / Schreier
6This module formalizes Schreier generators and rewriting.
7-/
9namespace ReidemeisterSchreier
10namespace Schreier
12/-- The Schreier rank transform \(T(r,i)=1+i(r-1)\), with the rank-zero convention. -/
13def rankTransform (r i : ℕ) : ℕ :=
14 if r = 0 then 0 else 1 + i * (r - 1)
16/-- Schreier's rank transform satisfies the displayed cardinal-arithmetic identity. -/
17@[simp] theorem rankTransform_zero_left (i : ℕ) : rankTransform 0 i = 0 := by
18 simp only [rankTransform, ↓reduceIte]
20/-- Schreier's rank transform satisfies the displayed cardinal-arithmetic identity. -/
21@[simp] theorem rankTransform_succ (r i : ℕ) : rankTransform (r + 1) i = 1 + i * r := by
22 simp only [rankTransform, Nat.add_eq_zero_iff, Nat.succ_ne_self, and_false, ↓reduceIte,
23 Nat.add_one_sub_one]
25/-- Schreier's rank transform satisfies the displayed cardinal-arithmetic identity. -/
26@[simp] theorem rankTransform_one_left (i : ℕ) : rankTransform 1 i = 1 := by
27 simp only [rankTransform, Nat.succ_ne_self, ↓reduceIte, Nat.sub_self, Nat.mul_zero, Nat.add_zero]
29/-- For nonzero \(r\), the Schreier rank transform is \(1+i(r-1)\). -/
30theorem rankTransform_eq_one_add {r i : ℕ} (hr : r ≠ 0) :
31 rankTransform r i = 1 + i * (r - 1) := by
32 simp only [rankTransform, hr, ↓reduceIte]
34/-- Multiplying subgroup indices composes the Schreier rank transform. -/
35theorem rankTransform_mul_index (r i j : ℕ) :
36 rankTransform (rankTransform r i) j = rankTransform r (i * j) := by
37 cases r with
38 | zero =>
39 simp only [rankTransform, ↓reduceIte]
40 | succ r =>
41 simp only [rankTransform, Nat.add_eq_zero_iff, Nat.succ_ne_self, and_false, ↓reduceIte,
42 Nat.add_one_sub_one, false_and, Nat.add_sub_cancel_left, Nat.mul_left_comm, Nat.mul_comm]
44/-- The Schreier rank transform is monotone in the rank variable. -/
45theorem rankTransform_mono_left {r s i : ℕ} (hrs : r ≤ s) :
46 rankTransform r i ≤ rankTransform s i := by
47 cases s with
48 | zero =>
49 have hr : r = 0 := Nat.eq_zero_of_le_zero hrs
50 subst hr
51 simp only [rankTransform_zero_left, le_refl]
52 | succ s =>
53 cases r with
54 | zero =>
55 simp only [rankTransform_zero_left, rankTransform_succ, Nat.zero_le]
56 | succ r =>
57 simpa only [rankTransform_succ] using
58 Nat.add_le_add_left (Nat.mul_le_mul_left i (Nat.succ_le_succ_iff.mp hrs)) 1
60end Schreier
61end ReidemeisterSchreier