Transporting HNN extensions across an equivalence of HNN data

@[reducible, inline]

noncomputable abbrev Undecidability.HNNLemmas.equivRangeOfInjective {G : Type u_1} [Group G] {H : Type u_2} [Group H] (f : H →* G) (hf : Function.Injective ⇑f) : H ≃* ↥f.range

An injective homomorphism identifies its domain with its range.

Equations

• Undecidability.HNNLemmas.equivRangeOfInjective f hf = MonoidHom.ofInjective hf

noncomputable def Undecidability.HNNLemmas.rangeEquiv {G : Type u_1} [Group G] {H : Type u_2} [Group H] (f g : H →* G) (hf : Function.Injective ⇑f) (hg : Function.Injective ⇑g) : ↥f.range ≃* ↥g.range

Two injectively parametrized subgroups with the same parameter group are canonically isomorphic.

Equations

• Undecidability.HNNLemmas.rangeEquiv f g hf hg = (MonoidHom.ofInjective hf).symm.trans (MonoidHom.ofInjective hg)

@[simp]

theorem Undecidability.HNNLemmas.rangeEquiv_apply_range {G : Type u_1} [Group G] {H : Type u_2} [Group H] (f g : H →* G) (hf : Function.Injective ⇑f) (hg : Function.Injective ⇑g) (x : H) : ↑((rangeEquiv f g hf hg) ⟨f x, ⋯⟩) = g x

def Undecidability.HNNLemmas.generatedWithStable {G : Type u_1} [Group G] {A B : Subgroup G} {phi : ↥A ≃* ↥B} (H : Subgroup G) : Subgroup (HNNExtension G A B phi)

The subgroup generated by an embedded subgroup and the stable letter.

Equations

• Undecidability.HNNLemmas.generatedWithStable H = Subgroup.closure (↑(Subgroup.map HNNExtension.of H) ∪ {HNNExtension.t})

def Undecidability.HNNLemmas.congrHom {G : Type u_1} [Group G] {A B : Subgroup G} {phi : ↥A ≃* ↥B} {G' : Type u_2} [Group G'] {A' B' : Subgroup G'} {φ' : ↥A' ≃* ↥B'} (e : G ≃* G') (eA : ↥A ≃* ↥A') (eB : ↥B ≃* ↥B') (hA : ∀ (a : ↥A), ↑(eA a) = e ↑a) (hB : ∀ (b : ↥B), ↑(eB b) = e ↑b) (hφ : ∀ (a : ↥A), eB (phi a) = φ' (eA a)) : HNNExtension G A B phi →* HNNExtension G' A' B' φ'

A homomorphism between HNN extensions induced by equivalences of the base groups and both associated subgroups. The three compatibility hypotheses say that the subgroup equivalences are the restrictions of the base equivalence and intertwine the attaching maps.

Equations

• Undecidability.HNNLemmas.congrHom e eA eB hA hB hφ = HNNExtension.lift (HNNExtension.of.comp e.toMonoidHom) HNNExtension.t ⋯

@[simp]

theorem Undecidability.HNNLemmas.congrHom_of {G : Type u_1} [Group G] {A B : Subgroup G} {phi : ↥A ≃* ↥B} {G' : Type u_2} [Group G'] {A' B' : Subgroup G'} {φ' : ↥A' ≃* ↥B'} (e : G ≃* G') (eA : ↥A ≃* ↥A') (eB : ↥B ≃* ↥B') (hA : ∀ (a : ↥A), ↑(eA a) = e ↑a) (hB : ∀ (b : ↥B), ↑(eB b) = e ↑b) (hφ : ∀ (a : ↥A), eB (phi a) = φ' (eA a)) (g : G) : (congrHom e eA eB hA hB hφ) (HNNExtension.of g) = HNNExtension.of (e g)

@[simp]

theorem Undecidability.HNNLemmas.congrHom_t {G : Type u_1} [Group G] {A B : Subgroup G} {phi : ↥A ≃* ↥B} {G' : Type u_2} [Group G'] {A' B' : Subgroup G'} {φ' : ↥A' ≃* ↥B'} (e : G ≃* G') (eA : ↥A ≃* ↥A') (eB : ↥B ≃* ↥B') (hA : ∀ (a : ↥A), ↑(eA a) = e ↑a) (hB : ∀ (b : ↥B), ↑(eB b) = e ↑b) (hφ : ∀ (a : ↥A), eB (phi a) = φ' (eA a)) : (congrHom e eA eB hA hB hφ) HNNExtension.t = HNNExtension.t

