Module

RealProPFrobeniusCut.lean

Nyll.SawinTotallyRealTowers.RealProPFrobeniusCut

6 declarations indexed from sourceView source ↗

Module documentation

Killing a countable family of actual Frobenius elements

The closed normal subgroup generated by the chosen arithmetic Frobenii has a Hausdorff group quotient. At primes outside the allowed ramification support, its projection kills the whole absolute decomposition group.

Imports4

Imported by4

abbrev

realProPFrobeniusCutKernel

ClassFieldTower.Sawin.realProPFrobeniusCutKernel

Documentation

The closed normal subgroup generated by actual arithmetic Frobenii.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Sawin
open ProCGroups.Presentations
open ClassFieldTower.Martinet.Shafarevich
variable (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ)))
variable (v : ℕ → HeightOneSpectrum (𝓞 ℚ))

Lean source · statement

abbrev realProPFrobeniusCutKernel :
    Subgroup (maximalRealProPOutside p T ≃ₐ[ℚ] maximalRealProPOutside p T)

abbrev

RealProPFrobeniusCut

ClassFieldTower.Sawin.RealProPFrobeniusCut

Documentation

The actual maximal real group after the selected Frobenii are killed.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Sawin
open ProCGroups.Presentations
open ClassFieldTower.Martinet.Shafarevich
variable (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ)))
variable (v : ℕ → HeightOneSpectrum (𝓞 ℚ))

Lean source · statement

abbrev RealProPFrobeniusCut

def

realProPFrobeniusCutProjection

ClassFieldTower.Sawin.realProPFrobeniusCutProjection

Documentation

The continuous projection to the actual Frobenius quotient.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Sawin
open ProCGroups.Presentations
open ClassFieldTower.Martinet.Shafarevich
variable (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ)))
variable (v : ℕ → HeightOneSpectrum (𝓞 ℚ))

Lean source · statement

def realProPFrobeniusCutProjection :
    (maximalRealProPOutside p T ≃ₐ[ℚ] maximalRealProPOutside p T) →ₜ*
      RealProPFrobeniusCut p T v

theorem

realProPFrobeniusCutProjection_frobenius

ClassFieldTower.Sawin.realProPFrobeniusCutProjection_frobenius

Documentation

Every selected arithmetic Frobenius is killed by the quotient projection.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Sawin
open ProCGroups.Presentations
open ClassFieldTower.Martinet.Shafarevich
variable (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ)))
variable (v : ℕ → HeightOneSpectrum (𝓞 ℚ))

Lean source · statement

theorem realProPFrobeniusCutProjection_frobenius (n : ℕ) :
    realProPFrobeniusCutProjection p T v
      (maximalRealProPArithmeticFrobenius p T (v n)) = 1

theorem

realProPFrobeniusCutProjection_decomposition

ClassFieldTower.Sawin.realProPFrobeniusCutProjection_decomposition

Documentation

At a selected prime outside T the entire actual decomposition image is killed.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Sawin
open ProCGroups.Presentations
open ClassFieldTower.Martinet.Shafarevich
variable (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ)))
variable (v : ℕ → HeightOneSpectrum (𝓞 ℚ))

Lean source · statement

theorem realProPFrobeniusCutProjection_decomposition (n : ℕ) (hv : v n ∉ T)
    (sigma : finitePlaceAbsoluteDecompositionGroup ℚ (v n)) :
    realProPFrobeniusCutProjection p T v
      (maximalRealProPDecompositionMap p T (v n) sigma) = 1

theorem

realProPFrobeniusCutProjection_surjective

ClassFieldTower.Sawin.realProPFrobeniusCutProjection_surjective

Documentation

The actual Frobenius quotient is the image of its arithmetic parent group.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Sawin
open ProCGroups.Presentations
open ClassFieldTower.Martinet.Shafarevich
variable (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ)))
variable (v : ℕ → HeightOneSpectrum (𝓞 ℚ))

Lean source · statement

theorem realProPFrobeniusCutProjection_surjective :
    Function.Surjective (realProPFrobeniusCutProjection p T v)