Module

ArithmeticStageH2FinitePlaceDefect.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.ArithmeticStageH2FinitePlaceDefect

11 declarations indexed from sourceView source ↗

Module documentation

Finite-place splitting defects of arithmetic-stage H² embedding problems

At a finite place, restrict the arithmetic-stage quotient to its chosen decomposition group. The restricted degree-two class is the local splitting defect: it vanishes exactly when the pulled-back central extension has a continuous section.

Imports4

Imported by1

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.All

abbrev

ArithmeticStageFinitePlaceDecompositionGroup

L35 ↗

ClassFieldTower.Martinet.Shafarevich.ArithmeticStageFinitePlaceDecompositionGroup

Documentation

The chosen finite-place decomposition group of an arithmetic stage.

Source context 8 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet
open ProCGroups ProCGroups.ProC
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

abbrev ArithmeticStageFinitePlaceDecompositionGroup
    (hpOdd : Odd p)
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p))
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F))

def

arithmeticStageFinitePlaceDecompositionInclusion

L45 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticStageFinitePlaceDecompositionInclusion

Documentation

Inclusion of the chosen decomposition group into the arithmetic-stage Galois group.

Source context 8 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet
open ProCGroups ProCGroups.ProC
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

def arithmeticStageFinitePlaceDecompositionInclusion
    (hpOdd : Odd p)
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p))
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    ArithmeticStageFinitePlaceDecompositionGroup F p hpOdd U v →ₜ*
      ((openNormalArithmeticStage F p hpOdd U).field ≃ₐ[F]
        (openNormalArithmeticStage F p hpOdd U).field)

def

arithmeticStageFinitePlaceQuotientInclusion

L57 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticStageFinitePlaceQuotientInclusion

Documentation

The decomposition-group inclusion transported back to the open-normal quotient of the maximal everywhere-unramified pro-p group.

Source context 8 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet
open ProCGroups ProCGroups.ProC
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

def arithmeticStageFinitePlaceQuotientInclusion
    (hpOdd : Odd p)
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p))
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    ArithmeticStageFinitePlaceDecompositionGroup F p hpOdd U v →ₜ*
      (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
        (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p)))

def

arithmeticStageFinitePlaceH2Localization

L71 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticStageFinitePlaceH2Localization

Documentation

Restriction of stage H² to a chosen finite-place decomposition group.

Source context 8 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet
open ProCGroups ProCGroups.ProC
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

def arithmeticStageFinitePlaceH2Localization
    (hpOdd : Odd p)
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p))
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    continuousCohomologyZModPLifted p
        (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
          (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) 2 →ₗ[ZMod p]
      continuousCohomologyZModPLifted p
        (ArithmeticStageFinitePlaceDecompositionGroup F p hpOdd U v) 2

abbrev

ArithmeticStageFinitePlaceH2Defect

L85 ↗

ClassFieldTower.Martinet.Shafarevich.ArithmeticStageFinitePlaceH2Defect

Documentation

The prime-wise splitting defect of a stage class.

Source context 8 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet
open ProCGroups ProCGroups.ProC
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

abbrev ArithmeticStageFinitePlaceH2Defect
    (hpOdd : Odd p)
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p))
    (xU : continuousCohomologyZModPLifted p
      (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
        (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) 2)
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F))

theorem

arithmeticStageFinitePlaceH2Localization_apply

L96 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticStageFinitePlaceH2Localization_apply

Source context 8 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet
open ProCGroups ProCGroups.ProC
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

theorem arithmeticStageFinitePlaceH2Localization_apply
    (hpOdd : Odd p)
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p))
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F))
    (xU : continuousCohomologyZModPLifted p
      (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
        (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) 2) :
    arithmeticStageFinitePlaceH2Localization F p hpOdd U v xU =
      continuousCohomologyZModPMapLifted p
        (arithmeticStageFinitePlaceQuotientInclusion F p hpOdd U v) 2 xU

def

arithmeticStageFinitePlaceRestrictedCocycle

L112 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticStageFinitePlaceRestrictedCocycle

Documentation

The chosen stage cocycle restricted to the finite-place decomposition group. Its extension is the cocycle pullback of the arithmetic embedding problem.

Source context 8 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet
open ProCGroups ProCGroups.ProC
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

def arithmeticStageFinitePlaceRestrictedCocycle
    (hpOdd : Odd p)
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p))
    (xU : continuousCohomologyZModPLifted p
      (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
        (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) 2)
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    trivialZModPCocyclesLifted p
      (ArithmeticStageFinitePlaceDecompositionGroup F p hpOdd U v) 2

def

ArithmeticStageH2LocallySplitAt

L128 ↗

ClassFieldTower.Martinet.Shafarevich.ArithmeticStageH2LocallySplitAt

Documentation

Local splitting means that the pulled-back cocycle extension over the decomposition group has a continuous section.

Source context 8 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet
open ProCGroups ProCGroups.ProC
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

def ArithmeticStageH2LocallySplitAt
    (hpOdd : Odd p)
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p))
    (xU : continuousCohomologyZModPLifted p
      (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
        (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) 2)
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) : Prop

theorem

arithmeticStageFinitePlaceRestrictedCocycle_π

L145 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticStageFinitePlaceRestrictedCocycle_π

Documentation

The cohomology class of the restricted stage cocycle is exactly the finite-place splitting defect.

Source context 8 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet
open ProCGroups ProCGroups.ProC
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

theorem arithmeticStageFinitePlaceRestrictedCocycle_π
    (hpOdd : Odd p)
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p))
    (xU : continuousCohomologyZModPLifted p
      (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
        (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) 2)
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    ContinuousCohomology.π
        (trivialZModPLifted p
          (ArithmeticStageFinitePlaceDecompositionGroup F p hpOdd U v)) 2
        (arithmeticStageFinitePlaceRestrictedCocycle F p hpOdd U xU v) =
      ArithmeticStageFinitePlaceH2Defect F p hpOdd U xU v

theorem

arithmeticStageH2LocallySplitAt_iff_defect_eq_zero

L181 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2LocallySplitAt_iff_defect_eq_zero

Documentation

The local defect vanishes exactly when the pulled-back central embedding problem splits over the chosen decomposition group.

Source context 8 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet
open ProCGroups ProCGroups.ProC
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

theorem arithmeticStageH2LocallySplitAt_iff_defect_eq_zero
    (hpOdd : Odd p)
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p))
    (xU : continuousCohomologyZModPLifted p
      (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
        (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) 2)
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    ArithmeticStageH2LocallySplitAt F p hpOdd U xU v ↔
      ArithmeticStageFinitePlaceH2Defect F p hpOdd U xU v = 0

theorem

arithmeticStageH2LocallySplitAt_allFinitePlaces_iff

L202 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2LocallySplitAt_allFinitePlaces_iff

Documentation

The stage embedding problem is locally split at every finite place exactly when every prime-wise defect vanishes.

Source context 8 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet
open ProCGroups ProCGroups.ProC
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

theorem arithmeticStageH2LocallySplitAt_allFinitePlaces_iff
    (hpOdd : Odd p)
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p))
    (xU : continuousCohomologyZModPLifted p
      (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
        (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) 2) :
    (∀ v, ArithmeticStageH2LocallySplitAt F p hpOdd U xU v) ↔
      ∀ v, ArithmeticStageFinitePlaceH2Defect F p hpOdd U xU v = 0

Module documentation

Finite-place splitting defects of arithmetic-stage H² embedding problems

Declarations