Module

RelationCardinal.lean

Nyll.ProCGroups.ProP.Presentation.RelationCardinal

7 declarations indexed from sourceView source ↗

Module documentation

Minimal relation cardinal

The relation rank is defined only after an actual finite minimal presentation witness has been constructed. It is the least displayed relation count among such presentations; no existence or comparison theorem is hidden in the definition.

Imports1

Nyll.ProCGroups.ProP.Presentation.GeneratorRank

Imported by7

def

HasFiniteMinimalPresentation

L29 ↗

ClassFieldTower.ProP.HasFiniteMinimalPresentation

Documentation

A profinite group admits an actual finite minimal pro-p presentation.

Source context 5 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
noncomputable section
universe u

Lean source · statement

def HasFiniteMinimalPresentation
    (p : ℕ) [Fact p.Prime]
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] : Prop

def

relationCounts

L39 ↗

ClassFieldTower.ProP.relationCounts

Documentation

Relation counts realized by finite minimal presentations.

Source context 5 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
noncomputable section
universe u

Lean source · statement

def relationCounts
    (p : ℕ) [Fact p.Prime]
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] : Set ℕ

theorem

relationCounts_nonempty

L50 ↗

ClassFieldTower.ProP.relationCounts_nonempty

Documentation

A finite minimal presentation witness makes the set of relation counts nonempty.

Source context 5 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
noncomputable section
universe u

Lean source · statement

theorem relationCounts_nonempty
    {p : ℕ} [Fact p.Prime]
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (hG : HasFiniteMinimalPresentation p G) :
    (relationCounts p G).Nonempty

def

minimalRelationRank

L60 ↗

ClassFieldTower.ProP.minimalRelationRank

Documentation

The least relation count among actual finite minimal presentations.

Source context 5 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
noncomputable section
universe u

Lean source · statement

def minimalRelationRank
    (p : ℕ) [Fact p.Prime]
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (_hG : HasFiniteMinimalPresentation p G) : ℕ

theorem

minimalRelationRank_mem_relationCounts

L69 ↗

ClassFieldTower.ProP.minimalRelationRank_mem_relationCounts

Documentation

The least relation count is itself realized by a finite minimal presentation.

Source context 5 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
noncomputable section
universe u

Lean source · statement

theorem minimalRelationRank_mem_relationCounts
    {p : ℕ} [Fact p.Prime]
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (hG : HasFiniteMinimalPresentation p G) :
    minimalRelationRank p G hG ∈ relationCounts p G

theorem

minimalRelationRank_le

L78 ↗

ClassFieldTower.ProP.FiniteProPPresentation.minimalRelationRank_le

Documentation

Every concrete minimal presentation bounds the least relation rank.

Source context 5 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
noncomputable section
universe u

Lean source · statement

theorem FiniteProPPresentation.minimalRelationRank_le
    {p d r : ℕ} [Fact p.Prime]
    {sourceData :
      FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
        (FiniteGroupClass.pGroup p)}
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (P : FiniteProPPresentation p d r sourceData G) (hP : P.IsMinimal)
    (hG : HasFiniteMinimalPresentation p G) :
    minimalRelationRank p G hG ≤ r

theorem

exists_presentation_relationCard_eq_minimal

L93 ↗

ClassFieldTower.ProP.exists_presentation_relationCard_eq_minimal

Documentation

Some concrete finite minimal presentation realizes the least relation rank.

Source context 5 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
noncomputable section
universe u

Lean source · statement

theorem exists_presentation_relationCard_eq_minimal
    {p : ℕ} [Fact p.Prime]
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (hG : HasFiniteMinimalPresentation p G) :
    ∃ sourceData :
        FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
          (FiniteGroupClass.pGroup p),
      ∃ d, ∃ P : FiniteProPPresentation p d (minimalRelationRank p G hG)
          sourceData G,
        P.IsMinimal

Module documentation

Minimal relation cardinal

Declarations

HasFiniteMinimalPresentation

relationCounts

relationCounts_nonempty

minimalRelationRank

minimalRelationRank_mem_relationCounts

minimalRelationRank_le

exists_presentation_relationCard_eq_minimal