ClassFieldTower.ProP.FiniteProPPresentation.infinite_target_quotient_of_countable_relator_budget
The actual presented group remains infinite after killing the images of a countable deep relator family within the displayed GS budget.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTower.ProP.FiniteProPPresentation
open ProCGroups ProCGroups.Presentations
noncomputable section
universe u
variable {p d r : ℕ} [Fact p.Prime]
variable {sourceData :
FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
(FiniteGroupClass.pGroup p)}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]Lean source · statement
theorem infinite_target_quotient_of_countable_relator_budget
(P : FiniteProPPresentation p d r sourceData G)
(ν₀ : Fin r → ℕ)
(hν₀ : ∀ i, P.RelatorZassenhausDepthAtLeast (ν₀ i) i)
(f : ℕ → sourceData.carrier) (ν : ℕ → ℕ)
(hν : ∀ n, ZassenhausDepthAtLeast p (ν n) (f n))
{t : ℝ} (ht0 : 0 ≤ t) (ht1 : t < 1)
(hbudget : ∀ N, 1 - (d : ℝ) * t +
(∑ i : Fin r, t ^ ν₀ i) + (∑ i : Fin N, t ^ ν i) ≤ 0) :
Infinite (G ⧸ closedNormalClosure (Set.range (P.quotient ∘ f)))