The finite-rank free source is an actual completion of an abstract free group. Its epimorphism to the arithmetic group has kernel in the Frattini subgroup.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTower.Sawin
open ProCGroups ProCGroups.FreeProC ProCGroups.Generation ProCGroups.FiniteGeneration
open ClassFieldTower.ProPinstance : Fact (Nat.Prime 2)The constructed free pro-2 group on five generators.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTower.Sawin
open ProCGroups ProCGroups.FreeProC ProCGroups.Generation ProCGroups.FiniteGeneration
open ClassFieldTower.ProPdef sawinFreeProTwoSource :
EpimorphicallyFreeProCGroupOnConvergingSetData.{0, 0} (FiniteGroupClass.pGroup 2)The actual free source has exactly five basis elements.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTower.Sawin
open ProCGroups ProCGroups.FreeProC ProCGroups.Generation ProCGroups.FiniteGeneration
open ClassFieldTower.ProPtheorem sawinFreeProTwoSource_basisCard : Cardinal.mk sawinFreeProTwoSource.basis = 5The arithmetic group is an actual quotient of a rank-five free pro-2 group whose kernel lies in the closed power--commutator subgroup.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTower.Sawin
open ProCGroups ProCGroups.FreeProC ProCGroups.Generation ProCGroups.FiniteGeneration
open ClassFieldTower.ProPtheorem exists_maximalRealProTwo_minimal_free_epimorphism :
∃ q : sawinFreeProTwoSource.carrier →ₜ*
(maximalRealProPOutside 2 sawinRationalPrimeSupport ≃ₐ[ℚ]
maximalRealProPOutside 2 sawinRationalPrimeSupport),
Function.Surjective q ∧
q.toMonoidHom.ker ≤ closedPowerCommutator 2 sawinFreeProTwoSource.carrier