noncomputable def Undecidability.HNNLemmas.congr {G : Type u_1} [Group G] {A B : Subgroup G} {phi : ↥A ≃* ↥B} {G' : Type u_2} [Group G'] {A' B' : Subgroup G'} {φ' : ↥A' ≃* ↥B'} (e : G ≃* G') (eA : ↥A ≃* ↥A') (eB : ↥B ≃* ↥B') (hA : ∀ (a : ↥A), ↑(eA a) = e ↑a) (hB : ∀ (b : ↥B), ↑(eB b) = e ↑b) (hφ : ∀ (a : ↥A), eB (phi a) = φ' (eA a)) : HNNExtension G A B phi ≃* HNNExtension G' A' B' φ'

Isomorphic HNN data give isomorphic HNN extensions, with the stable letter fixed.

Equations

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

The first intersection calculation is most conveniently proved by comparing the ambient HNN extension with the HNN extension obtained by restricting both associated subgroups to H. The following definitions and lemmas implement that comparison. The construction and its basic API are public because the same restricted embedding is also used to prove exact subgroup presentations at later HNN stages; only the normal-form implementation remains private.

def Undecidability.HNNLemmas.restrictedA {G : Type u_1} [Group G] {A : Subgroup G} (H : Subgroup G) : Subgroup ↥H

Restrict the first associated subgroup to a base subgroup.

Equations

• Undecidability.HNNLemmas.restrictedA H = Subgroup.comap H.subtype A

def Undecidability.HNNLemmas.restrictedB {G : Type u_1} [Group G] {B : Subgroup G} (H : Subgroup G) : Subgroup ↥H

Restrict the second associated subgroup to a base subgroup.

Equations

• Undecidability.HNNLemmas.restrictedB H = Subgroup.comap H.subtype B

def Undecidability.HNNLemmas.restrictedPhi {G : Type u_1} [Group G] {A B : Subgroup G} {phi : ↥A ≃* ↥B} (H : Subgroup G) (hphi : ∀ (a : ↥A), ↑a ∈ H ↔ ↑(phi a) ∈ H) : ↥(restrictedA H) ≃* ↥(restrictedB H)

The associated-subgroup isomorphism restricted to a compatible base subgroup.

Equations

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

def Undecidability.HNNLemmas.restrictedEmbedding {G : Type u_1} [Group G] {A B : Subgroup G} {phi : ↥A ≃* ↥B} (H : Subgroup G) (hphi : ∀ (a : ↥A), ↑a ∈ H ↔ ↑(phi a) ∈ H) : HNNExtension (↥H) (restrictedA H) (restrictedB H) (restrictedPhi H hphi) →* HNNExtension G A B phi

The induced homomorphism from the restricted HNN extension into the original extension.

Equations

• Undecidability.HNNLemmas.restrictedEmbedding H hphi = HNNExtension.lift (HNNExtension.of.comp H.subtype) HNNExtension.t ⋯

@[simp]

theorem Undecidability.HNNLemmas.restrictedEmbedding_of {G : Type u_1} [Group G] {A B : Subgroup G} {phi : ↥A ≃* ↥B} (H : Subgroup G) (hphi : ∀ (a : ↥A), ↑a ∈ H ↔ ↑(phi a) ∈ H) (h : ↥H) : (restrictedEmbedding H hphi) (HNNExtension.of h) = HNNExtension.of ↑h

@[simp]

theorem Undecidability.HNNLemmas.restrictedEmbedding_t {G : Type u_1} [Group G] {A B : Subgroup G} {phi : ↥A ≃* ↥B} (H : Subgroup G) (hphi : ∀ (a : ↥A), ↑a ∈ H ↔ ↑(phi a) ∈ H) : (restrictedEmbedding H hphi) HNNExtension.t = HNNExtension.t

theorem Undecidability.HNNLemmas.restrictedEmbedding_range {G : Type u_1} [Group G] {A B : Subgroup G} {phi : ↥A ≃* ↥B} (H : Subgroup G) (hphi : ∀ (a : ↥A), ↑a ∈ H ↔ ↑(phi a) ∈ H) : (restrictedEmbedding H hphi).range = generatedWithStable H

def Undecidability.HNNLemmas.mapRestrictedReducedWord {G : Type u_1} [Group G] {A B : Subgroup G} (H : Subgroup G) (w : HNNExtension.NormalWord.ReducedWord (↥H) (restrictedA H) (restrictedB H)) : HNNExtension.NormalWord.ReducedWord G A B

Carry a reduced word of the restricted HNN extension into the original base group.

