ModuleRealProTwoDeepFrobenius.lean
Nyll.SawinTotallyRealTowers.RealProTwoDeepFrobenius
2 declarations indexed from sourceView source ↗ Module documentation
New rational primes with deep Frobenius lifts
The actual finite stage detecting source depth has completely split rational primes congruent to one modulo four outside any finite set. Excluding also the six allowed ramified primes gives an actual new unramified Frobenius with a source lift of the prescribed depth.
Declarations
ClassFieldTower.Sawin.deepFrobeniusPrimeTwo
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
namespace ClassFieldTower.Sawin
open ClassFieldTower.ProP ProCGroups.FiniteGeneration
open AlgebraicNumberTheory.PrimeSelection
universe u
ClassFieldTower.Sawin.exists_sawinPrime_with_deep_frobenius_lift
DocumentationOutside any finite set and the six ramified primes, a rational prime congruent to one modulo four has an actual Frobenius lift of any requested depth in the given finitely generated profinite source.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
namespace ClassFieldTower.Sawin
open ClassFieldTower.ProP ProCGroups.FiniteGeneration
open AlgebraicNumberTheory.PrimeSelection
universe u
private local instance deepFrobeniusPrimeTwo : Fact (Nat.Prime 2) := ⟨Nat.prime_two⟩