NYLL
Module

RealProTwoH2Bound.lean

Nyll.SawinTotallyRealTowers.RealProTwoH2Bound
3 declarations indexed from sourceView source ↗

Module documentation

Six-dimensional degree two for the initial real pro-two group

At every actual finite arithmetic stage the field-unit Kummer image has at most 64 elements. Its kernel is killed by inflation to the constructed maximal group. Discrete comparison and the finite-stage Galois equivalence therefore give a surjection from that Kummer image onto the stage inflation image. Uniform finite-stage cardinality bounds imply finite continuous H² and dimension at most six, with no cohomological finiteness assumption.

Imports22
Imported by2

Declarations

theorem

natCard_le_range_of_ker_le

L51 ↗
ClassFieldTower.Sawin.natCard_le_range_of_ker_le
Source context 6 commands

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

open scoped NumberField Topology
open NumberField IsDedekindDomain CategoryTheory
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Cohomology ClassFieldTower.ProP
open ClassFieldTower.Martinet.Shafarevich ProCGroups ProCGroups.ProC
Lean source · statement
theorem natCard_le_range_of_ker_le
    {A B C : Type} [AddCommGroup A] [AddCommGroup B] [AddCommGroup C]
    (f : A →+ B) (g : A →+ C) (hker : f.ker ≤ g.ker)
    (hg : Function.Surjective g) [Finite f.range] : Nat.card C ≤ Nat.card f.range
theorem

initialStage_inflationRange_natCard_le

L62 ↗
ClassFieldTower.Sawin.initialStage_inflationRange_natCard_le
Source context 6 commands

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

open scoped NumberField Topology
open NumberField IsDedekindDomain CategoryTheory
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Cohomology ClassFieldTower.ProP
open ClassFieldTower.Martinet.Shafarevich ProCGroups ProCGroups.ProC
Lean source · statement
theorem initialStage_inflationRange_natCard_le
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup 2)
      (maximalRealProPOutside 2 sawinRationalPrimeSupport ≃ₐ[ℚ]
        maximalRealProPOutside 2 sawinRationalPrimeSupport)) :
    Nat.card (degreeTwoInflationRange (p := 2) U) ≤ 2 ^ 6
theorem

sawinInitialProTwoH2_finiteDimensional_finrank_le

L138 ↗
ClassFieldTower.Sawin.sawinInitialProTwoH2_finiteDimensional_finrank_le
Documentation

The initial maximal real pro-two group has finite continuous H², and its dimension over F₂ is at most six.

Source context 6 commands

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

open scoped NumberField Topology
open NumberField IsDedekindDomain CategoryTheory
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Cohomology ClassFieldTower.ProP
open ClassFieldTower.Martinet.Shafarevich ProCGroups ProCGroups.ProC
Lean source · statement
theorem sawinInitialProTwoH2_finiteDimensional_finrank_le :
    FiniteDimensional (ZMod 2)
      (continuousCohomologyZModPLifted 2
        (maximalRealProPOutside 2 sawinRationalPrimeSupport ≃ₐ[ℚ]
          maximalRealProPOutside 2 sawinRationalPrimeSupport) 2) ∧
    Module.finrank (ZMod 2)
      (continuousCohomologyZModPLifted 2
        (maximalRealProPOutside 2 sawinRationalPrimeSupport ≃ₐ[ℚ]
          maximalRealProPOutside 2 sawinRationalPrimeSupport) 2) ≤ 6

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