Equations

• Undecidability.HNNLemmas.mapRestrictedReducedWord H w = { head := ↑w.head, toList := List.map (fun (x : ℤˣ × ↥H) => (x.1, ↑x.2)) w.toList, chain := ⋯ }

theorem Undecidability.HNNLemmas.restrictedEmbedding_injective {G : Type u_1} [Group G] {A B : Subgroup G} {phi : ↥A ≃* ↥B} (H : Subgroup G) (hphi : ∀ (a : ↥A), ↑a ∈ H ↔ ↑(phi a) ∈ H) : Function.Injective ⇑(restrictedEmbedding H hphi)

The canonical homomorphism from an HNN extension restricted to a subgroup H into the ambient HNN extension is injective. This is the injectivity assertion in the restricted-HNN lemma: a non-base reduced word remains reduced in the ambient extension, while injectivity on the base is HNNExtension.of_injective.

noncomputable def Undecidability.HNNLemmas.restrictedEquivGeneratedWithStable {G : Type u_1} [Group G] {A B : Subgroup G} {phi : ↥A ≃* ↥B} (H : Subgroup G) (hphi : ∀ (a : ↥A), ↑a ∈ H ↔ ↑(phi a) ∈ H) : HNNExtension (↥H) (restrictedA H) (restrictedB H) (restrictedPhi H hphi) ≃* ↥(generatedWithStable H)

The restricted HNN extension, identified with the subgroup generated by the embedded copy of H and the ambient stable letter. This is the exact subgroup-presentation form of Lemma B.2 of the paper used by the compression stages.

Equations

• Undecidability.HNNLemmas.restrictedEquivGeneratedWithStable H hphi = (MonoidHom.ofInjective ⋯).trans (MulEquiv.subgroupCongr ⋯)

@[simp]

theorem Undecidability.HNNLemmas.restrictedEquivGeneratedWithStable_coe {G : Type u_1} [Group G] {A B : Subgroup G} {phi : ↥A ≃* ↥B} (H : Subgroup G) (hphi : ∀ (a : ↥A), ↑a ∈ H ↔ ↑(phi a) ∈ H) (x : HNNExtension (↥H) (restrictedA H) (restrictedB H) (restrictedPhi H hphi)) : ↑((restrictedEquivGeneratedWithStable H hphi) x) = (restrictedEmbedding H hphi) x

theorem Undecidability.HNNLemmas.generatedWithStable_inf_base {G : Type u_1} [Group G] {A B : Subgroup G} {phi : ↥A ≃* ↥B} (H : Subgroup G) (hphi : ∀ (a : ↥A), ↑a ∈ H ↔ ↑(phi a) ∈ H) : generatedWithStable H ⊓ HNNExtension.of.range = Subgroup.map HNNExtension.of H

Restricted-HNN intersection lemma (Lemma B.2 of the paper), stated in the form used by the tower calculations.

theorem Undecidability.HNNLemmas.exists_reducedWord_of_mem_generatedWithStable {G : Type u_1} [Group G] {A B : Subgroup G} {phi : ↥A ≃* ↥B} (H : Subgroup G) (hphi : ∀ (a : ↥A), ↑a ∈ H ↔ ↑(phi a) ∈ H) {x : HNNExtension G A B phi} (hx : x ∈ generatedWithStable H) : ∃ (w : HNNExtension.NormalWord.ReducedWord G A B), HNNExtension.NormalWord.ReducedWord.prod phi w = x ∧ w.head ∈ H ∧ ∀ p ∈ w.toList, p.2 ∈ H

Every element of the subgroup generated by an embedded subgroup H and the stable letter admits an ambient HNN-reduced word all of whose base coefficients lie in H. The compatibility hypothesis is exactly what is needed to form the restricted HNN extension over H.

This is the normal-form existence statement used for Borisov's irreducible {c,d} and {c,e} contexts.

@[reducible, inline]

abbrev Undecidability.HNNLemmas.CentralizerHNN (G : Type u_2) [Group G] (C : Subgroup G) : Type u_2

A centralizer HNN extension.

Equations

• Undecidability.HNNLemmas.CentralizerHNN G C = HNNExtension G C C (MulEquiv.refl ↥C)

def Undecidability.HNNLemmas.centralizerOf {G : Type u_1} [Group G] (C : Subgroup G) : G →* CentralizerHNN G C

The base-group inclusion into the HNN extension centralizing the chosen subgroup.

Equations

• Undecidability.HNNLemmas.centralizerOf C = HNNExtension.of

