Module

ShafarevichRelationRankBound.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.ShafarevichRelationRankBound

3 declarations indexed from sourceView source ↗

Module documentation

Shafarevich's relation-rank bound

For every number field and every odd prime, the maximal everywhere-unramified pro-p Galois group has finite-dimensional H². Its relation rank is at most the generator rank plus the unit rank and the roots-of-unity correction. All arithmetic input is supplied by the constructed finite-stage radical maps and their proved kernel bounds.

Imports3

Imported by1

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.All

theorem

maxEverywhereUnramified_h2_finite_and_finrank_le_radicalDual

L37 ↗

ClassFieldTower.Martinet.Shafarevich.maxEverywhereUnramified_h2_finite_and_finrank_le_radicalDual

Documentation

The actual maximal unramified H² is finite and bounded by the arithmetic radical dual.

Source context 8 commands

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

open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.ProP ClassFieldTower.Martinet
open ProCGroups.Generation ProCGroups.FiniteGeneration
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime] (hpOdd : Odd p)
include hpOdd

Lean source · statement

theorem maxEverywhereUnramified_h2_finite_and_finrank_le_radicalDual :
    FiniteDimensional (ZMod p)
      (continuousCohomologyZModPLifted p (MaxEverywhereUnramifiedProPGaloisGroup F p) 2) ∧
    Module.finrank (ZMod p)
      (continuousCohomologyZModPLifted p (MaxEverywhereUnramifiedProPGaloisGroup F p) 2) ≤
        Module.finrank (ZMod p) (Module.Dual (ZMod p) (idealPowerRadicalModP F p))

theorem

shafarevich_relation_rank_bound_lifted

L57 ↗

ClassFieldTower.Martinet.Shafarevich.shafarevich_relation_rank_bound_lifted

Documentation

Shafarevich's bound in the universe-lifted continuous-cohomology model.

Source context 8 commands

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

open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.ProP ClassFieldTower.Martinet
open ProCGroups.Generation ProCGroups.FiniteGeneration
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime] (hpOdd : Odd p)
include hpOdd

Lean source · full declaration

theorem shafarevich_relation_rank_bound_lifted :
    FiniteDimensional (ZMod p)
      (continuousCohomologyZModPLifted p (MaxEverywhereUnramifiedProPGaloisGroup F p) 2) ∧
    (open Classical in
      Module.finrank (ZMod p)
        (continuousCohomologyZModPLifted p (MaxEverywhereUnramifiedProPGaloisGroup F p) 2) ≤
      topologicalGeneratorRank (MaxEverywhereUnramifiedProPGaloisGroup F p) +
        (NumberField.InfinitePlace.nrRealPlaces F +
          NumberField.InfinitePlace.nrComplexPlaces F - 1) +
          (if ∃ ζ : F, IsPrimitiveRoot ζ p then 1 else 0)) := by
  obtain ⟨hfinite, hle⟩ := maxEverywhereUnramified_h2_finite_and_finrank_le_radicalDual F p hpOdd
  exact maxEverywhereUnramified_h2_numerical_bound_of_finrank_le_radicalDual F p hpOdd hfinite hle

theorem