Signature uniqueness for flat two-letter HNN words

This file develops the coefficient comparison behind the uniqueness of the color/sign signature of MultipleHNNFlat.ReducedWord. The proof first compares the outer HNN normal forms and then recursively compares the inner normal forms of their coefficients. Multiplication by an element of the original base changes only an end coefficient of an inner reduced word, and hence does not change its stable-letter signature.

@[reducible, inline]

abbrev Undecidability.MultipleHNNFlatUniqueness.InnerWord {G : Type u_1} [Group G] (A B : Subgroup G) : Type u_1

A reduced normal word in the inner single HNN extension.

Equations

• Undecidability.MultipleHNNFlatUniqueness.InnerWord A B = HNNExtension.NormalWord.ReducedWord G A B

Right multiplication of a single-HNN reduced word

def Undecidability.MultipleHNNFlatUniqueness.rightMulList {G : Type u_1} [Group G] : List (ℤˣ × G) → G → List (ℤˣ × G)

Multiply the last coefficient of a syllable list on the right.

Equations

• Undecidability.MultipleHNNFlatUniqueness.rightMulList [] x✝ = []
• Undecidability.MultipleHNNFlatUniqueness.rightMulList [x_2] x✝ = [(x_2.1, x_2.2 * x✝)]
• Undecidability.MultipleHNNFlatUniqueness.rightMulList (x_2 :: y :: rest) x✝ = x_2 :: Undecidability.MultipleHNNFlatUniqueness.rightMulList (y :: rest) x✝

theorem Undecidability.MultipleHNNFlatUniqueness.rightMulList_map_fst {G : Type u_1} [Group G] (l : List (ℤˣ × G)) (g : G) : List.map Prod.fst (rightMulList l g) = List.map Prod.fst l

theorem Undecidability.MultipleHNNFlatUniqueness.rightMulList_chain {G : Type u_1} [Group G] (A B : Subgroup G) (l : List (ℤˣ × G)) (hchain : List.IsChain (fun (a b : ℤˣ × G) => a.2 ∈ HNNExtension.toSubgroup A B a.1 → a.1 = b.1) l) (g : G) : List.IsChain (fun (a b : ℤˣ × G) => a.2 ∈ HNNExtension.toSubgroup A B a.1 → a.1 = b.1) (rightMulList l g)

def Undecidability.MultipleHNNFlatUniqueness.rightMul {G : Type u_1} [Group G] (A B : Subgroup G) (w : InnerWord A B) (g : G) : InnerWord A B

Right-multiply an inner HNN normal word by a base-group element.

Equations

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

theorem Undecidability.MultipleHNNFlatUniqueness.rightMul_map_fst {G : Type u_1} [Group G] (A B : Subgroup G) (w : InnerWord A B) (g : G) : List.map Prod.fst (rightMul A B w g).toList = List.map Prod.fst w.toList

theorem Undecidability.MultipleHNNFlatUniqueness.rightMulList_prod {G : Type u_1} [Group G] (A B : Subgroup G) (phi : ↥A ≃* ↥B) (l : List (ℤˣ × G)) (g : G) (hne : l ≠ []) : (List.map (fun (x : ℤˣ × G) => HNNExtension.t ^ ↑x.1 * HNNExtension.of x.2) (rightMulList l g)).prod = (List.map (fun (x : ℤˣ × G) => HNNExtension.t ^ ↑x.1 * HNNExtension.of x.2) l).prod * HNNExtension.of g

theorem Undecidability.MultipleHNNFlatUniqueness.rightMul_prod {G : Type u_1} [Group G] (A B : Subgroup G) (phi : ↥A ≃* ↥B) (w : InnerWord A B) (g : G) : HNNExtension.NormalWord.ReducedWord.prod phi (rightMul A B w g) = HNNExtension.NormalWord.ReducedWord.prod phi w * HNNExtension.of g

theorem Undecidability.MultipleHNNFlatUniqueness.inner_signs_eq_of_inv_mul_mem_range {G : Type u_1} [Group G] (A B : Subgroup G) (phi : ↥A ≃* ↥B) (w₁ w₂ : InnerWord A B) (hmem : (HNNExtension.NormalWord.ReducedWord.prod phi w₁)⁻¹ * HNNExtension.NormalWord.ReducedWord.prod phi w₂ ∈ HNNExtension.of.range) : List.map Prod.fst w₁.toList = List.map Prod.fst w₂.toList

Right multiplication by an embedded base element preserves the complete stable-sign list of a reduced word.

Coefficient transport in the outer HNN extension

def Undecidability.MultipleHNNFlatUniqueness.innerLeftMul {G : Type u_1} [Group G] (A B : Subgroup G) (g : G) (w : InnerWord A B) : InnerWord A B

Left-multiply the initial coefficient of an inner HNN normal word.

Equations

• Undecidability.MultipleHNNFlatUniqueness.innerLeftMul A B g w = { head := g * w.head, toList := w.toList, chain := ⋯ }

