Module

GeneratorRank.lean

Nyll.ProCGroups.ProP.GeneratorRank

10 declarations indexed from sourceView source ↗

Module documentation

Generator rank of a finitely generated pro-p group

This file packages the natural-valued topological generator rank and proves that, for a topologically finitely generated pro-p group, it equals the ZMod p dimension of the power--commutator quotient.

The quotient structures are canonical but deliberately section-local. This keeps them out of global instance search while avoiding repeated letI blocks in theorem statements and proofs.

Imports2

Imported by13

def

topologicalGeneratorRank

L34 ↗

ClassFieldTower.ProP.topologicalGeneratorRank

Documentation

The natural-valued topological generator rank. Its intended API is for groups whose cardinal-valued topological rank is finite.

Source context 6 commands

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

open Set
open scoped IsMulCommutative
namespace ClassFieldTower.ProP
universe u
open ProCGroups.Generation
open ProCGroups.FiniteGeneration

Lean source · statement

def topologicalGeneratorRank
    (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : ℕ

instance

(anonymous instance)

L43 ↗

Source context 8 commands

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

open Set
open scoped IsMulCommutative
namespace ClassFieldTower.ProP
universe u
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
section PowerCommutatorRank
variable {p : ℕ} {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] [Fact (Nat.Prime p)]

Lean source · statement

instance : (closedPowerCommutator p G).Normal

instance

(anonymous instance)

L46 ↗

Source context 9 commands

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

open Set
open scoped IsMulCommutative
namespace ClassFieldTower.ProP
universe u
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
section PowerCommutatorRank
variable {p : ℕ} {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] [Fact (Nat.Prime p)]
local instance : (closedPowerCommutator p G).Normal :=
  closedPowerCommutator_normal p G

Lean source · statement

instance : IsClosed (closedPowerCommutator p G : Set G)

instance

(anonymous instance)

L49 ↗

Source context 10 commands

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

open Set
open scoped IsMulCommutative
namespace ClassFieldTower.ProP
universe u
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
section PowerCommutatorRank
variable {p : ℕ} {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] [Fact (Nat.Prime p)]
local instance : (closedPowerCommutator p G).Normal :=
  closedPowerCommutator_normal p G
local instance : IsClosed (closedPowerCommutator p G : Set G) :=
  isClosed_closedPowerCommutator p G

Lean source · statement

instance : IsMulCommutative (powerCommutatorQuotient p G)

instance

(anonymous instance)

L52 ↗

Source context 11 commands

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

open Set
open scoped IsMulCommutative
namespace ClassFieldTower.ProP
universe u
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
section PowerCommutatorRank
variable {p : ℕ} {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] [Fact (Nat.Prime p)]
local instance : (closedPowerCommutator p G).Normal :=
  closedPowerCommutator_normal p G
local instance : IsClosed (closedPowerCommutator p G : Set G) :=
  isClosed_closedPowerCommutator p G
local instance : IsMulCommutative (powerCommutatorQuotient p G) :=
  powerCommutatorQuotient_isMulCommutative p G

Lean source · statement

instance : Module (ZMod p) (Additive (powerCommutatorQuotient p G))

def

powerCommutatorQuotientRank

L58 ↗

ClassFieldTower.ProP.powerCommutatorQuotientRank

Documentation

The canonical ZMod p dimension of the power--commutator quotient.

Source context 12 commands

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

open Set
open scoped IsMulCommutative
namespace ClassFieldTower.ProP
universe u
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
section PowerCommutatorRank
variable {p : ℕ} {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] [Fact (Nat.Prime p)]
local instance : (closedPowerCommutator p G).Normal :=
  closedPowerCommutator_normal p G
local instance : IsClosed (closedPowerCommutator p G : Set G) :=
  isClosed_closedPowerCommutator p G
local instance : IsMulCommutative (powerCommutatorQuotient p G) :=
  powerCommutatorQuotient_isMulCommutative p G
local instance : Module (ZMod p) (Additive (powerCommutatorQuotient p G)) :=
  AddCommGroup.zmodModule (fun x => by
    change (Additive.toMul x) ^ p = 1
    exact powerCommutatorQuotient_pow_eq_one p G (Additive.toMul x))

Lean source · statement

def powerCommutatorQuotientRank : ℕ

theorem

powerCommutatorQuotient_finite_of_topologicallyFinitelyGenerated

L63 ↗

ClassFieldTower.ProP.powerCommutatorQuotient_finite_of_topologicallyFinitelyGenerated

Documentation

A topologically finitely generated power--commutator quotient is finite.

Source context 13 commands

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

open Set
open scoped IsMulCommutative
namespace ClassFieldTower.ProP
universe u
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
section PowerCommutatorRank
variable {p : ℕ} {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] [Fact (Nat.Prime p)]
local instance : (closedPowerCommutator p G).Normal :=
  closedPowerCommutator_normal p G
local instance : IsClosed (closedPowerCommutator p G : Set G) :=
  isClosed_closedPowerCommutator p G
local instance : IsMulCommutative (powerCommutatorQuotient p G) :=
  powerCommutatorQuotient_isMulCommutative p G
local instance : Module (ZMod p) (Additive (powerCommutatorQuotient p G)) :=
  AddCommGroup.zmodModule (fun x => by
    change (Additive.toMul x) ^ p = 1
    exact powerCommutatorQuotient_pow_eq_one p G (Additive.toMul x))
omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in

Lean source · statement

theorem powerCommutatorQuotient_finite_of_topologicallyFinitelyGenerated
    (hfg : TopologicallyFinitelyGenerated G) :
    Finite (powerCommutatorQuotient p G)

theorem

topologicallyGeneratedByAtMost_iff_powerCommutatorQuotientRank_le

L101 ↗

ClassFieldTower.ProP.topologicallyGeneratedByAtMost_iff_powerCommutatorQuotientRank_le

Documentation

Bounded generation of a finitely generated pro-p group is equivalent to the dimension bound on its power--commutator quotient.

Source context 12 commands

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

open Set
open scoped IsMulCommutative
namespace ClassFieldTower.ProP
universe u
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
section PowerCommutatorRank
variable {p : ℕ} {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] [Fact (Nat.Prime p)]
local instance : (closedPowerCommutator p G).Normal :=
  closedPowerCommutator_normal p G
local instance : IsClosed (closedPowerCommutator p G : Set G) :=
  isClosed_closedPowerCommutator p G
local instance : IsMulCommutative (powerCommutatorQuotient p G) :=
  powerCommutatorQuotient_isMulCommutative p G
local instance : Module (ZMod p) (Additive (powerCommutatorQuotient p G)) :=
  AddCommGroup.zmodModule (fun x => by
    change (Additive.toMul x) ^ p = 1
    exact powerCommutatorQuotient_pow_eq_one p G (Additive.toMul x))

Lean source · statement

theorem topologicallyGeneratedByAtMost_iff_powerCommutatorQuotientRank_le
    (hpG : ProCGroups.ProC.HasPGroupOpenNormalBasis p G)
    (hfg : TopologicallyFinitelyGenerated G) {d : ℕ} :
    TopologicallyGeneratedByAtMost d G ↔ powerCommutatorQuotientRank (p := p) (G := G) ≤ d

theorem

topologicalGeneratorRank_eq_powerCommutatorQuotientRank

L141 ↗

ClassFieldTower.ProP.topologicalGeneratorRank_eq_powerCommutatorQuotientRank

Documentation

For a finitely generated pro-p group, generator rank is the canonical dimension of the power--commutator quotient.

Source context 12 commands

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

open Set
open scoped IsMulCommutative
namespace ClassFieldTower.ProP
universe u
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
section PowerCommutatorRank
variable {p : ℕ} {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] [Fact (Nat.Prime p)]
local instance : (closedPowerCommutator p G).Normal :=
  closedPowerCommutator_normal p G
local instance : IsClosed (closedPowerCommutator p G : Set G) :=
  isClosed_closedPowerCommutator p G
local instance : IsMulCommutative (powerCommutatorQuotient p G) :=
  powerCommutatorQuotient_isMulCommutative p G
local instance : Module (ZMod p) (Additive (powerCommutatorQuotient p G)) :=
  AddCommGroup.zmodModule (fun x => by
    change (Additive.toMul x) ^ p = 1
    exact powerCommutatorQuotient_pow_eq_one p G (Additive.toMul x))

Lean source · statement

theorem topologicalGeneratorRank_eq_powerCommutatorQuotientRank
    (hpG : ProCGroups.ProC.HasPGroupOpenNormalBasis p G)
    (hfg : TopologicallyFinitelyGenerated G) :
    topologicalGeneratorRank G = powerCommutatorQuotientRank (p := p) (G := G)

theorem

topologicalGeneratorRank_eq_powerCommutatorQuotient_finrank

L166 ↗

ClassFieldTower.ProP.topologicalGeneratorRank_eq_powerCommutatorQuotient_finrank

Documentation

The generator-rank formula written directly as a ZMod p finrank equality.

Source context 12 commands

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

open Set
open scoped IsMulCommutative
namespace ClassFieldTower.ProP
universe u
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
section PowerCommutatorRank
variable {p : ℕ} {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] [Fact (Nat.Prime p)]
local instance : (closedPowerCommutator p G).Normal :=
  closedPowerCommutator_normal p G
local instance : IsClosed (closedPowerCommutator p G : Set G) :=
  isClosed_closedPowerCommutator p G
local instance : IsMulCommutative (powerCommutatorQuotient p G) :=
  powerCommutatorQuotient_isMulCommutative p G
local instance : Module (ZMod p) (Additive (powerCommutatorQuotient p G)) :=
  AddCommGroup.zmodModule (fun x => by
    change (Additive.toMul x) ^ p = 1
    exact powerCommutatorQuotient_pow_eq_one p G (Additive.toMul x))

Lean source · statement

theorem topologicalGeneratorRank_eq_powerCommutatorQuotient_finrank
    (hpG : ProCGroups.ProC.HasPGroupOpenNormalBasis p G)
    (hfg : TopologicallyFinitelyGenerated G) :
    topologicalGeneratorRank G =
      Module.finrank (ZMod p) (Additive (powerCommutatorQuotient p G))

Module documentation

Generator rank of a finitely generated pro-p group

Declarations