A two-stable-letter form of Britton's lemma

This file packages an iterated HNN extension in which both stable letters identify the same pair of subgroups of a base group. At the second stage the associated subgroups are, necessarily, their images in the first HNN extension.

The type ReducedWord records a reduced word for every coefficient in the first HNN extension, together with the usual reducedness condition for the outer HNN extension. The main theorem eval_not_mem_base says that a reduced word containing either stable letter cannot represent an element of the original base group. In particular, such a word is nontrivial.

The construction is independent of Borisov's concrete base group and can be reused for the two-stable-letter stage of his group G₀.

@[reducible, inline]

abbrev Undecidability.MultipleHNN.StageOne {G : Type u_1} [Group G] (A B : Subgroup G) (phi : ↥A ≃* ↥B) : Type u_1

The first HNN extension, with its first stable letter.

Equations

• Undecidability.MultipleHNN.StageOne A B phi = HNNExtension G A B phi

def Undecidability.MultipleHNN.stageOneOf {G : Type u_1} [Group G] (A B : Subgroup G) (phi : ↥A ≃* ↥B) : G →* StageOne A B phi

The canonical embedding of the original base in the first stage.

Equations

• Undecidability.MultipleHNN.stageOneOf A B phi = HNNExtension.of

@[reducible, inline]

abbrev Undecidability.MultipleHNN.MappedA {G : Type u_1} [Group G] (A B : Subgroup G) (phi : ↥A ≃* ↥B) : Subgroup (StageOne A B phi)

The first associated subgroup transported to the first stage.

Equations

• Undecidability.MultipleHNN.MappedA A B phi = Subgroup.map (Undecidability.MultipleHNN.stageOneOf A B phi) A

@[reducible, inline]

abbrev Undecidability.MultipleHNN.MappedB {G : Type u_1} [Group G] (A B : Subgroup G) (phi : ↥A ≃* ↥B) : Subgroup (StageOne A B phi)

The second associated subgroup transported to the first stage.

Equations

• Undecidability.MultipleHNN.MappedB A B phi = Subgroup.map (Undecidability.MultipleHNN.stageOneOf A B phi) B

noncomputable def Undecidability.MultipleHNN.mappedEquiv {G : Type u_1} [Group G] (A B : Subgroup G) (phi : ↥A ≃* ↥B) : ↥(MappedA A B phi) ≃* ↥(MappedB A B phi)

The equivalence of the mapped associated subgroups induced by phi.

Equations

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

@[reducible, inline]

abbrev Undecidability.MultipleHNN.Extension {G : Type u_1} [Group G] (A B : Subgroup G) (phi : ↥A ≃* ↥B) : Type u_1

The iterated HNN extension, carrying two stable letters.

Equations

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

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

The canonical embedding of the first stage in the two-letter extension.

Equations

• Undecidability.MultipleHNN.stageTwoOf A B phi = HNNExtension.of

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

The canonical embedding of the original base in the two-letter extension.

Equations

• Undecidability.MultipleHNN.baseEmbedding A B phi = (Undecidability.MultipleHNN.stageTwoOf A B phi).comp (Undecidability.MultipleHNN.stageOneOf A B phi)

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

The first stable letter, viewed in the iterated extension.

Equations

• Undecidability.MultipleHNN.firstStable A B phi = (Undecidability.MultipleHNN.stageTwoOf A B phi) HNNExtension.t

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

The second stable letter.

Equations

• Undecidability.MultipleHNN.secondStable A B phi = HNNExtension.t

@[reducible, inline]

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

A reduced word in the first HNN extension.

Equations

• Undecidability.MultipleHNN.InnerReducedWord A B = HNNExtension.NormalWord.ReducedWord G A B

@[reducible, inline]

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

An outer syllable consists of a sign for the second stable letter and a reduced coefficient in the first HNN extension.

Equations

• Undecidability.MultipleHNN.Syllable A B = (ℤˣ × Undecidability.MultipleHNN.InnerReducedWord A B)

structure Undecidability.MultipleHNN.ReducedWord {G : Type u_1} [Group G] (A B : Subgroup G) (phi : ↥A ≃* ↥B) : Type u_1

A nested reduced word for the two-stable-letter extension.

The inner words are already reduced with respect to the first stable letter. The chain field says that, after evaluating those coefficients, the outer word is reduced with respect to the second stable letter.

• head : InnerReducedWord A B

  The coefficient before the first occurrence of the second stable letter.

• toList : List (Syllable A B)

  The second-stable-letter syllables and their following coefficients.

• chain : List.IsChain (fun (a b : ℤˣ × HNNExtension G A B phi) => a.2 ∈ HNNExtension.toSubgroup (MappedA A B phi) (MappedB A B phi) a.1 → a.1 = b.1) (List.map (fun (p : Syllable A B) => (p.1, HNNExtension.NormalWord.ReducedWord.prod phi p.2)) self.toList)

  Britton reducedness for the outer HNN extension.

def Undecidability.MultipleHNN.ReducedWord.toOuter {G : Type u_1} [Group G] (A B : Subgroup G) (phi : ↥A ≃* ↥B) (w : ReducedWord A B phi) : HNNExtension.NormalWord.ReducedWord (StageOne A B phi) (MappedA A B phi) (MappedB A B phi)

Forget the nested description and obtain an ordinary reduced word for the outer HNN extension.

Equations

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

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

Evaluation of a nested reduced word in the iterated HNN extension.

Equations

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

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

The word contains the second stable letter.

Equations

• Undecidability.MultipleHNN.ReducedWord.ContainsSecond A B phi w = (w.toList ≠ [])

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

If the outer list is empty, the first stable letters in head are the stable letters occurring in the whole word. Together with ContainsSecond, this is the support condition needed by the generalized Britton lemma.

Equations

• Undecidability.MultipleHNN.ReducedWord.ContainsFirstInHead A B phi w = (w.head.toList ≠ [])

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

The nested word contains at least one of the two stable letters.

Equations

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

theorem Undecidability.MultipleHNN.ReducedWord.eval_not_mem_stageOne {G : Type u_1} [Group G] (A B : Subgroup G) (phi : ↥A ≃* ↥B) (w : ReducedWord A B phi) (hsecond : ContainsSecond A B phi w) : eval A B phi w ∉ (stageTwoOf A B phi).range

Outer Britton lemma: a reduced word containing the second stable letter does not lie in the embedded first-stage group.

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

Generalized two-stable-letter Britton lemma: a reduced word containing a stable letter does not represent an element of the original base group.

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

A reduced two-stable-letter word containing a stable letter is nontrivial.