Module

WeightedFiniteCriterion.lean

Nyll.ProCGroups.GolodShafarevich.WeightedFiniteCriterion

2 declarations indexed from sourceView source ↗

Module documentation

Weighted finite-presentation Golod--Shafarevich criterion

Arbitrary displayed relator depth bounds are already supported by the truncated Fox inequality. No minimality or finite-presentation assertion about a later countable quotient is required here.

Imports4

Imported by2

theorem

finite_gsPolynomial_pos

L39 ↗

ClassFieldTower.ProP.FiniteProPPresentation.finite_gsPolynomial_pos

Documentation

Every finite target satisfies strict positivity of the polynomial of any displayed finite presentation with the given lower relator depths.

Source context 9 commands

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

namespace ClassFieldTower.ProP
open ProCGroups
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 finite_gsPolynomial_pos
    [Finite G] (P : FiniteProPPresentation p d r sourceData G)
    (ν : Fin r → ℕ)
    (hν : ∀ i, P.RelatorZassenhausDepthAtLeast (ν i) i)
    {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t < 1) :
    0 < 1 - d * t + ∑ i : Fin r, t ^ ν i

theorem

infinite_of_gsPolynomial_nonpos

L60 ↗

ClassFieldTower.ProP.FiniteProPPresentation.infinite_of_gsPolynomial_nonpos