Reduce SmallUndecidableGroups compilation memory

LeanPool/SmallUndecidableGroups/GroupTheory/HNNLemmas.lean

@@ -20,6 +20,50 @@ namespace HNNLemmas
 variable {G : Type*} [Group G]
 variable {A B : Subgroup G} {phi : A ≃* B}
 
+/-- Homomorphisms out of a generated subgroup agree when they agree on its generators. -/
+theorem closure_hom_ext {Q : Type*} [Group Q] {s : Set G}
+    {f g : Subgroup.closure s →* Q}
+    (h : ∀ x (hx : x ∈ s),
+      f ⟨x, Subgroup.subset_closure hx⟩ = g ⟨x, Subgroup.subset_closure hx⟩) :
+    f = g := by
+  apply MonoidHom.ext
+  intro x
+  refine Subgroup.closure_induction
+    (p := fun y hy ↦ f ⟨y, hy⟩ = g ⟨y, hy⟩) h ?_ ?_ ?_ x.property
+  · exact (map_one f).trans (map_one g).symm
+  · intro a b ha hb hfa hfb
+    change f (⟨a, ha⟩ * ⟨b, hb⟩) = g (⟨a, ha⟩ * ⟨b, hb⟩)
+    rw [map_mul, map_mul]
+    exact congrArg₂ (fun u v : Q ↦ u * v) hfa hfb
+  · intro a ha hfa
+    change f (⟨a, ha⟩⁻¹) = g (⟨a, ha⟩⁻¹)
+    rw [map_inv, map_inv]
+    exact congrArg (fun u : Q ↦ u⁻¹) hfa
+
+/-- Transport the base-and-stable-letter extensionality criterion through an equivalence. -/
+theorem hom_ext_of_equiv {K Q : Type*} [Group K] [Group Q]
+    (e : HNNExtension G A B phi ≃* K) {f g : K →* Q}
+    (hbase : f.comp (e.toMonoidHom.comp HNNExtension.of) =
+      g.comp (e.toMonoidHom.comp HNNExtension.of))
+    (hstable : f (e HNNExtension.t) = g (e HNNExtension.t)) : f = g := by
+  apply (MonoidHom.cancel_right (f := e.toMonoidHom) e.surjective).mp
+  exact HNNExtension.hom_ext hbase hstable
+
+/-- A cyclic-base HNN model is determined by the base generator and stable letter. -/
+theorem cyclic_hom_ext_of_equiv {K Q : Type*} [Group K] [Group Q]
+    (c : G) {A' B' : Subgroup (Subgroup.closure ({c} : Set G))} {phi' : A' ≃* B'}
+    (e : HNNExtension (Subgroup.closure ({c} : Set G)) A' B' phi' ≃* K)
+    {f g : K →* Q}
+    (hc : f (e (HNNExtension.of ⟨c, Subgroup.subset_closure (by rfl)⟩)) =
+      g (e (HNNExtension.of ⟨c, Subgroup.subset_closure (by rfl)⟩)))
+    (hstable : f (e HNNExtension.t) = g (e HNNExtension.t)) : f = g := by
+  apply hom_ext_of_equiv e
+  · apply closure_hom_ext
+    intro x hx
+    rcases Set.mem_singleton_iff.mp hx with rfl
+    exact hc
+  · exact hstable
+
 /-- An injective homomorphism identifies its domain with its range. -/
 noncomputable abbrev equivRangeOfInjective
     {H : Type*} [Group H] (f : H →* G) (hf : Function.Injective f) :

LeanPool/SmallUndecidableGroups/Host/Compression.lean

@@ -92,6 +92,14 @@ theorem eval_word {G : Type*} [Group G] (x : Fin 3 → G)
       Word.eval (fun i => Word.eval x (generatorWord i)) u :=
   Word.eval_substitute x generatorWord u
 
+/-- Evaluate a conjugated word without expanding either substituted word. -/
+private theorem eval_conjugated_word {G : Type*} [Group G]
+    (x : Fin 3 → G) (u v : HostWord) :
+    Word.eval x (Word.product [Word.inverse u, v, u]) =
+      (Word.eval x u)⁻¹ * Word.eval x v * Word.eval x u := by
+  simp only [Word.eval_product, Word.eval_inverse, List.map_cons, List.map_nil,
+    List.prod_cons, List.prod_nil, mul_one, mul_assoc]
+
 private theorem commute_inv_left {G : Type*} [Group G]
     {a b : G} (h : a * b = b * a) : a⁻¹ * b = b * a⁻¹ :=
   (Commute.inv_left_iff.mpr h).eq
@@ -264,17 +272,19 @@ theorem relator_eq_one (datum : Thue.StandingDatum) (i : Fin 14) :
       (Y⁻¹ * E * Y) * D⁻¹ = Y⁻¹ * (E * Y) * D⁻¹ := by group
       _ = 1 := h8raw
   have hTdef : T = Z⁻¹ * D * Z := by
-    simp [T, Z, D, tWord, Word.eval_product, mul_assoc]
+    exact eval_conjugated_word x zWord dWord
   have hCdef : C = Z⁻¹ * T * Z := by
-    simp [C, Z, T, cWord, tWord, Word.eval_product, mul_assoc]
+    exact eval_conjugated_word x zWord tWord
   have hYdef : Y = Z⁻¹ * C * Z := by
-    simp [Y, Z, C, yWord, cWord, tWord, Word.eval_product, mul_assoc]
+    exact eval_conjugated_word x zWord cWord
   have hEdef : E = Y⁻¹ * D⁻¹ * Y := by
-    simp [E, Y, D, eWord, yWord, cWord, tWord, Word.eval_product, mul_assoc]
+    simpa only [E, Y, D, eWord, Word.eval_inverse] using
+      eval_conjugated_word x yWord (Word.inverse dWord)
   have hKdef : K = Y⁻¹ * T * Y := by
-    simp [K, Y, T, kWord, yWord, cWord, tWord, Word.eval_product, mul_assoc]
+    exact eval_conjugated_word x yWord tWord
   have hRdef : R = Y⁻¹ * S⁻¹ * Y := by
-    simp [R, Y, S, s2Word, yWord, cWord, tWord, Word.eval_product, mul_assoc]
+    simpa only [R, Y, S, s2Word, Word.eval_inverse] using
+      eval_conjugated_word x yWord (Word.inverse sWord)
   obtain ⟨hRd, hRe, hRCC, hKCC, hKEcomm, hTc⟩ :=
     transported_relations D E S R C T K Y Z
       hTdef hCdef hYdef hEdef hKdef hRdef hSd hSe hSc hDt hYe

LeanPool/SmallUndecidableGroups/Host/YStage.lean

@@ -6,8 +6,7 @@ Authors: Marc Kegel, Shana Yunsheng Li, Qiuyu Ren
 
 module
 
-public import LeanPool.SmallUndecidableGroups.Borisov.Model.FinalModel
-public import LeanPool.SmallUndecidableGroups.Borisov.Assertions.InputsBridge
+public import LeanPool.SmallUndecidableGroups.Host.YStage.Definitions
 
 /-!
 # The first compression HNN extension
@@ -49,14 +48,6 @@ honest automorphism of the four-generator group `Gamma3`; its inverse sends
 `d ↦ e`, `e ↦ d⁻¹` and has the same action on the stable letters.
 -/
 
-/-- The four generator images defining the twisting automorphism of the initial Borisov group. -/
-def twistGenerator : Fin 4 → Gamma3 :=
-  ![e3⁻¹, d3, secondStableInStageThree⁻¹, firstStableInStageThree⁻¹]
-
-/-- The four generator images defining the inverse twisting automorphism. -/
-def untwistGenerator : Fin 4 → Gamma3 :=
-  ![e3, d3⁻¹, secondStableInStageThree⁻¹, firstStableInStageThree⁻¹]
-
 private theorem stable_conjugates_d
     (s : Gamma3) (hs : d3 ^ 4 * s = s * d3) :
     s * d3 * s⁻¹ = d3 ^ 4 := by
@@ -311,25 +302,6 @@ theorem untwist_mem_V {x : Gamma3}
   rw [← V_inf_J3 datum 1]
   exact ⟨hxV, hxJ⟩
 
-/-- The source rule subgroup restricted to the selected three-generator subgroup. -/
-abbrev CRestrictedA (beta : Fin 2) :=
-  restrictedA (A := U datum) (J3 beta)
-
-/-- The target rule subgroup restricted to the selected three-generator subgroup. -/
-abbrev CRestrictedB (beta : Fin 2) :=
-  restrictedB (B := V datum) (J3 beta)
-
-/-- The rewriting-rule subgroup isomorphism restricted to the selected base subgroup. -/
-def cRestrictedPhi (beta : Fin 2) :
-    CRestrictedA datum beta ≃* CRestrictedB datum beta :=
-  restrictedPhi (J3 beta)
-    (cEquiv_mem_J3_iff datum (rankFiveFree datum) beta)
-
-/-- The exact restricted `c`-HNN extension over `J_beta`. -/
-abbrev CRestricted (beta : Fin 2) :=
-  HNNExtension (J3 beta) (CRestrictedA datum beta) (CRestrictedB datum beta)
-    (cRestrictedPhi datum beta)
-
 /-- The twisting equivalence between the two restricted source rule subgroups. -/
 def cRestrictedAEquiv :
     CRestrictedA datum 0 ≃* CRestrictedA datum 1 where
@@ -401,17 +373,6 @@ def cRestrictedEquiv : CRestricted datum 0 ≃* CRestricted datum 1 :=
         (HNNExtension.t : CRestricted datum 0) =
       (HNNExtension.t : CRestricted datum 1) := rfl
 
-/-- The exact subgroup `⟨d,e,c,s_beta⟩` of `Gamma2`. -/
-def CSubgroup (beta : Fin 2) : Subgroup (Gamma2 datum (rankFiveFree datum)) :=
-  generatedWithStable (A := U datum) (B := V datum)
-    (phi := cEquiv datum (rankFiveFree datum)) (J3 beta)
-
-/-- The equivalence from the restricted HNN model onto its generated subgroup. -/
-def cRestrictedRangeEquiv (beta : Fin 2) :
-    CRestricted datum beta ≃* CSubgroup datum beta :=
-  restrictedEquivGeneratedWithStable (J3 beta)
-    (cEquiv_mem_J3_iff datum (rankFiveFree datum) beta)
-
 @[simp] private theorem cRestrictedRangeEquiv_of_coe
     (beta : Fin 2) (x : J3 beta) :
     ((cRestrictedRangeEquiv datum beta (HNNExtension.of x) :
@@ -454,37 +415,6 @@ def cSubgroupEquiv : CSubgroup datum 0 ≃* CSubgroup datum 1 :=
   (cRestrictedRangeEquiv datum 0).symm.trans
     ((cRestrictedEquiv datum).trans (cRestrictedRangeEquiv datum 1))
 
-theorem d3_mem_J3 (beta : Fin 2) : d3 ∈ J3 beta :=
-  Subgroup.subset_closure (by simp)
-
-theorem e3_mem_J3 (beta : Fin 2) : e3 ∈ J3 beta :=
-  Subgroup.subset_closure (by simp)
-
-theorem stable3_mem_J3 (beta : Fin 2) : stable3 beta ∈ J3 beta :=
-  Subgroup.subset_closure (by simp)
-
-/-- The generator `d` regarded as an element of the selected core subgroup. -/
-def coreD (beta : Fin 2) : CSubgroup datum beta :=
-  ⟨of3 datum (rankFiveFree datum) d3,
-    Subgroup.subset_closure (Or.inl ⟨d3, d3_mem_J3 beta, rfl⟩)⟩
-
-/-- The generator `e` regarded as an element of the selected core subgroup. -/
-def coreE (beta : Fin 2) : CSubgroup datum beta :=
-  ⟨of3 datum (rankFiveFree datum) e3,
-    Subgroup.subset_closure (Or.inl ⟨e3, e3_mem_J3 beta, rfl⟩)⟩
-
-/-- The selected stable generator regarded as an element of the core subgroup. -/
-def coreStable (beta : Fin 2) : CSubgroup datum beta :=
-  ⟨of3 datum (rankFiveFree datum) (stable3 beta),
-    Subgroup.subset_closure
-      (Or.inl ⟨stable3 beta, stable3_mem_J3 beta, rfl⟩)⟩
-
-/-- The generator `c` regarded as an element of the core subgroup. -/
-def coreC (beta : Fin 2) : CSubgroup datum beta :=
-  ⟨BorisovCStage.c datum (rankFiveFree datum),
-    (CSubgroup datum beta).inv_mem
-      (Subgroup.subset_closure (Or.inr (Set.mem_singleton _)))⟩
-
 private theorem cRestrictedRangeEquiv_symm_of (beta : Fin 2) (x : J3 beta) :
     (cRestrictedRangeEquiv datum beta).symm
         ⟨of3 datum (rankFiveFree datum) (x : Gamma3),
@@ -854,65 +784,6 @@ def minusEmbedding :
     MinusRestricted datum →* FinalStage datum (rankFiveFree datum) :=
   (toFinalStage datum (rankFiveFree datum)).comp (minusEmbeddingToT datum)
 
-/-- The proved freeness witness supplying the concrete iterated-HNN model. -/
-abbrev FreeInput : RankFiveFree datum := rankFiveFree datum
-
-/-- The semantic Borisov group `Gamma`. -/
-abbrev Gamma := FinalStage datum (FreeInput datum)
-
-/-- The concrete generator `d` in the final Borisov model. -/
-def d : Gamma datum := modelD datum (FreeInput datum)
-/-- The concrete generator `e` in the final Borisov model. -/
-def e : Gamma datum := modelE datum (FreeInput datum)
-/-- The concrete first stable generator in the final Borisov model. -/
-def s1 : Gamma datum := modelS1 datum (FreeInput datum)
-/-- The concrete second stable generator in the final Borisov model. -/
-def s2 : Gamma datum := modelS2 datum (FreeInput datum)
-/-- The concrete generator `c` in the final Borisov model. -/
-def c : Gamma datum := modelC datum (FreeInput datum)
-/-- The concrete generator `t` in the final Borisov model. -/
-def t : Gamma datum := modelT datum (FreeInput datum)
-/-- The concrete generator `k` in the final Borisov model. -/
-def k : Gamma datum := modelK datum (FreeInput datum)
-
-/-- `H_y^- = ⟨d,e,c,t,s₁⟩`. -/
-def HMinus : Subgroup (Gamma datum) :=
-  Subgroup.closure ({d datum, e datum, c datum, t datum, s1 datum} : Set (Gamma datum))
-
-/-- `H_y^+ = ⟨d,e,c,k,s₂⟩`. -/
-def HPlus : Subgroup (Gamma datum) :=
-  Subgroup.closure ({d datum, e datum, c datum, k datum, s2 datum} : Set (Gamma datum))
-
-@[simp] theorem d_mem_HMinus : d datum ∈ HMinus datum :=
-  Subgroup.subset_closure (Or.inl rfl)
-
-@[simp] theorem e_mem_HMinus : e datum ∈ HMinus datum :=
-  Subgroup.subset_closure (Or.inr (Or.inl rfl))
-
-@[simp] theorem c_mem_HMinus : c datum ∈ HMinus datum :=
-  Subgroup.subset_closure (Or.inr (Or.inr (Or.inl rfl)))
-
-@[simp] theorem t_mem_HMinus : t datum ∈ HMinus datum :=
-  Subgroup.subset_closure (Or.inr (Or.inr (Or.inr (Or.inl rfl))))
-
-@[simp] theorem s1_mem_HMinus : s1 datum ∈ HMinus datum :=
-  Subgroup.subset_closure (Or.inr (Or.inr (Or.inr (Or.inr rfl))))
-
-@[simp] theorem d_mem_HPlus : d datum ∈ HPlus datum :=
-  Subgroup.subset_closure (Or.inl rfl)
-
-@[simp] theorem e_mem_HPlus : e datum ∈ HPlus datum :=
-  Subgroup.subset_closure (Or.inr (Or.inl rfl))
-
-@[simp] theorem c_mem_HPlus : c datum ∈ HPlus datum :=
-  Subgroup.subset_closure (Or.inr (Or.inr (Or.inl rfl)))
-
-@[simp] theorem k_mem_HPlus : k datum ∈ HPlus datum :=
-  Subgroup.subset_closure (Or.inr (Or.inr (Or.inr (Or.inl rfl))))
-
-@[simp] theorem s2_mem_HPlus : s2 datum ∈ HPlus datum :=
-  Subgroup.subset_closure (Or.inr (Or.inr (Or.inr (Or.inr rfl))))
-
 private theorem J3_zero_to_HMinus {x : Gamma3} (hx : x ∈ J3 0) :
     cStageToFinal datum (rankFiveFree datum)
         (of3 datum (rankFiveFree datum) x) ∈ HMinus datum := by
@@ -1155,28 +1026,6 @@ def plusParamS2 : PlusRestricted datum :=
 /-- The stable generator `k` in the positive restricted model. -/
 def plusParamK : PlusRestricted datum := HNNExtension.t
 
-/-- The element `d` with its membership witness in the negative associated subgroup. -/
-def minusD : HMinus datum := ⟨d datum, d_mem_HMinus datum⟩
-/-- The element `e` with its membership witness in the negative associated subgroup. -/
-def minusE : HMinus datum := ⟨e datum, e_mem_HMinus datum⟩
-/-- The element `c` with its membership witness in the negative associated subgroup. -/
-def minusC : HMinus datum := ⟨c datum, c_mem_HMinus datum⟩
-/-- The element `t` with its membership witness in the negative associated subgroup. -/
-def minusT : HMinus datum := ⟨t datum, t_mem_HMinus datum⟩
-/-- The first stable element with its membership witness in the negative associated subgroup. -/
-def minusS1 : HMinus datum := ⟨s1 datum, s1_mem_HMinus datum⟩
-
-/-- The element `d` with its membership witness in the positive associated subgroup. -/
-def plusD : HPlus datum := ⟨d datum, d_mem_HPlus datum⟩
-/-- The element `e` with its membership witness in the positive associated subgroup. -/
-def plusE : HPlus datum := ⟨e datum, e_mem_HPlus datum⟩
-/-- The element `c` with its membership witness in the positive associated subgroup. -/
-def plusC : HPlus datum := ⟨c datum, c_mem_HPlus datum⟩
-/-- The element `k` with its membership witness in the positive associated subgroup. -/
-def plusK : HPlus datum := ⟨k datum, k_mem_HPlus datum⟩
-/-- The second stable element with its membership witness in the positive associated subgroup. -/
-def plusS2 : HPlus datum := ⟨s2 datum, s2_mem_HPlus datum⟩
-
 @[simp] private theorem minusParamEquiv_paramD :
     minusParamEquiv datum (minusParamD datum) = minusD datum := by
   apply Subtype.ext