Module

CountableRelators.lean

Nyll.ProCGroups.GolodShafarevich.CountableRelators

2 declarations indexed from sourceView source ↗

Module documentation

Countable deep relations preserve a strict Golod--Shafarevich budget

If the final quotient were finite, its open, finitely generated relation subgroup would already be generated by one finite prefix. The weighted finite-presentation inequality then contradicts the prefix budget.

Imports5

Nyll.ProCGroups.GolodShafarevich.WeightedFiniteCriterion
Nyll.ProCGroups.ProP.CountableRelatorFiniteWitness
Nyll.ProCGroups.ProP.Presentation.FiniteGeneration
Nyll.ProCGroups.ProC.InverseLimits.Limits
Mathlib.Algebra.BigOperators.Fin

Imported by2

theorem

range_addCases_prefix

L29 ↗

ClassFieldTower.ProP.range_addCases_prefix

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.Presentations
noncomputable section
universe u

Lean source · full declaration

theorem range_addCases_prefix
    {F : Type u} {r N : ℕ} (a : Fin r → F) (f : ℕ → F) :
    Set.range (Fin.addCases a (fun i : Fin N => f i)) =
      Set.range a ∪ f '' (Finset.range N : Set ℕ) := by
  ext x
  constructor
  · rintro ⟨i, rfl⟩
    refine Fin.addCases ?_ ?_ i
    · intro j
      exact Or.inl ⟨j, by simp⟩
    · intro j
      exact Or.inr ⟨j, by simp, by simp⟩
  · rintro (⟨i, rfl⟩ | ⟨n, hn, rfl⟩)
    · exact ⟨Fin.castAdd N i, by simp⟩
    · refine ⟨Fin.natAdd r ⟨n, by simpa using hn⟩, ?_⟩
      exact Fin.addCases_right _

theorem

infinite_quotient_of_countable_relator_budget

L57 ↗

ClassFieldTower.ProP.FiniteProPPresentation.infinite_quotient_of_countable_relator_budget

Documentation

Adding a countable family of displayed deep relators preserves infinitude when every finite prefix has a nonpositive weighted GS polynomial.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.Presentations
noncomputable section
universe u
namespace FiniteProPPresentation
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_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 (sourceData.carrier ⧸
      closedNormalClosure (Set.range P.relator ∪ Set.range f))

Module documentation

Countable deep relations preserve a strict Golod--Shafarevich budget

Declarations

range_addCases_prefix

infinite_quotient_of_countable_relator_budget