Module

RelatorDepth.lean

Nyll.ProCGroups.ProP.Presentation.RelatorDepth

4 declarations indexed from sourceView source ↗

Module documentation

Zassenhaus depth of displayed relators

The relation-depth interface reuses the group-level predicate-valued depth. Minimality supplies degree two directly from the identified power--commutator core, without choosing a finite maximum for an element of infinite depth.

Imports2

Imported by6

def

RelatorZassenhausDepthAtLeast

L39 ↗

ClassFieldTower.ProP.FiniteProPPresentation.RelatorZassenhausDepthAtLeast

Documentation

The displayed i-th relator has Zassenhaus depth at least n.

Source context 10 commands

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

open scoped Topology
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

def RelatorZassenhausDepthAtLeast
    (P : FiniteProPPresentation p d r sourceData G)
    (n : ℕ) (i : Fin r) : Prop

theorem

relatorZassenhausDepthAtLeast_iff

L46 ↗

ClassFieldTower.ProP.FiniteProPPresentation.relatorZassenhausDepthAtLeast_iff

Documentation

Relator depth is exactly completed augmentation-power membership of its group-like difference.

Source context 10 commands

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

open scoped Topology
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 relatorZassenhausDepthAtLeast_iff
    (P : FiniteProPPresentation p d r sourceData G)
    (n : ℕ) (i : Fin r) :
    P.RelatorZassenhausDepthAtLeast n i ↔
      groupLikeDifference p sourceData.carrier (P.relator i) ∈
        closedAugmentationPower p sourceData.carrier n

theorem

relatorZassenhausDepthAtLeast_mono

L55 ↗

ClassFieldTower.ProP.FiniteProPPresentation.relatorZassenhausDepthAtLeast_mono

Documentation

A lower depth bound for a relator can be weakened.

Source context 10 commands

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

open scoped Topology
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 relatorZassenhausDepthAtLeast_mono
    (P : FiniteProPPresentation p d r sourceData G)
    {m n : ℕ} (hmn : m ≤ n) {i : Fin r}
    (hi : P.RelatorZassenhausDepthAtLeast n i) :
    P.RelatorZassenhausDepthAtLeast m i

theorem

relatorZassenhausDepthAtLeast_two

L64 ↗

ClassFieldTower.ProP.FiniteProPPresentation.relatorZassenhausDepthAtLeast_two

Documentation

Every displayed relator of a minimal presentation has depth at least two.

Source context 10 commands

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

open scoped Topology
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 relatorZassenhausDepthAtLeast_two
    (P : FiniteProPPresentation p d r sourceData G)
    (hP : P.IsMinimal) (i : Fin r) :
    P.RelatorZassenhausDepthAtLeast 2 i

Module documentation

Zassenhaus depth of displayed relators

Declarations

RelatorZassenhausDepthAtLeast

relatorZassenhausDepthAtLeast_iff

relatorZassenhausDepthAtLeast_mono

relatorZassenhausDepthAtLeast_two