NYLL
Module

ArithmeticStageH2GlobalLift.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.ArithmeticStageH2GlobalLift
13 declarations indexed from sourceView source ↗

Module documentation

Actual global lifts and their finite ramification defect

The proved vanishing of absolute inflation supplies an actual continuous global solution of every finite arithmetic-stage central embedding problem. Restricting it to decomposition groups and subtracting the constructed unramified local solution produces local characters. Their inertia parts are supported on a finite set, by the open-kernel fixed-field argument.

The local difference character, its inertia restriction, and the finite set are explicit chosen objects with proved projection and support laws. Only one local compactness proof is introduced; all algebra structures and finite-stage certificates are inherited from the existing sources.

Imports3
Imported by2

Declarations

def

arithmeticStageAbsoluteQuotientMap

L41 ↗
ClassFieldTower.Martinet.Shafarevich.arithmeticStageAbsoluteQuotientMap
Documentation

Actual absolute restriction to the finite open-normal quotient.

Source context 10 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet ClassFieldTower.ProP
open ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
variable (xU : continuousCohomologyZModPLifted (n : ℕ)
  (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
    (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))) 2)
Lean source · statement
def arithmeticStageAbsoluteQuotientMap :
    Field.absoluteGaloisGroup F →ₜ*
      (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
        (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ))))
theorem

arithmeticStageH2_exists_absoluteGlobalLift

L51 ↗
ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2_exists_absoluteGlobalLift
Documentation

Every finite arithmetic-stage cocycle extension has a global solution.

Source context 11 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet ClassFieldTower.ProP
open ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
variable (xU : continuousCohomologyZModPLifted (n : ℕ)
  (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
    (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))) 2)
include hpOdd
Lean source · statement
theorem arithmeticStageH2_exists_absoluteGlobalLift :
    ∃ s : Field.absoluteGaloisGroup F →ₜ* DegreeTwoCentralExtension xU,
      (H2CocycleExtension.projection (degreeTwoCocycleRepresentative xU)).comp s =
        arithmeticStageAbsoluteQuotientMap F n U
def

arithmeticStageH2AbsoluteGlobalLift

L67 ↗
ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2AbsoluteGlobalLift
Documentation

A chosen actual global lift supplied by absolute degree-two vanishing.

Source context 11 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet ClassFieldTower.ProP
open ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
variable (xU : continuousCohomologyZModPLifted (n : ℕ)
  (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
    (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))) 2)
include hpOdd
Lean source · statement
def arithmeticStageH2AbsoluteGlobalLift :
    Field.absoluteGaloisGroup F →ₜ* DegreeTwoCentralExtension xU
theorem

arithmeticStageH2AbsoluteGlobalLift_projection

L72 ↗
ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2AbsoluteGlobalLift_projection
Documentation

The global lift has the required finite-stage projection.

Source context 11 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet ClassFieldTower.ProP
open ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
variable (xU : continuousCohomologyZModPLifted (n : ℕ)
  (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
    (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))) 2)
include hpOdd
Lean source · statement
theorem arithmeticStageH2AbsoluteGlobalLift_projection :
    (H2CocycleExtension.projection (degreeTwoCocycleRepresentative xU)).comp
      (arithmeticStageH2AbsoluteGlobalLift F n hpOdd U xU) =
        arithmeticStageAbsoluteQuotientMap F n U
def

arithmeticStageH2GlobalLiftAtFinitePlace

L79 ↗
ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2GlobalLiftAtFinitePlace
Documentation

Restriction of the actual global lift to a finite decomposition group.

Source context 11 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet ClassFieldTower.ProP
open ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
variable (xU : continuousCohomologyZModPLifted (n : ℕ)
  (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
    (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))) 2)
include hpOdd
Lean source · statement
def arithmeticStageH2GlobalLiftAtFinitePlace
    (v : HeightOneSpectrum (𝓞 F)) :
    finitePlaceAbsoluteDecompositionGroup F v →ₜ* DegreeTwoCentralExtension xU
theorem

arithmeticStageH2GlobalLiftAtFinitePlace_projection

L86 ↗
ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2GlobalLiftAtFinitePlace_projection
Documentation

The restricted global solution has the prescribed local projection.

Source context 11 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet ClassFieldTower.ProP
open ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
variable (xU : continuousCohomologyZModPLifted (n : ℕ)
  (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
    (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))) 2)
include hpOdd
Lean source · statement
theorem arithmeticStageH2GlobalLiftAtFinitePlace_projection
    (v : HeightOneSpectrum (𝓞 F)) :
    (H2CocycleExtension.projection (degreeTwoCocycleRepresentative xU)).comp
      (arithmeticStageH2GlobalLiftAtFinitePlace F n hpOdd U xU v) =
        arithmeticStageFinitePlaceAbsoluteQuotientMap F (n : ℕ) U v
def

arithmeticStageH2GlobalRamificationCharacter

L97 ↗
ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2GlobalRamificationCharacter
Documentation