def Undecidability.HNNLemmas.centralizerStable {G : Type u_1} [Group G] (C : Subgroup G) : CentralizerHNN G C

The stable letter centralizing the chosen subgroup.

Equations

• Undecidability.HNNLemmas.centralizerStable C = HNNExtension.t

theorem Undecidability.HNNLemmas.centralizerOf_commute_stable_iff {G : Type u_1} [Group G] (C : Subgroup G) (g : G) : Commute ((centralizerOf C) g) (centralizerStable C) ↔ g ∈ C

In a centralizer HNN extension, an element of the base group commutes with the stable letter exactly when it belongs to the centralized subgroup. This is the two-syllable form of Britton's lemma used at Borisov's final k-stage.

def Undecidability.HNNLemmas.conjugatedStable {G : Type u_1} [Group G] (C : Subgroup G) (P : G) : CentralizerHNN G C

The stable letter conjugated by an element of the base group.

Equations

• Undecidability.HNNLemmas.conjugatedStable C P = (Undecidability.HNNLemmas.centralizerOf C) P⁻¹ * Undecidability.HNNLemmas.centralizerStable C * (Undecidability.HNNLemmas.centralizerOf C) P

def Undecidability.HNNLemmas.generatedWith {E : Type u_2} [Group E] (H : Subgroup E) (u : E) : Subgroup E

The subgroup generated by H and one additional element u.

Equations

• Undecidability.HNNLemmas.generatedWith H u = Subgroup.closure (↑H ∪ {u})

Auxiliary restricted HNN extension for the calculation in Lemma B.4 of the paper.

def Undecidability.HNNLemmas.conjugatePullback {G : Type u_1} [Group G] (A C : Subgroup G) (P : G) : Subgroup ↥A

The subgroup of A whose conjugates by P lie in C.

Equations

• Undecidability.HNNLemmas.conjugatePullback A C P = Subgroup.comap ((MulEquiv.toMonoidHom (MulAut.conj P)).comp A.subtype) C

def Undecidability.HNNLemmas.conjugatedEmbedding {G : Type u_1} [Group G] (A C : Subgroup G) (P : G) : CentralizerHNN (↥A) (conjugatePullback A C P) →* CentralizerHNN G C

The homomorphism embedding the conjugated restricted centralizer HNN extension.

Equations

• Undecidability.HNNLemmas.conjugatedEmbedding A C P = HNNExtension.lift ((Undecidability.HNNLemmas.centralizerOf C).comp A.subtype) (Undecidability.HNNLemmas.conjugatedStable C P) ⋯

def Undecidability.HNNLemmas.conjugatedList {G : Type u_1} [Group G] {A : Subgroup G} (P : G) : List (ℤˣ × ↥A) → List (ℤˣ × G)

The syllable list obtained by conjugating a restricted reduced word.

Equations

• Undecidability.HNNLemmas.conjugatedList P [] = []
• Undecidability.HNNLemmas.conjugatedList P [x_1] = [(x_1.1, P * ↑x_1.2)]
• Undecidability.HNNLemmas.conjugatedList P (x_1 :: y :: xs) = (x_1.1, P * ↑x_1.2 * P⁻¹) :: Undecidability.HNNLemmas.conjugatedList P (y :: xs)

theorem Undecidability.HNNLemmas.conjugatedList_chain {G : Type u_1} [Group G] (A C : Subgroup G) (P : G) (l : List (ℤˣ × ↥A)) (hchain : List.IsChain (fun (a b : ℤˣ × ↥A) => a.2 ∈ HNNExtension.toSubgroup (conjugatePullback A C P) (conjugatePullback A C P) a.1 → a.1 = b.1) l) : List.IsChain (fun (a b : ℤˣ × G) => a.2 ∈ HNNExtension.toSubgroup C C a.1 → a.1 = b.1) (conjugatedList P l)

def Undecidability.HNNLemmas.conjugatedReducedWord {G : Type u_1} [Group G] (A C : Subgroup G) (P : G) (w : HNNExtension.NormalWord.ReducedWord (↥A) (conjugatePullback A C P) (conjugatePullback A C P)) : HNNExtension.NormalWord.ReducedWord G C C

The reduced HNN word obtained from the conjugated restricted normal word.

Equations

• Undecidability.HNNLemmas.conjugatedReducedWord A C P w = { head := ↑w.head * P⁻¹, toList := Undecidability.HNNLemmas.conjugatedList P w.toList, chain := ⋯ }

