Module

FinitePlaceFrobenius.lean

Nyll.SawinTotallyRealTowers.FinitePlaceFrobenius

6 declarations indexed from sourceView source ↗

Module documentation

Arithmetic Frobenius in an absolute decomposition group

The existing local residue comparison identifies the quotient by inertia with the profinite integers. The class of arithmetic Frobenius is the inverse image of additive one, and a representative is chosen in the actual absolute decomposition group.

Imports3

Imported by3

def

finitePlaceUnramifiedDegreeEquiv

L33 ↗

ClassFieldTower.Sawin.finitePlaceUnramifiedDegreeEquiv

Documentation

The unramified absolute decomposition quotient has its actual residue degree.

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 ClassFieldTower.Martinet.Shafarevich ClassFormation
open AlgebraicNumberTheory.Valuations ProCGroups.Generation
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (𝓞 F))

Lean source · statement

def finitePlaceUnramifiedDegreeEquiv :
    (finitePlaceAbsoluteDecompositionGroup F v ⧸
      finitePlaceAbsoluteInertiaSubgroup F v) ≃ₜ* ZHatMul

def

finitePlaceArithmeticFrobeniusClass

L46 ↗

ClassFieldTower.Sawin.finitePlaceArithmeticFrobeniusClass

Documentation

The residue-degree-one class of arithmetic Frobenius.

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 ClassFieldTower.Martinet.Shafarevich ClassFormation
open AlgebraicNumberTheory.Valuations ProCGroups.Generation
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (𝓞 F))

Lean source · statement

def finitePlaceArithmeticFrobeniusClass :
    finitePlaceAbsoluteDecompositionGroup F v ⧸ finitePlaceAbsoluteInertiaSubgroup F v

def

finitePlaceArithmeticFrobeniusLift

L51 ↗

ClassFieldTower.Sawin.finitePlaceArithmeticFrobeniusLift

Documentation

An actual absolute decomposition element representing arithmetic Frobenius.

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 ClassFieldTower.Martinet.Shafarevich ClassFormation
open AlgebraicNumberTheory.Valuations ProCGroups.Generation
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (𝓞 F))

Lean source · statement

def finitePlaceArithmeticFrobeniusLift : finitePlaceAbsoluteDecompositionGroup F v

theorem

finitePlaceArithmeticFrobeniusLift_mk

L56 ↗

ClassFieldTower.Sawin.finitePlaceArithmeticFrobeniusLift_mk

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 ClassFieldTower.Martinet.Shafarevich ClassFormation
open AlgebraicNumberTheory.Valuations ProCGroups.Generation
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (𝓞 F))

Lean source · statement

theorem finitePlaceArithmeticFrobeniusLift_mk :
    QuotientGroup.mk' (finitePlaceAbsoluteInertiaSubgroup F v)
        (finitePlaceArithmeticFrobeniusLift F v) =
      finitePlaceArithmeticFrobeniusClass F v

theorem

finitePlaceArithmeticFrobeniusLift_degree

L64 ↗

ClassFieldTower.Sawin.finitePlaceArithmeticFrobeniusLift_degree

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 ClassFieldTower.Martinet.Shafarevich ClassFormation
open AlgebraicNumberTheory.Valuations ProCGroups.Generation
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (𝓞 F))

Lean source · statement

theorem finitePlaceArithmeticFrobeniusLift_degree :
    finitePlaceUnramifiedDegreeEquiv F v
      (QuotientGroup.mk' (finitePlaceAbsoluteInertiaSubgroup F v)
        (finitePlaceArithmeticFrobeniusLift F v)) = Multiplicative.ofAdd (1 : ZHat)

theorem

finitePlaceArithmeticFrobeniusClass_topologicallyGenerates

L72 ↗

ClassFieldTower.Sawin.finitePlaceArithmeticFrobeniusClass_topologicallyGenerates

Documentation

The chosen Frobenius class generates the whole unramified decomposition 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 ClassFieldTower.Martinet.Shafarevich ClassFormation
open AlgebraicNumberTheory.Valuations ProCGroups.Generation
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (𝓞 F))

Lean source · statement

theorem finitePlaceArithmeticFrobeniusClass_topologicallyGenerates :
    ProCGroups.Generation.TopologicallyGenerates
      ({finitePlaceArithmeticFrobeniusClass F v} :
        Set (finitePlaceAbsoluteDecompositionGroup F v ⧸
          finitePlaceAbsoluteInertiaSubgroup F v))

Module documentation

Arithmetic Frobenius in an absolute decomposition group

Declarations

finitePlaceUnramifiedDegreeEquiv

finitePlaceArithmeticFrobeniusClass

finitePlaceArithmeticFrobeniusLift

finitePlaceArithmeticFrobeniusLift_mk

finitePlaceArithmeticFrobeniusLift_degree

finitePlaceArithmeticFrobeniusClass_topologicallyGenerates