Module

RealProPFrobeniusStage.lean

Nyll.SawinTotallyRealTowers.RealProPFrobeniusStage

3 declarations indexed from sourceView source ↗

Module documentation

Split finite stages and deep arithmetic Frobenius lifts

The actual arithmetic Frobenius is represented by an absolute decomposition element. Complete splitting makes its finite-stage restriction trivial, so the constructed depth-detecting stage supplies a deep source lift.

Imports9

Imported by2

instance

depthStageIsGalois

L35 ↗

ClassFieldTower.Sawin.depthStageIsGalois

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.Martinet.Shafarevich ClassFieldTower.ProP
open ProCGroups.FiniteGeneration
universe u

Lean source · statement

instance depthStageIsGalois
    (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ)))
    (U : OpenNormalSubgroup
      (maximalRealProPOutside p T ≃ₐ[ℚ] maximalRealProPOutside p T)) :
    IsGalois ℚ (realProPOpenNormalStage p T U).val.toIntermediateField

theorem

maximalRealProPArithmeticFrobenius_stageRestriction_eq_one

L44 ↗

ClassFieldTower.Sawin.maximalRealProPArithmeticFrobenius_stageRestriction_eq_one

Documentation

Arithmetic Frobenius acts trivially on an actual finite arithmetic stage at every place which splits completely in that stage.

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.Martinet.Shafarevich ClassFieldTower.ProP
open ProCGroups.FiniteGeneration
universe u
private local instance depthStageIsGalois
    (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ)))
    (U : OpenNormalSubgroup
      (maximalRealProPOutside p T ≃ₐ[ℚ] maximalRealProPOutside p T)) :
    IsGalois ℚ (realProPOpenNormalStage p T U).val.toIntermediateField :=
  (realProPOpenNormalStage p T U).val.isGalois

Lean source · statement

theorem maximalRealProPArithmeticFrobenius_stageRestriction_eq_one
    (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ)))
    (U : OpenNormalSubgroup
      (maximalRealProPOutside p T ≃ₐ[ℚ] maximalRealProPOutside p T))
    (v : HeightOneSpectrum (𝓞 ℚ))
    (hsplit : FinitePlaceSplitsCompletely
      (K := ℚ) (L := (realProPOpenNormalStage p T U).val) v) :
    realProPOpenNormalStageRestriction p T U
      (maximalRealProPArithmeticFrobenius p T v) = 1

theorem

exists_realProPOpenNormalStage_with_deep_frobenius_lifts

L68 ↗

ClassFieldTower.Sawin.exists_realProPOpenNormalStage_with_deep_frobenius_lifts

Documentation

For every requested source depth, an actual finite arithmetic stage ensures that its completely split places have Frobenius lifts of that depth.

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.Martinet.Shafarevich ClassFieldTower.ProP
open ProCGroups.FiniteGeneration
universe u
private local instance depthStageIsGalois
    (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ)))
    (U : OpenNormalSubgroup
      (maximalRealProPOutside p T ≃ₐ[ℚ] maximalRealProPOutside p T)) :
    IsGalois ℚ (realProPOpenNormalStage p T U).val.toIntermediateField :=
  (realProPOpenNormalStage p T U).val.isGalois

Lean source · statement

theorem exists_realProPOpenNormalStage_with_deep_frobenius_lifts
    (p : ℕ) [Fact p.Prime] (T : Set (HeightOneSpectrum (𝓞 ℚ)))
    {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
    [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
    (hfg : TopologicallyFinitelyGenerated F)
    (q : F →ₜ* (maximalRealProPOutside p T ≃ₐ[ℚ] maximalRealProPOutside p T))
    (hq : Function.Surjective q) (n : ℕ) :
    ∃ U : OpenNormalSubgroup
      (maximalRealProPOutside p T ≃ₐ[ℚ] maximalRealProPOutside p T),
      ∀ v : HeightOneSpectrum (𝓞 ℚ),
        FinitePlaceSplitsCompletely (K := ℚ) (L := (realProPOpenNormalStage p T U).val) v →
          ∃ f : F, q f = maximalRealProPArithmeticFrobenius p T v ∧
            ZassenhausDepthAtLeast p n f

Module documentation

Split finite stages and deep arithmetic Frobenius lifts

Declarations

depthStageIsGalois

maximalRealProPArithmeticFrobenius_stageRestriction_eq_one

exists_realProPOpenNormalStage_with_deep_frobenius_lifts