NYLL
Module

ArithmeticStageH2AdditionDifference.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.ArithmeticStageH2AdditionDifference
6 declarations indexed from sourceView source ↗

Module documentation

The actual global character measuring nonadditivity of chosen lifts

Adding coefficient coordinates solves the embedding problem of the sum class. Its difference from the chosen solution is a global character, and all three lifts are unramified outside the fixed stage support. On inertia this character is exactly the additivity defect of the local characters.

Imports3
Imported by2

Declarations

instance

arithmeticStageH2AdditionCanonicalZModAddCommGroup

L31 ↗
ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2AdditionCanonicalZModAddCommGroup
Source context 8 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.ProP ClassFieldTower.Martinet ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
Lean source · statement
instance arithmeticStageH2AdditionCanonicalZModAddCommGroup :
    AddCommGroup (ZMod (n : ℕ))
def

arithmeticStageH2AbsoluteAddLift

L44 ↗
ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2AbsoluteAddLift
Documentation

A solution for the sum class, constructed by adding the two chosen solutions.

Source context 12 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.ProP ClassFieldTower.Martinet ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local instance arithmeticStageH2AdditionCanonicalZModAddCommGroup :
    AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
local notation "StageQuotient" => MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
  (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
variable (x y : continuousCohomologyZModPLifted (n : ℕ)
  (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
    (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))) 2)
include hpOdd x y
Lean source · statement
def arithmeticStageH2AbsoluteAddLift :
    Field.absoluteGaloisGroup F →ₜ* DegreeTwoCentralExtension (p := (n : ℕ))
      (Q := StageQuotient) (x + y)
theorem

arithmeticStageH2AbsoluteAddLift_projection

L54 ↗
ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2AbsoluteAddLift_projection
Documentation

The constructed sum lift has the same actual finite-stage projection.

Source context 12 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.ProP ClassFieldTower.Martinet ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local instance arithmeticStageH2AdditionCanonicalZModAddCommGroup :
    AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
local notation "StageQuotient" => MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
  (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
variable (x y : continuousCohomologyZModPLifted (n : ℕ)
  (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
    (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))) 2)
include hpOdd x y
Lean source · statement
theorem arithmeticStageH2AbsoluteAddLift_projection :
    (H2CocycleExtension.projection (degreeTwoCocycleRepresentative (p := (n : ℕ))
      (Q := StageQuotient) (x + y))).comp
      (arithmeticStageH2AbsoluteAddLift F n hpOdd U x y) =
        arithmeticStageAbsoluteQuotientMap F n U
def

arithmeticStageH2AdditionDifference

L63 ↗
ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2AdditionDifference
Documentation

The continuous absolute character measuring the chosen lifts' additivity defect.

Source context 12 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.ProP ClassFieldTower.Martinet ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local instance arithmeticStageH2AdditionCanonicalZModAddCommGroup :
    AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
local notation "StageQuotient" => MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
  (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
variable (x y : continuousCohomologyZModPLifted (n : ℕ)
  (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
    (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))) 2)
include hpOdd x y
Lean source · statement
def arithmeticStageH2AdditionDifference :
    Field.absoluteGaloisGroup F →ₜ* Multiplicative (ZMod (n : ℕ))
theorem

arithmeticStageH2AdditionDifference_inertia_of_not_mem

L72 ↗
ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2AdditionDifference_inertia_of_not_mem
Documentation

No new ramification is introduced outside the common finite support.

Source context 12 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.ProP ClassFieldTower.Martinet ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local instance arithmeticStageH2AdditionCanonicalZModAddCommGroup :
    AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
local notation "StageQuotient" => MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
  (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
variable (x y : continuousCohomologyZModPLifted (n : ℕ)
  (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
    (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))) 2)
include hpOdd x y
Lean source · statement
theorem arithmeticStageH2AdditionDifference_inertia_of_not_mem
    (v : HeightOneSpectrum (𝓞 F))
    (hv : v ∉ arithmeticStageH2UniformRamifiedPlaces F n hpOdd U)
    (sigma : finitePlaceAbsoluteInertiaSubgroup F v) :
    arithmeticStageH2AdditionDifference F n hpOdd U x y
      (finitePlaceAbsoluteDecompositionInclusion F v sigma.1) = 1
theorem

arithmeticStageH2AdditionDifference_inertia

L96 ↗
ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2AdditionDifference_inertia
Documentation

On inertia, the local additivity defect is the restriction of the actual global defect.

Source context 12 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.ProP ClassFieldTower.Martinet ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local instance arithmeticStageH2AdditionCanonicalZModAddCommGroup :
    AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
local notation "StageQuotient" => MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
  (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
variable (x y : continuousCohomologyZModPLifted (n : ℕ)
  (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
    (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))) 2)
include hpOdd x y
Lean source · statement
theorem arithmeticStageH2AdditionDifference_inertia
    (v : HeightOneSpectrum (𝓞 F)) (sigma : finitePlaceAbsoluteInertiaSubgroup F v) :
    (arithmeticStageH2GlobalLocalDifferenceCharacter F n hpOdd U (x + y) v sigma.1).toAdd -
      ((arithmeticStageH2GlobalLocalDifferenceCharacter F n hpOdd U x v sigma.1).toAdd +
        (arithmeticStageH2GlobalLocalDifferenceCharacter F n hpOdd U y v sigma.1).toAdd) =
      (arithmeticStageH2AdditionDifference F n hpOdd U x y
        (finitePlaceAbsoluteDecompositionInclusion F v sigma.1)).toAdd

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