The inertia character recording ramification of the chosen global lift.

Source context 11 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet ClassFieldTower.ProP
open ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
variable (xU : continuousCohomologyZModPLifted (n : ℕ)
  (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
    (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))) 2)
include hpOdd
Lean source · statement
def arithmeticStageH2GlobalRamificationCharacter
    (v : HeightOneSpectrum (𝓞 F)) :
    finitePlaceAbsoluteInertiaSubgroup F v →ₜ* Multiplicative (ZMod (n : ℕ))
theorem

arithmeticStageH2GlobalRamificationCharacter_support_finite

L105 ↗
ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2GlobalRamificationCharacter_support_finite
Documentation

The actual global lift's inertia defect is supported at finitely many places.

Source context 11 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet ClassFieldTower.ProP
open ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
variable (xU : continuousCohomologyZModPLifted (n : ℕ)
  (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
    (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))) 2)
include hpOdd
Lean source · statement
theorem arithmeticStageH2GlobalRamificationCharacter_support_finite :
    {v : HeightOneSpectrum (𝓞 F) |
      arithmeticStageH2GlobalRamificationCharacter F n hpOdd U xU v ≠ 1}.Finite
def

arithmeticStageH2GlobalLocalDifferenceCharacter

L121 ↗
ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2GlobalLocalDifferenceCharacter
Documentation

A character on the full decomposition group extending the inertia defect.

Source context 11 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet ClassFieldTower.ProP
open ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
variable (xU : continuousCohomologyZModPLifted (n : ℕ)
  (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
    (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))) 2)
include hpOdd
Lean source · statement
def arithmeticStageH2GlobalLocalDifferenceCharacter
    (v : HeightOneSpectrum (𝓞 F)) :
    finitePlaceAbsoluteDecompositionGroup F v →ₜ* Multiplicative (ZMod (n : ℕ))
theorem

arithmeticStageH2GlobalLocalDifferenceCharacter_inertia

L131 ↗
ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2GlobalLocalDifferenceCharacter_inertia
Documentation

Subtracting the unramified local lift gives the actual inertia defect.

Source context 11 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet ClassFieldTower.ProP
open ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
variable (xU : continuousCohomologyZModPLifted (n : ℕ)
  (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
    (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))) 2)
include hpOdd
Lean source · statement
theorem arithmeticStageH2GlobalLocalDifferenceCharacter_inertia
    (v : HeightOneSpectrum (𝓞 F)) :
    (arithmeticStageH2GlobalLocalDifferenceCharacter F n hpOdd U xU v).comp
      (finitePlaceAbsoluteInertiaInclusion F v) =
        arithmeticStageH2GlobalRamificationCharacter F n hpOdd U xU v
def

arithmeticStageH2GlobalRamifiedPlaces

L138 ↗
ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2GlobalRamifiedPlaces
Documentation

The finite set of places with nontrivial inertia defect.

Source context 11 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet ClassFieldTower.ProP
open ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
variable (xU : continuousCohomologyZModPLifted (n : ℕ)
  (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
    (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))) 2)
include hpOdd
Lean source · statement
def arithmeticStageH2GlobalRamifiedPlaces : Finset (HeightOneSpectrum (𝓞 F))
theorem

arithmeticStageH2GlobalRamificationCharacter_eq_one_of_not_mem

L142 ↗
ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2GlobalRamificationCharacter_eq_one_of_not_mem
Documentation

Outside the named finite set, the inertia character is trivial.

Source context 11 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet ClassFieldTower.ProP
open ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
variable (xU : continuousCohomologyZModPLifted (n : ℕ)
  (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
    (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))) 2)
include hpOdd
Lean source · statement
theorem arithmeticStageH2GlobalRamificationCharacter_eq_one_of_not_mem
    (v : HeightOneSpectrum (𝓞 F))
    (hv : v ∉ arithmeticStageH2GlobalRamifiedPlaces F n hpOdd U xU) :
    arithmeticStageH2GlobalRamificationCharacter F n hpOdd U xU v = 1
theorem

arithmeticStageH2GlobalLiftAtFinitePlace_inertia_le_ker_of_not_mem

L150 ↗
ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2GlobalLiftAtFinitePlace_inertia_le_ker_of_not_mem
Documentation

The chosen global solution is unramified outside its named finite set.

Source context 11 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet ClassFieldTower.ProP
open ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
variable (xU : continuousCohomologyZModPLifted (n : ℕ)
  (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
    (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))) 2)
include hpOdd
Lean source · statement
theorem arithmeticStageH2GlobalLiftAtFinitePlace_inertia_le_ker_of_not_mem
    (v : HeightOneSpectrum (𝓞 F))
    (hv : v ∉ arithmeticStageH2GlobalRamifiedPlaces F n hpOdd U xU) :
    finitePlaceAbsoluteInertiaSubgroup F v ≤
      (arithmeticStageH2GlobalLiftAtFinitePlace F n hpOdd U xU v).toMonoidHom.ker

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