NYLL
Module

MinimalEpimorphism.lean

Nyll.ProCGroups.ProP.MinimalEpimorphism
3 declarations indexed from sourceView source ↗

Module documentation

Minimal epimorphisms of finitely generated pro-p groups

Equal generator ranks make the induced epimorphism of finite Frattini quotients injective. The original kernel therefore lies in the source Frattini subgroup.

Imports10
Imported by3

Declarations

theorem

natCard_module

L34 ↗
ClassFieldTower.ProP.natCard_module
Source context 4 commands

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

open scoped IsMulCommutative
namespace ClassFieldTower.ProP
open ProCGroups.FiniteGeneration
universe u v

-- Fix the module data at the generic field boundary before specializing to a quotient.
Lean source · statement
theorem natCard_module
    (K : Type*) (V : Type*) [DivisionRing K] [AddCommGroup V]
    [moduleInst : Module K V] [finiteModuleInst : Module.Finite K V] :
    Nat.card V = Nat.card K ^ Module.finrank K V
theorem

natCard_powerCommutatorQuotient

L41 ↗
ClassFieldTower.ProP.natCard_powerCommutatorQuotient
Documentation

The Frattini quotient has cardinality p raised to the minimal generator number.

Source context 4 commands

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

open scoped IsMulCommutative
namespace ClassFieldTower.ProP
open ProCGroups.FiniteGeneration
universe u v

-- Fix the module data at the generic field boundary before specializing to a quotient.
Lean source · statement
theorem natCard_powerCommutatorQuotient
    (p : ℕ) [Fact p.Prime]
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (hG : ProCGroups.ProC.HasPGroupOpenNormalBasis p G)
    (hfg : TopologicallyFinitelyGenerated G) :
    Nat.card (powerCommutatorQuotient p G) = p ^ topologicalGeneratorRank G
theorem

ker_le_closedPowerCommutator_of_generatorRank_eq

L72 ↗
ClassFieldTower.ProP.ker_le_closedPowerCommutator_of_generatorRank_eq
Documentation

A continuous epimorphism between equally generated pro-p groups has Frattini kernel.

Source context 4 commands

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

open scoped IsMulCommutative
namespace ClassFieldTower.ProP
open ProCGroups.FiniteGeneration
universe u v

-- Fix the module data at the generic field boundary before specializing to a quotient.
Lean source · statement
theorem ker_le_closedPowerCommutator_of_generatorRank_eq
    (p : ℕ) [Fact p.Prime]
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
    (hG : ProCGroups.ProC.HasPGroupOpenNormalBasis p G)
    (hH : ProCGroups.ProC.HasPGroupOpenNormalBasis p H)
    (hfg : TopologicallyFinitelyGenerated G) (hhfg : TopologicallyFinitelyGenerated H)
    (f : G →ₜ* H) (hf : Function.Surjective f)
    (hrank : topologicalGeneratorRank G = topologicalGeneratorRank H) :
    f.toMonoidHom.ker ≤ closedPowerCommutator p G

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.