FenchelNielsenZomorrodian.Discrete.Singerman.FreeGroupWords
theorem list_ofFn_one_add {α : Type*} {n : ℕ} (f : Fin (1 + n) → α) :
List.ofFn f =
f ⟨0, by omega⟩ ::
List.ofFn (fun j : Fin n => f ⟨1 + j.val, by omega⟩)A finite list indexed by \(\mathrm{Fin}(1+n)\) splits into its first entry and the remaining \(n\) entries.
Show proof
by
rw [List.ofFn_congr (show 1 + n = n + 1 by omega)]
rw [List.ofFn_succ]
simp only [Fin.cast_zero, Fin.mk_zero', List.cons.injEq, List.ofFn_inj, true_and]
funext j
apply congrArg f
ext
simp only [Fin.val_cast, Fin.val_succ]
omegaProof. Use the Fenchel--Nielsen--Zomorrodian presentation with elliptic generators of prescribed periods, handle and boundary generators, and the defining product relation. The proof checks the images of the named generators and verifies that every presentation relator is preserved in the target quotient, abelianization, or reduced presentation. For period-class statements, the relevant lcm or gcd divisibility is converted into a scalar multiple of the abelianized elliptic generator, and the defining period relation makes that multiple vanish. Schreier-rewriting steps are performed with the chosen transversal; the letter-by-letter formula sends each relator to the corresponding canonical word in the subgroup presentation. Because the generator images satisfy all defining relations and agree with the displayed quotient data, the presentation universal property yields the asserted identity. The reductions preserve the ordering of the canonical generators and the period data, so the image of every relator can be read directly in the target presentation. In the abelianized arguments, commutators vanish and only the period coefficients remain. The divisibility or lcm calculation then gives the required scalar multiple, while the presentation relation supplies its vanishing. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked. For the Fenchel--Nielsen--Zomorrodian relations, the period calculation checks that each elliptic generator has image of the prescribed order, and the product relation is verified by multiplying the images in the stated order. Divisibility, lcm, or gcd hypotheses are used precisely to make the period relators vanish in the target quotient.
□theorem list_ofFn_two_add {α : Type*} {n : ℕ} (f : Fin (2 + n) → α) :
List.ofFn f =
f ⟨0, by omega⟩ :: f ⟨1, by omega⟩ ::
List.ofFn (fun j : Fin n => f ⟨2 + j.val, by omega⟩)A finite list indexed by \(\mathrm{Fin}(2+n)\) splits into its first two entries and the remaining \(n\) entries.
Show proof
by
rw [List.ofFn_congr (show 2 + n = (1 + n) + 1 by omega)]
rw [List.ofFn_succ]
rw [List.ofFn_congr (show 1 + n = n + 1 by omega)]
rw [List.ofFn_succ]
simp only [Fin.cast_zero, Fin.succ_zero_eq_one', Fin.mk_zero', List.cons.injEq,
List.ofFn_inj, true_and]
constructor
· apply congrArg f
ext
simp only [Fin.val_cast, Fin.coe_ofNat_eq_mod, Nat.mod_succ_eq_iff_lt, Nat.succ_eq_add_one,
lt_add_iff_pos_left, add_pos_iff, zero_lt_one, true_or]
· funext j
apply congrArg f
ext
simp only [Fin.val_cast, Fin.val_succ]
omegaProof. Use the Fenchel--Nielsen--Zomorrodian presentation with elliptic generators of prescribed periods, handle and boundary generators, and the defining product relation. The proof checks the images of the named generators and verifies that every presentation relator is preserved in the target quotient, abelianization, or reduced presentation. For period-class statements, the relevant lcm or gcd divisibility is converted into a scalar multiple of the abelianized elliptic generator, and the defining period relation makes that multiple vanish. Schreier-rewriting steps are performed with the chosen transversal; the letter-by-letter formula sends each relator to the corresponding canonical word in the subgroup presentation. Because the generator images satisfy all defining relations and agree with the displayed quotient data, the presentation universal property yields the asserted identity. The reductions preserve the ordering of the canonical generators and the period data, so the image of every relator can be read directly in the target presentation. In the abelianized arguments, commutators vanish and only the period coefficients remain. The divisibility or lcm calculation then gives the required scalar multiple, while the presentation relation supplies its vanishing. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked. For the Fenchel--Nielsen--Zomorrodian relations, the period calculation checks that each elliptic generator has image of the prescribed order, and the product relation is verified by multiplying the images in the stated order. Divisibility, lcm, or gcd hypotheses are used precisely to make the period relators vanish in the target quotient.
□theorem freeGroup_of_pow_ne_one {X : Type*}
(x : X) {n : ℕ} (hn : n ≠ 0) :
(FreeGroup.of x : FreeGroup X) ^ n ≠ 1A nonzero power of a free generator is nontrivial.
Show proof
by
classical
intro h
let χ : X → Multiplicative ℤ :=
fun y => if y = x then Multiplicative.ofAdd (1 : ℤ) else 1
have hmap := congrArg (FreeGroup.lift χ) h
have hn0 : n = 0 := by
simpa [χ, map_pow] using hmap
exact hn hn0Proof. Use the Fenchel--Nielsen--Zomorrodian presentation with elliptic generators of prescribed periods, handle and boundary generators, and the defining product relation. The proof checks the images of the named generators and verifies that every presentation relator is preserved in the target quotient, abelianization, or reduced presentation. Because the generator images satisfy all defining relations and agree with the displayed quotient data, the presentation universal property yields the asserted identity. The reductions preserve the ordering of the canonical generators and the period data, so the image of every relator can be read directly in the target presentation. In the abelianized arguments, commutators vanish and only the period coefficients remain. The divisibility or lcm calculation then gives the required scalar multiple, while the presentation relation supplies its vanishing. Every map between the reduced presentations is determined by the images of elliptic, handle, and boundary generators. The period and product relators are checked explicitly after applying those images. Therefore the constructed quotient or abelianized map is well defined and has the claimed effect on the named generator or class. For the Fenchel--Nielsen--Zomorrodian relations, the period calculation checks that each elliptic generator has image of the prescribed order, and the product relation is verified by multiplying the images in the stated order. Divisibility, lcm, or gcd hypotheses are used precisely to make the period relators vanish in the target quotient. Consequently the two expressions have the same determining coordinates, and the defining extensionality principle for the inverse-limit, quotient, or presentation construction gives the claim in the statement.
□private theorem freeGroup_isReduced_pow_mul_of_mul_pow_inv_word {X : Type*}
{x y : X} (hxy : x ≠ y) (a b : ℕ) :
FreeGroup.IsReduced
(List.replicate a (x, true) ++ [(y, true)] ++ List.replicate b (x, false))The explicit word with \(a\) copies of \(x\), then \(y\), then \(b\) copies of \(x^{-1}\), is reduced when \(x e y\).
Show proof
by
apply List.IsChain.append
· apply List.IsChain.append
· exact List.isChain_replicate_of_rel a (by intro _; rfl)
· simp only [List.IsChain.singleton]
· intro u hu v hv huv
simp only [List.head?_cons, Option.mem_def, Option.some.injEq] at hv
subst v
by_cases ha : a = 0
· simp only [ha, List.replicate_zero, List.getLast?_nil, Option.mem_def, reduceCtorEq] at hu
· have hlast : u = (x, true) := by
simpa [List.getLast?_replicate, ha] using hu.symm
subst u
exact False.elim (hxy huv)
· exact List.isChain_replicate_of_rel b (by intro _; rfl)
· intro u hu v hv huv
by_cases hb : b = 0
· simp only [hb, List.replicate_zero, List.head?_nil, Option.mem_def, reduceCtorEq] at hv
· have hvx : v = (x, false) := by
simpa [List.head?_replicate, hb] using hv.symm
subst v
have huy : u = (y, true) := by
simpa using hu.symm
subst u
exact False.elim (hxy huv.symm)Proof. Use the Fenchel--Nielsen--Zomorrodian presentation with elliptic generators of prescribed periods, handle and boundary generators, and the defining product relation. The proof checks the images of the named generators and verifies that every presentation relator is preserved in the target quotient, abelianization, or reduced presentation. For period-class statements, the relevant lcm or gcd divisibility is converted into a scalar multiple of the abelianized elliptic generator, and the defining period relation makes that multiple vanish. Schreier-rewriting steps are performed with the chosen transversal; the letter-by-letter formula sends each relator to the corresponding canonical word in the subgroup presentation. Because the generator images satisfy all defining relations and agree with the displayed quotient data, the presentation universal property yields the asserted identity. The reductions preserve the ordering of the canonical generators and the period data, so the image of every relator can be read directly in the target presentation. In the abelianized arguments, commutators vanish and only the period coefficients remain. The divisibility or lcm calculation then gives the required scalar multiple, while the presentation relation supplies its vanishing. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked. For the Fenchel--Nielsen--Zomorrodian relations, the period calculation checks that each elliptic generator has image of the prescribed order, and the product relation is verified by multiplying the images in the stated order. Divisibility, lcm, or gcd hypotheses are used precisely to make the period relators vanish in the target quotient.
□theorem freeGroup_toWord_pow_mul_of_mul_pow_inv {X : Type*} [DecidableEq X]
{x y : X} (hxy : x ≠ y) (a b : ℕ) :
FreeGroup.toWord
((FreeGroup.of x : FreeGroup X) ^ a * FreeGroup.of y *
((FreeGroup.of x : FreeGroup X) ^ b)⁻¹) =
List.replicate a (x, true) ++ [(y, true)] ++ List.replicate b (x, false)The reduced word for \(x^a y x^{-b}\) is the explicit list of \(a\) positive \(x\) letters, one positive \(y\), and \(b\) negative \(x\) letters.
Show proof
by
let L := List.replicate a (x, true) ++ [(y, true)] ++ List.replicate b (x, false)
have hmk :
(FreeGroup.of x : FreeGroup X) ^ a * FreeGroup.of y *
((FreeGroup.of x : FreeGroup X) ^ b)⁻¹ =
FreeGroup.mk L := by
simp only [FreeGroup.of, FreeGroup.pow_mk, List.flatten_replicate_singleton, FreeGroup.mul_mk,
FreeGroup.inv_mk, FreeGroup.invRev, List.map_replicate, Bool.not_true, List.reverse_replicate, List.append_assoc,
List.cons_append, List.nil_append, L]
rw [hmk, FreeGroup.toWord_mk]
exact (freeGroup_isReduced_pow_mul_of_mul_pow_inv_word hxy a b).reduce_eqProof. Use the Fenchel--Nielsen--Zomorrodian presentation with elliptic generators of prescribed periods, handle and boundary generators, and the defining product relation. The proof checks the images of the named generators and verifies that every presentation relator is preserved in the target quotient, abelianization, or reduced presentation. For period-class statements, the relevant lcm or gcd divisibility is converted into a scalar multiple of the abelianized elliptic generator, and the defining period relation makes that multiple vanish. Schreier-rewriting steps are performed with the chosen transversal; the letter-by-letter formula sends each relator to the corresponding canonical word in the subgroup presentation. Because the generator images satisfy all defining relations and agree with the displayed quotient data, the presentation universal property yields the asserted identity. The reductions preserve the ordering of the canonical generators and the period data, so the image of every relator can be read directly in the target presentation. In the abelianized arguments, commutators vanish and only the period coefficients remain. The divisibility or lcm calculation then gives the required scalar multiple, while the presentation relation supplies its vanishing. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked. For the Fenchel--Nielsen--Zomorrodian relations, the period calculation checks that each elliptic generator has image of the prescribed order, and the product relation is verified by multiplying the images in the stated order. Divisibility, lcm, or gcd hypotheses are used precisely to make the period relators vanish in the target quotient.
□private theorem freeGroup_pow_mul_of_mul_pow_inv_word_initialLength {X : Type*} [DecidableEq X]
{x y : X} (hxy : x ≠ y) (a b : ℕ) :
(List.takeWhile (fun q : X × Bool => q = (x, true))
(List.replicate a (x, true) ++ [(y, true)] ++ List.replicate b (x, false))).length =
aIn the explicit reduced word for \(x^a y x^{-b}\), the initial run of positive \(x\) letters has length \(a\).
Show proof
by
have hyx : (y, true) ≠ (x, true) := by
intro h
exact hxy (by cases h; rfl)
induction a with
| zero => simp [hyx]
| succ a _ih => simp [List.replicate_succ, hyx]Proof. Use the Fenchel--Nielsen--Zomorrodian presentation with elliptic generators of prescribed periods, handle and boundary generators, and the defining product relation. The proof checks the images of the named generators and verifies that every presentation relator is preserved in the target quotient, abelianization, or reduced presentation. For period-class statements, the relevant lcm or gcd divisibility is converted into a scalar multiple of the abelianized elliptic generator, and the defining period relation makes that multiple vanish. Schreier-rewriting steps are performed with the chosen transversal; the letter-by-letter formula sends each relator to the corresponding canonical word in the subgroup presentation. Because the generator images satisfy all defining relations and agree with the displayed quotient data, the presentation universal property yields the asserted identity. The reductions preserve the ordering of the canonical generators and the period data, so the image of every relator can be read directly in the target presentation. In the abelianized arguments, commutators vanish and only the period coefficients remain. The divisibility or lcm calculation then gives the required scalar multiple, while the presentation relation supplies its vanishing. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked. For the Fenchel--Nielsen--Zomorrodian relations, the period calculation checks that each elliptic generator has image of the prescribed order, and the product relation is verified by multiplying the images in the stated order. Divisibility, lcm, or gcd hypotheses are used precisely to make the period relators vanish in the target quotient.
□theorem freeGroup_pow_mul_of_mul_pow_inv_left_exponent_eq_of_eq {X : Type*}
{x y : X} (hxy : x ≠ y) {a b c d : ℕ}
(h :
(FreeGroup.of x : FreeGroup X) ^ a * FreeGroup.of y *
((FreeGroup.of x : FreeGroup X) ^ b)⁻¹ =
(FreeGroup.of x : FreeGroup X) ^ c * FreeGroup.of y *
((FreeGroup.of x : FreeGroup X) ^ d)⁻¹) :
a = cEquality of words \(x^a y x^{-b}=x^c y x^{-d}\) with \(x e y\) forces \(a=c\).
Show proof
by
classical
have hwords := congrArg (fun w : FreeGroup X => FreeGroup.toWord w) h
change
FreeGroup.toWord
((FreeGroup.of x : FreeGroup X) ^ a * FreeGroup.of y *
((FreeGroup.of x : FreeGroup X) ^ b)⁻¹) =
FreeGroup.toWord
((FreeGroup.of x : FreeGroup X) ^ c * FreeGroup.of y *
((FreeGroup.of x : FreeGroup X) ^ d)⁻¹) at hwords
rw [freeGroup_toWord_pow_mul_of_mul_pow_inv hxy a b,
freeGroup_toWord_pow_mul_of_mul_pow_inv hxy c d] at hwords
have htake := congrArg
(fun L : List (X × Bool) =>
(List.takeWhile (fun q : X × Bool => q = (x, true)) L).length) hwords
change
(List.takeWhile (fun q : X × Bool => q = (x, true))
(List.replicate a (x, true) ++ [(y, true)] ++ List.replicate b (x, false))).length =
(List.takeWhile (fun q : X × Bool => q = (x, true))
(List.replicate c (x, true) ++ [(y, true)] ++ List.replicate d (x, false))).length at htake
rw [freeGroup_pow_mul_of_mul_pow_inv_word_initialLength hxy a b,
freeGroup_pow_mul_of_mul_pow_inv_word_initialLength hxy c d] at htake
exact htakeProof. Unfold the named Fenchel--Nielsen reduction, cyclic-Schreier word, or total-relation definition. The equality or membership follows by evaluating the relevant generator branch, simplifying the period or product formula, and using that normal closures are closed under products, inverses, and conjugation when a relator membership is involved.
□