NYLL
Module

LeanEvalAdapter.lean

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

Module documentation

Adapter infrastructure for the LeanEval Shafarevich statement

This file isolates the three representation differences between the production theorem and the trusted benchmark statement: the explicit everywhere-unramified predicate, finite-set generator rank, and small versus universe-lifted trivial cohomology coefficients.

Imports3
Imported by2

Declarations

def

ExplicitIsEverywhereUnramified

L38 ↗
ClassFieldTower.Martinet.Shafarevich.ExplicitIsEverywhereUnramified
Documentation

The finite-prime and real-place formula used as the trusted benchmark's everywhere-unramified predicate.

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
open ClassFieldTower.ProP
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
universe u v
Lean source · statement
def ExplicitIsEverywhereUnramified
    (F : Type u) (M : Type v)
    [Field F] [Field M] [NumberField F] [NumberField M]
    [Algebra F M] : Prop
theorem

isEverywhereUnramified_iff_explicitPredicate

L51 ↗
ClassFieldTower.Martinet.Shafarevich.isEverywhereUnramified_iff_explicitPredicate
Documentation

The library predicate and the benchmark's explicit predicate agree.

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
open ClassFieldTower.ProP
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
universe u v
Lean source · statement
theorem isEverywhereUnramified_iff_explicitPredicate
    (F : Type u) (M : Type v)
    [Field F] [Field M] [NumberField F] [NumberField M]
    [Algebra F M] :
    IsEverywhereUnramified F M ↔ ExplicitIsEverywhereUnramified F M
def

explicitMaximalEverywhereUnramifiedProP

L59 ↗
ClassFieldTower.Martinet.Shafarevich.explicitMaximalEverywhereUnramifiedProP
Documentation

The maximal compositum written with the explicit benchmark predicate.

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
open ClassFieldTower.ProP
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
universe u v
Lean source · statement
def explicitMaximalEverywhereUnramifiedProP
    (F : Type u) [Field F] [NumberField F]
    (p : ℕ) [Fact p.Prime] :
    IntermediateField F (AlgebraicClosure F)
theorem

maximalEverywhereUnramifiedProP_eq_explicit

L73 ↗
ClassFieldTower.Martinet.Shafarevich.maximalEverywhereUnramifiedProP_eq_explicit
Documentation

Replacing the structured unramified predicate by its explicit clauses does not change the maximal compositum.

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
open ClassFieldTower.ProP
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
universe u v
Lean source · statement
theorem maximalEverywhereUnramifiedProP_eq_explicit
    (F : Type u) [Field F] [NumberField F]
    (p : ℕ) [Fact p.Prime] :
    maximalEverywhereUnramifiedProP F p =
      explicitMaximalEverywhereUnramifiedProP F p
theorem

maxEverywhereUnramifiedProPGaloisGroup_topologicallyFinitelyGenerated

L84 ↗
ClassFieldTower.Martinet.Shafarevich.maxEverywhereUnramifiedProPGaloisGroup_topologicallyFinitelyGenerated
Documentation

The maximal everywhere-unramified pro-p Galois group is topologically finitely generated for odd p.

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
open ClassFieldTower.ProP
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
universe u v
Lean source · statement
theorem maxEverywhereUnramifiedProPGaloisGroup_topologicallyFinitelyGenerated
    (F : Type) [Field F] [NumberField F]
    (p : ℕ) [Fact p.Prime] (hpOdd : Odd p) :
    TopologicallyFinitelyGenerated
      (MaxEverywhereUnramifiedProPGaloisGroup F p)
theorem

smallH2_and_finiteGeneratorRank_bound_of_lifted

L121 ↗
ClassFieldTower.Martinet.Shafarevich.smallH2_and_finiteGeneratorRank_bound_of_lifted
Documentation

A production bound for lifted cohomology converts directly to the small-coefficient and finite-generator-rank presentation used by LeanEval.

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
open ClassFieldTower.ProP
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
universe u v
Lean source · statement
theorem smallH2_and_finiteGeneratorRank_bound_of_lifted
    (p : ℕ) [Fact p.Prime]
    (G : Type) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (hG : TopologicallyFinitelyGenerated G)
    (a b : ℕ)
    (h : FiniteDimensional (ZMod p)
          (continuousCohomologyZModPLifted p G 2) ∧
        Module.finrank (ZMod p)
            (continuousCohomologyZModPLifted p G 2) ≤
          topologicalGeneratorRank G + a + b) :
    FiniteDimensional (ZMod p) (continuousCohomologyZModP p G 2) ∧
      Module.finrank (ZMod p) (continuousCohomologyZModP p G 2) ≤
        finiteTopologicalGeneratorRank G + a + b
theorem

maxEverywhereUnramified_smallH2_and_finiteGeneratorRank_bound_of_lifted

L142 ↗
ClassFieldTower.Martinet.Shafarevich.maxEverywhereUnramified_smallH2_and_finiteGeneratorRank_bound_of_lifted
Documentation

Maximal-group specialization of the LeanEval rank/coefficient adapter.

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
open ClassFieldTower.ProP
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
universe u v
Lean source · statement
theorem maxEverywhereUnramified_smallH2_and_finiteGeneratorRank_bound_of_lifted
    (F : Type) [Field F] [NumberField F]
    (p : ℕ) [Fact p.Prime] (hpOdd : Odd p)
    (a b : ℕ)
    (h : FiniteDimensional (ZMod p)
          (continuousCohomologyZModPLifted p
            (MaxEverywhereUnramifiedProPGaloisGroup F p) 2) ∧
        Module.finrank (ZMod p)
            (continuousCohomologyZModPLifted p
              (MaxEverywhereUnramifiedProPGaloisGroup F p) 2) ≤
          topologicalGeneratorRank
              (MaxEverywhereUnramifiedProPGaloisGroup F p) + a + b) :
    FiniteDimensional (ZMod p)
        (continuousCohomologyZModP p
          (MaxEverywhereUnramifiedProPGaloisGroup F p) 2) ∧
      Module.finrank (ZMod p)
          (continuousCohomologyZModP p
            (MaxEverywhereUnramifiedProPGaloisGroup F p) 2) ≤
        finiteTopologicalGeneratorRank
            (MaxEverywhereUnramifiedProPGaloisGroup F p) + a + b

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