NYLL
Module

CyclotomicAbsoluteH2Vanishing.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.CyclotomicAbsoluteH2Vanishing
7 declarations indexed from sourceView source ↗

Module documentation

Absolute inflation vanishes over every number field

The actual cyclotomic base change of an unramified arithmetic stage is mapped into the standard cyclotomic algebraic closure using exactly the equivalence underlying finite-extension absolute restriction. Evaluation on field elements proves the restriction square. The mapped stage has zero absolute H², and prime-to-p cyclotomic restriction is injective.

Thus no primitive-root hypothesis remains. Finite-stage realization then shows that every continuous degree-two class of the maximal everywhere- unramified pro-p group vanishes on the absolute Galois group, for odd p. Only two local proposition-valued instances name the finite cyclotomic base and its number-field certificate; no comparison assumption is used.

Imports5
Imported by2

Declarations

instance

cyclotomicVanishingBaseFinite

L44 ↗
ClassFieldTower.Martinet.Shafarevich.cyclotomicVanishingBaseFinite
Source context 9 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet ClassFieldTower.ProP ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local notation "Cyclo" => IdealRadicalCyclotomicBase F (n : ℕ) (Fact.out : Nat.Prime (n : ℕ))
local notation "OriginalStage" => FiniteEverywhereUnramifiedProPExtension.field
  (openNormalArithmeticStage F (n : ℕ) hpOdd U)
Lean source · statement
instance cyclotomicVanishingBaseFinite : FiniteDimensional F Cyclo
instance

cyclotomicVanishingBaseNumber

L47 ↗
ClassFieldTower.Martinet.Shafarevich.cyclotomicVanishingBaseNumber
Source context 10 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet ClassFieldTower.ProP ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local notation "Cyclo" => IdealRadicalCyclotomicBase F (n : ℕ) (Fact.out : Nat.Prime (n : ℕ))
local notation "OriginalStage" => FiniteEverywhereUnramifiedProPExtension.field
  (openNormalArithmeticStage F (n : ℕ) hpOdd U)
local instance cyclotomicVanishingBaseFinite : FiniteDimensional F Cyclo :=
  finiteDimensional_idealRadicalCyclotomicBase F (n : ℕ) Fact.out
Lean source · statement
instance cyclotomicVanishingBaseNumber : NumberField Cyclo
def

cyclotomicArithmeticStageRestrictionContinuous

L56 ↗
ClassFieldTower.Martinet.Shafarevich.cyclotomicArithmeticStageRestrictionContinuous
Documentation

Actual finite restriction from the synchronized cyclotomic stage, viewed as a continuous homomorphism between finite Galois groups.

Source context 13 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet ClassFieldTower.ProP ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local notation "Cyclo" => IdealRadicalCyclotomicBase F (n : ℕ) (Fact.out : Nat.Prime (n : ℕ))
local notation "OriginalStage" => FiniteEverywhereUnramifiedProPExtension.field
  (openNormalArithmeticStage F (n : ℕ) hpOdd U)
local instance cyclotomicVanishingBaseFinite : FiniteDimensional F Cyclo :=
  finiteDimensional_idealRadicalCyclotomicBase F (n : ℕ) Fact.out
local instance cyclotomicVanishingBaseNumber : NumberField Cyclo :=
  NumberField.of_module_finite F Cyclo
local notation "closureEquiv" => finiteIntermediateAbsoluteClosureEquiv F Cyclo
local notation "MappedStage" =>
  cyclotomicArithmeticStageMappedExtension F (n : ℕ) hpOdd U closureEquiv
Lean source · full declaration
def cyclotomicArithmeticStageRestrictionContinuous :
    Gal((MappedStage).field/Cyclo) →ₜ* Gal(OriginalStage/F) where
  toMonoidHom := cyclotomicArithmeticStageMappedRestriction F (n : ℕ) hpOdd U closureEquiv
  continuous_toFun := continuous_of_discreteTopology
theorem

cyclotomicArithmeticStageAbsoluteRestriction_factor

L63 ↗
ClassFieldTower.Martinet.Shafarevich.cyclotomicArithmeticStageAbsoluteRestriction_factor
Documentation

The finite restriction square commutes with the actual absolute Galois inclusion, using the same closure equivalence on both sides.

Source context 13 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet ClassFieldTower.ProP ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local notation "Cyclo" => IdealRadicalCyclotomicBase F (n : ℕ) (Fact.out : Nat.Prime (n : ℕ))
local notation "OriginalStage" => FiniteEverywhereUnramifiedProPExtension.field
  (openNormalArithmeticStage F (n : ℕ) hpOdd U)
local instance cyclotomicVanishingBaseFinite : FiniteDimensional F Cyclo :=
  finiteDimensional_idealRadicalCyclotomicBase F (n : ℕ) Fact.out
local instance cyclotomicVanishingBaseNumber : NumberField Cyclo :=
  NumberField.of_module_finite F Cyclo
local notation "closureEquiv" => finiteIntermediateAbsoluteClosureEquiv F Cyclo
local notation "MappedStage" =>
  cyclotomicArithmeticStageMappedExtension F (n : ℕ) hpOdd U closureEquiv