theorem Undecidability.MultipleHNNFlatUniqueness.mapped_toSubgroup_le_stageOne_range {G : Type u_1} [Group G] (A B : Subgroup G) (phi : ↥A ≃* ↥B) (u : ℤˣ) : HNNExtension.toSubgroup (MultipleHNN.MappedA A B phi) (MultipleHNN.MappedB A B phi) u ≤ (MultipleHNN.stageOneOf A B phi).range

theorem Undecidability.MultipleHNNFlatUniqueness.of_subgroup_mul_t_zpow {K : Type u_2} [Group K] (C D : Subgroup K) (psi : ↥C ≃* ↥D) (u : ℤˣ) (a : ↥(HNNExtension.toSubgroup C D (-u))) : HNNExtension.of ↑a * HNNExtension.t ^ ↑u = HNNExtension.t ^ ↑u * HNNExtension.of ↑((HNNExtension.toSubgroupEquiv psi (-u)) a)

Moving an element of the subgroup on the left of a stable letter across that letter. This unit-valued version packages the two usual HNN relations.

def Undecidability.MultipleHNNFlatUniqueness.outerTail {G : Type u_1} [Group G] (A B : Subgroup G) (phi : ↥A ≃* ↥B) (p : MultipleHNN.Syllable A B) (rest : List (MultipleHNN.Syllable A B)) (hchain : List.IsChain (fun (a b : ℤˣ × HNNExtension G A B phi) => a.2 ∈ HNNExtension.toSubgroup (MultipleHNN.MappedA A B phi) (MultipleHNN.MappedB A B phi) a.1 → a.1 = b.1) (List.map (fun (q : MultipleHNN.Syllable A B) => (q.1, HNNExtension.NormalWord.ReducedWord.prod phi q.2)) (p :: rest))) : MultipleHNN.ReducedWord A B phi

The outer reduced tail beginning at the selected nested syllable.

Equations

• Undecidability.MultipleHNNFlatUniqueness.outerTail A B phi p rest hchain = { head := p.2, toList := rest, chain := ⋯ }

def Undecidability.MultipleHNNFlatUniqueness.nestedLeftBase {G : Type u_1} [Group G] (A B : Subgroup G) (phi : ↥A ≃* ↥B) (g : G) (w : MultipleHNN.ReducedWord A B phi) : MultipleHNN.ReducedWord A B phi

Left-multiply the initial base coefficient of a nested HNN normal word.

Equations

• Undecidability.MultipleHNNFlatUniqueness.nestedLeftBase A B phi g w = { head := Undecidability.MultipleHNNFlatUniqueness.innerLeftMul A B g w.head, toList := w.toList, chain := ⋯ }

@[simp]

theorem Undecidability.MultipleHNNFlatUniqueness.nestedLeftBase_signature {G : Type u_1} [Group G] (A B : Subgroup G) (phi : ↥A ≃* ↥B) (g : G) (w : MultipleHNN.ReducedWord A B phi) : MultipleHNNFlat.nestedSignature A B phi (nestedLeftBase A B phi g w) = MultipleHNNFlat.nestedSignature A B phi w

theorem Undecidability.MultipleHNNFlatUniqueness.nestedLeftBase_eval {G : Type u_1} [Group G] (A B : Subgroup G) (phi : ↥A ≃* ↥B) (g : G) (w : MultipleHNN.ReducedWord A B phi) : MultipleHNN.ReducedWord.eval A B phi (nestedLeftBase A B phi g w) = (MultipleHNN.baseEmbedding A B phi) g * MultipleHNN.ReducedWord.eval A B phi w

Uniqueness of the nested signature

theorem Undecidability.MultipleHNNFlatUniqueness.nestedSignature_eq_of_eval_eq {G : Type u_1} [Group G] (A B : Subgroup G) (phi : ↥A ≃* ↥B) (w₁ w₂ : MultipleHNN.ReducedWord A B phi) (heval : MultipleHNN.ReducedWord.eval A B phi w₁ = MultipleHNN.ReducedWord.eval A B phi w₂) : MultipleHNNFlat.nestedSignature A B phi w₁ = MultipleHNNFlat.nestedSignature A B phi w₂

Equal evaluations of nested reduced words have identical interleaved color/sign signatures.

theorem Undecidability.MultipleHNNFlatUniqueness.signature_eq_of_eval_eq {G : Type u_1} [Group G] (A B : Subgroup G) (phi : ↥A ≃* ↥B) (w₁ w₂ : MultipleHNNFlat.ReducedWord A B) (heval : MultipleHNNFlat.eval A B phi w₁ = MultipleHNNFlat.eval A B phi w₂) : MultipleHNNFlat.signature A B w₁ = MultipleHNNFlat.signature A B w₂

The color/sign signature is a complete invariant of the stable letters in a flat reduced word. In particular, equality cannot change a sign, insert a stable letter, or change the interleaving of the two colors.