NYLL
Module

RealProPFrobenius.lean

Nyll.SawinTotallyRealTowers.RealProPFrobenius
7 declarations indexed from sourceView source ↗

Module documentation

Frobenius in the actual maximal real pro-p extension

Outside the allowed support inertia acts trivially. Consequently the actual decomposition map factors through its residue-degree quotient; killing arithmetic Frobenius kills its entire decomposition image.

Imports6
Imported by6

Declarations

def

maximalRealProPDecompositionMap

L34 ↗
ClassFieldTower.Sawin.maximalRealProPDecompositionMap
Documentation

The actual image of an absolute decomposition element in the maximal real group.

Source context 7 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich
variable (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ)))
variable (v : HeightOneSpectrum (𝓞 ℚ))
Lean source · statement
def maximalRealProPDecompositionMap :
    finitePlaceAbsoluteDecompositionGroup ℚ v →ₜ*
      (maximalRealProPOutside p T ≃ₐ[ℚ] maximalRealProPOutside p T)
def

maximalRealProPArithmeticFrobenius

L41 ↗
ClassFieldTower.Sawin.maximalRealProPArithmeticFrobenius
Documentation

The chosen arithmetic Frobenius as an element of the actual arithmetic group.

Source context 7 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich
variable (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ)))
variable (v : HeightOneSpectrum (𝓞 ℚ))
Lean source · statement
def maximalRealProPArithmeticFrobenius :
    maximalRealProPOutside p T ≃ₐ[ℚ] maximalRealProPOutside p T
theorem

maximalRealProPDecompositionMap_inertia_ker

L46 ↗
ClassFieldTower.Sawin.maximalRealProPDecompositionMap_inertia_ker
Documentation

Outside T the actual decomposition map kills absolute inertia.

Source context 7 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich
variable (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ)))
variable (v : HeightOneSpectrum (𝓞 ℚ))
Lean source · statement
theorem maximalRealProPDecompositionMap_inertia_ker (hv : v ∉ T) :
    finitePlaceAbsoluteInertiaSubgroup ℚ v ≤
      (maximalRealProPDecompositionMap p T v).toMonoidHom.ker
def

maximalRealProPUnramifiedDecompositionMap

L53 ↗
ClassFieldTower.Sawin.maximalRealProPUnramifiedDecompositionMap
Documentation

The actual decomposition map on the quotient by inertia.

Source context 7 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich
variable (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ)))
variable (v : HeightOneSpectrum (𝓞 ℚ))
Lean source · statement
def maximalRealProPUnramifiedDecompositionMap (hv : v ∉ T) :
    (finitePlaceAbsoluteDecompositionGroup ℚ v ⧸
      finitePlaceAbsoluteInertiaSubgroup ℚ v) →ₜ*
      (maximalRealProPOutside p T ≃ₐ[ℚ] maximalRealProPOutside p T)
theorem

maximalRealProPUnramifiedDecompositionMap_mk

L62 ↗
ClassFieldTower.Sawin.maximalRealProPUnramifiedDecompositionMap_mk
Source context 7 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich
variable (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ)))
variable (v : HeightOneSpectrum (𝓞 ℚ))
Lean source · statement
theorem maximalRealProPUnramifiedDecompositionMap_mk (hv : v ∉ T)
    (sigma : finitePlaceAbsoluteDecompositionGroup ℚ v) :
    maximalRealProPUnramifiedDecompositionMap p T v hv
        (QuotientGroup.mk' (finitePlaceAbsoluteInertiaSubgroup ℚ v) sigma) =
      maximalRealProPDecompositionMap p T v sigma
theorem

maximalRealProPFrobenius_eq_classMap

L69 ↗
ClassFieldTower.Sawin.maximalRealProPFrobenius_eq_classMap
Documentation

The unramified class maps to the same actual arithmetic Frobenius.

Source context 7 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich
variable (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ)))
variable (v : HeightOneSpectrum (𝓞 ℚ))
Lean source · statement
theorem maximalRealProPFrobenius_eq_classMap (hv : v ∉ T) :
    maximalRealProPArithmeticFrobenius p T v =
      maximalRealProPUnramifiedDecompositionMap p T v hv
        (finitePlaceArithmeticFrobeniusClass ℚ v)
theorem

maximalRealProPDecomposition_killed_of_frobenius

L78 ↗
ClassFieldTower.Sawin.maximalRealProPDecomposition_killed_of_frobenius
Documentation

Killing Frobenius in any Hausdorff continuous quotient kills the whole decomposition image, since inertia already acts trivially.

Source context 7 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich
variable (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ)))
variable (v : HeightOneSpectrum (𝓞 ℚ))
Lean source · statement
theorem maximalRealProPDecomposition_killed_of_frobenius
    (hv : v ∉ T) {H : Type*} [Group H] [TopologicalSpace H]
    [IsTopologicalGroup H] [T2Space H]
    (q : (maximalRealProPOutside p T ≃ₐ[ℚ] maximalRealProPOutside p T) →ₜ* H)
    (hq : q (maximalRealProPArithmeticFrobenius p T v) = 1)
    (sigma : finitePlaceAbsoluteDecompositionGroup ℚ v) :
    q (maximalRealProPDecompositionMap p T v sigma) = 1

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.