Module

AbsoluteUnramifiedH2Vanishing.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.AbsoluteUnramifiedH2Vanishing

3 declarations indexed from sourceView source ↗

Module documentation

Vanishing of absolute inflation from unramified pro-p degree two

The quotient/arithmetic-stage equivalence is checked on actual field automorphisms against restriction from the absolute Galois group. Thus the proved arithmetic-stage vanishing applies to every finite quotient. Finite-stage realization of continuous cohomology then gives vanishing for every degree-two class of the maximal everywhere-unramified pro-p group over a base containing the supplied primitive root. No comparison assumption or new instance is introduced.

Imports4

Imported by2

theorem

openNormalArithmeticStageAbsoluteRestriction_factor

L41 ↗

ClassFieldTower.Martinet.Shafarevich.openNormalArithmeticStageAbsoluteRestriction_factor

Documentation

Quotient restriction followed by the arithmetic-stage equivalence is exactly actual absolute restriction to that field.

Source context 9 commands

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

open scoped Topology NumberField
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 : ℕ)))
include hpOdd

Lean source · statement

theorem openNormalArithmeticStageAbsoluteRestriction_factor :
    (ContinuousMonoidHom.toContinuousMonoidHom
      (openNormalQuotientContinuousEquivArithmeticStageGalois F (n : ℕ) hpOdd U)).comp
        ((OpenNormalSubgroup.quotientProj U).comp
          (absoluteToMaxEverywhereUnramifiedProP F (n : ℕ))) =
      openNormalArithmeticStageAbsoluteRestriction F n hpOdd U

theorem

openNormalQuotient_absoluteH2Inflation_eq_zero

L82 ↗

ClassFieldTower.Martinet.Shafarevich.openNormalQuotient_absoluteH2Inflation_eq_zero

Documentation

Every finite unramified quotient class becomes zero on the absolute Galois group.

Source context 9 commands

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

open scoped Topology NumberField
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 : ℕ)))
include hpOdd

Lean source · statement

theorem openNormalQuotient_absoluteH2Inflation_eq_zero
    (hmu : (primitiveRoots (n : ℕ) F).Nonempty)
    (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_of_primitiveRoots

L113 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteUnramifiedH2Inflation_eq_zero_of_primitiveRoots

Documentation

Absolute inflation kills every continuous unramified pro-p degree-two class when the base contains a primitive p-th root of unity.

Source context 10 commands

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

open scoped Topology NumberField
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 : ℕ)))
include hpOdd
omit U in

Lean source · statement

theorem absoluteUnramifiedH2Inflation_eq_zero_of_primitiveRoots
    (hmu : (primitiveRoots (n : ℕ) F).Nonempty)
    (x : continuousCohomologyZModPLifted (n : ℕ)
      (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)) 2) :
    (continuousCohomologyZModPMapLifted (n : ℕ)
      (absoluteToMaxEverywhereUnramifiedProP F (n : ℕ)) 2).hom x = 0

Module documentation

Vanishing of absolute inflation from unramified pro-p degree two

Declarations

openNormalArithmeticStageAbsoluteRestriction_factor

openNormalQuotient_absoluteH2Inflation_eq_zero

absoluteUnramifiedH2Inflation_eq_zero_of_primitiveRoots