Flat reduced words for a two-stable-letter HNN extension

This is the simultaneous-letter view of the iterated HNN extension in MultipleHNN.lean. It is designed for Borisov's Assertion IV: a flat word records which of the two stable letters occurs at every syllable. The local reducedness condition is the ordinary Britton condition whenever two adjacent syllables use the same stable letter.

structure Undecidability.MultipleHNNFlat.Syllable {G : Type u_1} : Type u_1

A stable-generator color, orientation, and following base-group coefficient.

• color : Fin 2

  The label selecting one of the two stable generators.

• sign : ℤˣ

  The orientation of the stable generator, represented by 1 or -1.

• coeff : G

  The base-group coefficient following the stable generator.

def Undecidability.MultipleHNNFlat.Rel {G : Type u_1} [Group G] (A B : Subgroup G) (x y : Syllable) : Prop

The condition excluding a Britton pinch between adjacent same-color syllables.

Equations

• Undecidability.MultipleHNNFlat.Rel A B x y = (x.color = y.color → x.coeff ∈ HNNExtension.toSubgroup A B x.sign → x.sign = y.sign)

structure Undecidability.MultipleHNNFlat.ReducedWord {G : Type u_1} [Group G] (A B : Subgroup G) : Type u_1

A flattened HNN word with an initial base coefficient and a reduced syllable chain.

• head : G

  The initial base-group coefficient of the flattened word.

• toList : List Syllable

  The sequence of stable-generator syllables and their following base coefficients.

• chain : List.IsChain (Rel A B) self.toList

def Undecidability.MultipleHNNFlat.signature {G : Type u_1} [Group G] (A B : Subgroup G) (w : ReducedWord A B) : List (Fin 2 × ℤˣ)

The stable-letter signature of a flat word. Base coefficients are discarded, while the color and sign of every stable letter are retained.

Equations

• Undecidability.MultipleHNNFlat.signature A B w = List.map (fun (s : Undecidability.MultipleHNNFlat.Syllable) => (s.color, s.sign)) w.toList

def Undecidability.MultipleHNNFlat.nestedSignature {G : Type u_1} [Group G] (A B : Subgroup G) (phi : ↥A ≃* ↥B) (w : MultipleHNN.ReducedWord A B phi) : List (Fin 2 × ℤˣ)

The same signature read from the nested two-stage normal form: first the initial block of first stable letters, then each second stable letter and the following block of first stable letters.

Equations

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

noncomputable def Undecidability.MultipleHNNFlat.stableLetter {G : Type u_1} [Group G] (A B : Subgroup G) (phi : ↥A ≃* ↥B) : Fin 2 → MultipleHNN.Extension A B phi

The stable generator in the iterated HNN extension with the selected color.

Equations

• Undecidability.MultipleHNNFlat.stableLetter A B phi 0 = Undecidability.MultipleHNN.firstStable A B phi
• Undecidability.MultipleHNNFlat.stableLetter A B phi 1 = Undecidability.MultipleHNN.secondStable A B phi

noncomputable def Undecidability.MultipleHNNFlat.eval {G : Type u_1} [Group G] (A B : Subgroup G) (phi : ↥A ≃* ↥B) (w : ReducedWord A B) : MultipleHNN.Extension A B phi

Evaluate the flattened word in the iterated HNN extension.

Equations

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

def Undecidability.MultipleHNNFlat.innerEmpty {G : Type u_1} [Group G] (A B : Subgroup G) (g : G) : MultipleHNN.InnerReducedWord A B

The inner reduced word containing only the supplied base-group coefficient.

Equations

• Undecidability.MultipleHNNFlat.innerEmpty A B g = { head := g, toList := [], chain := ⋯ }

def Undecidability.MultipleHNNFlat.Front {G : Type u_1} [Group G] (A B : Subgroup G) (phi : ↥A ≃* ↥B) (l : List Syllable) (w : MultipleHNN.ReducedWord A B phi) : Prop

The correspondence between the first flat syllables and the front of the nested normal form.

Equations

• One or more equations did not get rendered due to their size.
• Undecidability.MultipleHNNFlat.Front A B phi [] w = (w.head.toList = [] ∧ w.toList = [])

theorem Undecidability.MultipleHNNFlat.exists_nested_with_signature {G : Type u_1} [Group G] (A B : Subgroup G) (phi : ↥A ≃* ↥B) (w : ReducedWord A B) : ∃ (v : MultipleHNN.ReducedWord A B phi), MultipleHNN.ReducedWord.eval A B phi v = eval A B phi w ∧ nestedSignature A B phi v = signature A B w

Every flat reduced word has a nested reduced representative with the same evaluation and exactly the same color/sign signature.

theorem Undecidability.MultipleHNNFlat.eval_not_mem_stageOne_of_contains_color_one {G : Type u_1} [Group G] (A B : Subgroup G) (phi : ↥A ≃* ↥B) (w : ReducedWord A B) (hcolor : ∃ s ∈ w.toList, s.color = 1) : eval A B phi w ∉ (MultipleHNN.stageTwoOf A B phi).range

Color-sensitive flat Britton lemma. If a reduced flat word contains the second stable letter, its value cannot lie in the embedded first HNN stage.

theorem Undecidability.MultipleHNNFlat.eval_ne_one {G : Type u_1} [Group G] (A B : Subgroup G) (phi : ↥A ≃* ↥B) (w : ReducedWord A B) (hne : w.toList ≠ []) : eval A B phi w ≠ 1

A nonempty flat reduced word is nontrivial. This is the simultaneous two-stable-letter form of Britton's lemma.

A base-membership form of the flat Britton lemma

theorem Undecidability.MultipleHNNFlat.eval_not_mem_base {G : Type u_1} [Group G] (A B : Subgroup G) (phi : ↥A ≃* ↥B) (w : ReducedWord A B) (hne : w.toList ≠ []) : eval A B phi w ∉ (MultipleHNN.baseEmbedding A B phi).range

A nonempty flat reduced word cannot lie in the embedded original base. This strengthens eval_ne_one in the form needed for Borisov's subgroup intersection calculations.