Lean source · statement
theorem cyclotomicArithmeticStageAbsoluteRestriction_factor :
    (cyclotomicArithmeticStageRestrictionContinuous F n hpOdd U).comp
      (finiteUnramifiedExtensionAbsoluteRestriction Cyclo n MappedStage) =
    (openNormalArithmeticStageAbsoluteRestriction F n hpOdd U).comp
      (cyclotomicAbsoluteGaloisInclusion F (n : ℕ))
theorem

openNormalArithmeticStage_absoluteH2Map_eq_zero_of_odd

L102 ↗
ClassFieldTower.Martinet.Shafarevich.openNormalArithmeticStage_absoluteH2Map_eq_zero_of_odd
Documentation

Every finite unramified arithmetic-stage H² class vanishes on the absolute Galois group, without assuming that the base contains mu_p.

Source context 13 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet ClassFieldTower.ProP ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local notation "Cyclo" => IdealRadicalCyclotomicBase F (n : ℕ) (Fact.out : Nat.Prime (n : ℕ))
local notation "OriginalStage" => FiniteEverywhereUnramifiedProPExtension.field
  (openNormalArithmeticStage F (n : ℕ) hpOdd U)
local instance cyclotomicVanishingBaseFinite : FiniteDimensional F Cyclo :=
  finiteDimensional_idealRadicalCyclotomicBase F (n : ℕ) Fact.out
local instance cyclotomicVanishingBaseNumber : NumberField Cyclo :=
  NumberField.of_module_finite F Cyclo
local notation "closureEquiv" => finiteIntermediateAbsoluteClosureEquiv F Cyclo
local notation "MappedStage" =>
  cyclotomicArithmeticStageMappedExtension F (n : ℕ) hpOdd U closureEquiv
Lean source · statement
theorem openNormalArithmeticStage_absoluteH2Map_eq_zero_of_odd
    (x : continuousCohomologyZModPLifted (n : ℕ) Gal(OriginalStage/F) 2) :
    (continuousCohomologyZModPMapLifted (n : ℕ)
      (openNormalArithmeticStageAbsoluteRestriction F n hpOdd U) 2).hom x = 0
theorem

openNormalQuotient_absoluteH2Inflation_eq_zero_of_odd

L122 ↗
ClassFieldTower.Martinet.Shafarevich.openNormalQuotient_absoluteH2Inflation_eq_zero_of_odd
Documentation

Absolute inflation kills a finite open-normal quotient H² class for every number field and odd p.

Source context 14 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet ClassFieldTower.ProP ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local notation "Cyclo" => IdealRadicalCyclotomicBase F (n : ℕ) (Fact.out : Nat.Prime (n : ℕ))
local notation "OriginalStage" => FiniteEverywhereUnramifiedProPExtension.field
  (openNormalArithmeticStage F (n : ℕ) hpOdd U)
local instance cyclotomicVanishingBaseFinite : FiniteDimensional F Cyclo :=
  finiteDimensional_idealRadicalCyclotomicBase F (n : ℕ) Fact.out
local instance cyclotomicVanishingBaseNumber : NumberField Cyclo :=
  NumberField.of_module_finite F Cyclo
local notation "closureEquiv" => finiteIntermediateAbsoluteClosureEquiv F Cyclo
local notation "MappedStage" =>
  cyclotomicArithmeticStageMappedExtension F (n : ℕ) hpOdd U closureEquiv
include hpOdd
Lean source · statement
theorem openNormalQuotient_absoluteH2Inflation_eq_zero_of_odd
    (x : continuousCohomologyZModPLifted (n : ℕ)
      (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
        (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))) 2) :
    (continuousCohomologyZModPMapLifted (n : ℕ)
      (absoluteToMaxEverywhereUnramifiedProP F (n : ℕ)) 2).hom
        ((continuousCohomologyZModPMapLifted (n : ℕ)
          (OpenNormalSubgroup.quotientProj U) 2).hom x) = 0
theorem

absoluteUnramifiedH2Inflation_eq_zero

L152 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteUnramifiedH2Inflation_eq_zero
Documentation

Every unramified pro-p degree-two class has zero absolute inflation over every number field, for odd p.

Source context 15 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet ClassFieldTower.ProP ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local notation "Cyclo" => IdealRadicalCyclotomicBase F (n : ℕ) (Fact.out : Nat.Prime (n : ℕ))
local notation "OriginalStage" => FiniteEverywhereUnramifiedProPExtension.field
  (openNormalArithmeticStage F (n : ℕ) hpOdd U)
local instance cyclotomicVanishingBaseFinite : FiniteDimensional F Cyclo :=
  finiteDimensional_idealRadicalCyclotomicBase F (n : ℕ) Fact.out
local instance cyclotomicVanishingBaseNumber : NumberField Cyclo :=
  NumberField.of_module_finite F Cyclo
local notation "closureEquiv" => finiteIntermediateAbsoluteClosureEquiv F Cyclo
local notation "MappedStage" =>
  cyclotomicArithmeticStageMappedExtension F (n : ℕ) hpOdd U closureEquiv
include hpOdd
omit U in
Lean source · statement
theorem absoluteUnramifiedH2Inflation_eq_zero
    (x : continuousCohomologyZModPLifted (n : ℕ)
      (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)) 2) :
    (continuousCohomologyZModPMapLifted (n : ℕ)
      (absoluteToMaxEverywhereUnramifiedProP F (n : ℕ)) 2).hom x = 0

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