ModuleRealProTwoFrattiniQuotient.lean
Nyll.SawinTotallyRealTowers.RealProTwoFrattiniQuotient
3 declarations indexed from sourceView source ↗ Module documentation
The actual finite Frattini quotient of the initial real tower
The proved Frattini fixed-field comparison identifies the canonical power--commutator quotient with the Galois group of the five quadratic layers. Its cardinality is therefore thirty-two. No finite-generation, quotient-finiteness, or rank hypothesis enters the construction.
Declarations
ClassFieldTower.Sawin.powerCommutatorNormal
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTower.Sawin
open ClassFieldTower.ProP
ClassFieldTower.Sawin.maximalRealProTwo_powerCommutatorQuotientEquiv
DocumentationThe canonical power--commutator quotient acts as the full Galois group of the actual five-generator multiquadratic field.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTower.Sawin
open ClassFieldTower.ProP
private local instance powerCommutatorNormal :
(closedPowerCommutator 2
(maximalRealProPOutside 2 sawinRationalPrimeSupport ≃ₐ[ℚ]
maximalRealProPOutside 2 sawinRationalPrimeSupport)).Normal :=
closedPowerCommutator_normal 2
(maximalRealProPOutside 2 sawinRationalPrimeSupport ≃ₐ[ℚ]
maximalRealProPOutside 2 sawinRationalPrimeSupport)
ClassFieldTower.Sawin.maximalRealProTwo_powerCommutatorQuotient_card
DocumentationThe canonical Frattini quotient of the constructed real pro-two group has exactly thirty-two elements.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTower.Sawin
open ClassFieldTower.ProP
private local instance powerCommutatorNormal :
(closedPowerCommutator 2
(maximalRealProPOutside 2 sawinRationalPrimeSupport ≃ₐ[ℚ]
maximalRealProPOutside 2 sawinRationalPrimeSupport)).Normal :=
closedPowerCommutator_normal 2
(maximalRealProPOutside 2 sawinRationalPrimeSupport ≃ₐ[ℚ]
maximalRealProPOutside 2 sawinRationalPrimeSupport)