Choose a presentation attaining the least relation count constructed in S1. Minimality identifies its displayed generator count with the actual rank five. The same presentation, including its free source and relators, is retained.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTower.Sawin
open ProCGroups ClassFieldTower.ProPinstance initialPresentationPrimeTwo : Fact (Nat.Prime 2)Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTower.Sawin
open ProCGroups ClassFieldTower.ProP
private local instance initialPresentationPrimeTwo : Fact (Nat.Prime 2) := ⟨Nat.prime_two⟩instance initialPresentationIsGalois :
IsGalois ℚ (maximalRealProPOutside 2 sawinRationalPrimeSupport)The initial arithmetic group has an actual minimal presentation on five generators and at most six relators. The chosen relator count attains the least relation rank supplied by S1.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTower.Sawin
open ProCGroups ClassFieldTower.ProP
private local instance initialPresentationPrimeTwo : Fact (Nat.Prime 2) := ⟨Nat.prime_two⟩
private local instance initialPresentationIsGalois :
IsGalois ℚ (maximalRealProPOutside 2 sawinRationalPrimeSupport) :=
maximalRealProPOutside_isGalois 2 sawinRationalPrimeSupporttheorem exists_sawinInitialProTwo_minimalPresentation :
∃ sourceData : FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{0, 0}
(FiniteGroupClass.pGroup 2),
∃ r : ℕ, ∃ P : FiniteProPPresentation 2 5 r sourceData
(maximalRealProPOutside 2 sawinRationalPrimeSupport ≃ₐ[ℚ]
maximalRealProPOutside 2 sawinRationalPrimeSupport),
P.IsMinimal ∧ r ≤ 6