theorem Undecidability.HNNLemmas.generatedWith_conjugatedStable_inf_base {G : Type u_1} [Group G] (A C : Subgroup G) (P : G) : generatedWith (Subgroup.map (centralizerOf C) A) (conjugatedStable C P) ⊓ (centralizerOf C).range = Subgroup.map (centralizerOf C) A

The subgroup generated by an embedded subgroup A and the conjugate P⁻¹tP meets the ambient base group exactly in A.

theorem Undecidability.HNNLemmas.conjugatedStable_not_mem_base {G : Type u_1} [Group G] (C : Subgroup G) (q : G) : conjugatedStable C q ∉ (centralizerOf C).range

A conjugate of the stable letter cannot lie in the embedded base group. This is the one-stable-letter case of Britton's lemma.

theorem Undecidability.HNNLemmas.conjugatedStable_mem_generatedWith_imp_doubleCoset {G : Type u_1} [Group G] (A C : Subgroup G) (P Q : G) (hQ : conjugatedStable C Q ∈ generatedWith (Subgroup.map (centralizerOf C) A) (conjugatedStable C P)) : ∃ (c : ↥C) (a : ↥A), P = ↑c * Q * ↑a

Exact first-coefficient consequence of membership in the subgroup generated by A and P⁻¹tP.

def Undecidability.HNNLemmas.deltaDoubleCoset {G : Type u_1} [Group G] (Delta B₀ : Subgroup G) : Set G

The product set Delta * B₀ * Delta appearing in Lemma B.5 of the paper.

Equations

• Undecidability.HNNLemmas.deltaDoubleCoset Delta B₀ = {x : G | ∃ d₁ ∈ Delta, ∃ b ∈ B₀, ∃ d₂ ∈ Delta, x = d₁ * b * d₂}

def Undecidability.HNNLemmas.centralizerReducedWord {G : Type u_1} [Group G] (Delta : Subgroup G) (g : G) (l : List (ℤˣ × G)) (chain : List.IsChain (fun (a b : ℤˣ × G) => a.2 ∈ HNNExtension.toSubgroup Delta Delta a.1 → a.1 = b.1) l) : HNNExtension.NormalWord.ReducedWord G Delta Delta

The reduced word with the specified initial coefficient and syllable chain.

Equations

• Undecidability.HNNLemmas.centralizerReducedWord Delta g l chain = { head := g, toList := l, chain := chain }

For two equal reduced words in a centralizer HNN extension, comparison of their first base coefficients gives an element of Delta. Commuting that element through the first stable letter lets us repeat the argument on the tails. This is the coefficient-by-coefficient form of the normal-form argument needed in Lemma B.5 of the paper.

theorem Undecidability.HNNLemmas.centralizer_intersection {G : Type u_1} [Group G] (Delta L B₀ C : Subgroup G) (hCL : C ≤ L) (hCB₀ : C ≤ B₀) (hinter : ↑L ∩ deltaDoubleCoset Delta B₀ = ↑C) : generatedWith (Subgroup.map (centralizerOf Delta) L) (centralizerStable Delta) ⊓ generatedWith (Subgroup.map (centralizerOf Delta) B₀) (centralizerStable Delta) = generatedWith (Subgroup.map (centralizerOf Delta) C) (centralizerStable Delta)

Lemma B.5 of the paper: intersection inside a centralizer HNN extension.

theorem Undecidability.HNNLemmas.conjugated_doubleCoset_intersection {G : Type u_1} [Group G] (A C B₀ C₀ : Subgroup G) (hAB : A ≤ B₀) (hCB : C ≤ B₀) (hC₀C : C₀ ≤ C) (P : G) (hP : P ∉ B₀) : ↑(generatedWith (Subgroup.map (centralizerOf C) C₀) (centralizerStable C)) ∩ deltaDoubleCoset (generatedWith (Subgroup.map (centralizerOf C) A) (conjugatedStable C P)) (Subgroup.map (centralizerOf C) B₀) = ↑(Subgroup.map (centralizerOf C) C₀)

The nested normal-form calculation used in the proof of Proposition 3.8 of the paper.

Inside the centralizer HNN extension of G over C, let p = P⁻¹tP. If A ≤ B₀, C ≤ B₀, C₀ ≤ C, and P ∉ B₀, then the subgroup generated by C₀ and t meets

<A,p> · B₀ · <A,p>

exactly in the embedded copy of C₀. The proof first takes a reduced p-word with coefficients in B₀, substitutes p = P⁻¹tP, and compares it with a reduced t-word whose coefficients lie in C₀. A first stable letter would force P ∈ B₀; hence the p-length is zero, after which the restricted-HNN intersection lemma applies.