NYLL
Module

RealProTwoGeneratorRank.lean

Nyll.SawinTotallyRealTowers.RealProTwoGeneratorRank
1 declaration indexed from sourceView source ↗

Module documentation

Five generators for the initial real pro-two group

The computed power--commutator quotient has order 32. Its vector-space basis lifts to a finite generating set of the actual Galois group by the pro-p Burnside criterion. The quotient dimension also proves minimality.

Imports19
Imported by4

Declarations

theorem

maximalRealProTwo_generatorRank

L43 ↗
ClassFieldTower.Sawin.maximalRealProTwo_generatorRank
Documentation

The actual maximal real pro-two group is generated by five elements, and five is its topological generator rank.

Source context 3 commands

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

open scoped IsMulCommutative
namespace ClassFieldTower.Sawin
open ClassFieldTower.ProP ProCGroups.Generation ProCGroups.FiniteGeneration
Lean source · statement
theorem maximalRealProTwo_generatorRank :
    TopologicallyGeneratedByAtMost 5
      (maximalRealProPOutside 2 sawinRationalPrimeSupport ≃ₐ[ℚ]
        maximalRealProPOutside 2 sawinRationalPrimeSupport) ∧
    topologicalGeneratorRank
      (maximalRealProPOutside 2 sawinRationalPrimeSupport ≃ₐ[ℚ]
        maximalRealProPOutside 2 sawinRationalPrimeSupport) = 5

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