Module

UnramifiedExplicitBridge.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Global.UnramifiedExplicitBridge

6 declarations indexed from sourceView source ↗

Module documentation

Explicit everywhere-unramified benchmark bridge

This file packages the library predicates for finite and infinite unramifiedness in the exact explicit form used by the Shafarevich benchmark. It also connects finite-place unramifiedness to formal unramifiedness and to finite étale algebras of rings of integers.

Imports7

Nyll.ClassFieldTheory.AlgebraicNumberTheory.NumberField.FiniteUnramifiedEtaleBridge
Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Global.EverywhereUnramifiedBridge
Mathlib.RingTheory.Etale.Finite
Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
Mathlib.RingTheory.Flat.TorsionFree
Mathlib.RingTheory.Smooth.Fiber
Mathlib.RingTheory.Unramified.Locus

Imported by1

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Global.All

theorem

finitePlaceUnramifiedness_iff_explicitRamificationIdx

L34 ↗

ClassFieldTower.Martinet.finitePlaceUnramifiedness_iff_explicitRamificationIdx

Documentation

Finite-place unramifiedness in the exact ramification-index form used by the benchmark contract.

Source context 4 commands

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

open scoped NumberField
noncomputable section
universe u v
namespace ClassFieldTower.Martinet

Lean source · statement

theorem finitePlaceUnramifiedness_iff_explicitRamificationIdx
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] :
    IsUnramifiedAtFinitePlaces K L ↔
      ∀ (p : Ideal (𝓞 K)) (P : Ideal (𝓞 L)),
        p.IsPrime → p ≠ ⊥ → P ∈ p.primesOver (𝓞 L) →
          P.ramificationIdx (𝓞 K) = 1

theorem

finitePlaceUnramifiedness_iff_formallyUnramified

L47 ↗

ClassFieldTower.Martinet.finitePlaceUnramifiedness_iff_formallyUnramified

Documentation

Unramifiedness at every finite place is equivalent to formal unramifiedness of the corresponding extension of rings of integers.

Source context 4 commands

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

open scoped NumberField
noncomputable section
universe u v
namespace ClassFieldTower.Martinet

Lean source · statement

theorem finitePlaceUnramifiedness_iff_formallyUnramified
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] :
    IsUnramifiedAtFinitePlaces K L ↔
      Algebra.FormallyUnramified (𝓞 K) (𝓞 L)

theorem

finitePlaceUnramifiedness_to_etale

L72 ↗

ClassFieldTower.Martinet.finitePlaceUnramifiedness_to_etale

Documentation

Finite-place unramifiedness makes the extension of rings of integers étale.

Source context 4 commands

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

open scoped NumberField
noncomputable section
universe u v
namespace ClassFieldTower.Martinet

Lean source · statement

theorem finitePlaceUnramifiedness_to_etale
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L]
    (h : IsUnramifiedAtFinitePlaces K L) :
    Algebra.Etale (𝓞 K) (𝓞 L)

def

finitePlaceUnramifiedness_toFiniteEtale

L95 ↗

ClassFieldTower.Martinet.finitePlaceUnramifiedness_toFiniteEtale

Documentation

The finite étale algebra of rings of integers attached to a finite-place-unramified number-field extension.

Source context 4 commands

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

open scoped NumberField
noncomputable section
universe u v
namespace ClassFieldTower.Martinet

Lean source · statement

def finitePlaceUnramifiedness_toFiniteEtale
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L]
    (h : IsUnramifiedAtFinitePlaces K L) :
    CommAlgCat.FiniteEtale (𝓞 K)

theorem

infinitePlaceUnramifiedness_iff_explicitRealLifts

L110 ↗

ClassFieldTower.Martinet.infinitePlaceUnramifiedness_iff_explicitRealLifts

Documentation

Infinite-place unramifiedness in the exact real-place lifting form used by the benchmark contract.

Source context 4 commands

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

open scoped NumberField
noncomputable section
universe u v
namespace ClassFieldTower.Martinet

Lean source · statement

theorem infinitePlaceUnramifiedness_iff_explicitRealLifts
    {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L] :
    IsUnramifiedAtInfinitePlaces K L ↔
      ∀ w : NumberField.InfinitePlace K, w.IsReal →
        ∀ w' : NumberField.InfinitePlace L,
          w'.comap (algebraMap K L) = w → w'.IsReal

theorem

everywhereUnramified_iff_explicitClauses

L121 ↗

ClassFieldTower.Martinet.everywhereUnramified_iff_explicitClauses

Documentation

The existing everywhere-unramified predicate is exactly the conjunction of the finite and infinite clauses in the benchmark contract.

Source context 4 commands

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

open scoped NumberField
noncomputable section
universe u v
namespace ClassFieldTower.Martinet

Lean source · statement

theorem everywhereUnramified_iff_explicitClauses
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] :
    IsEverywhereUnramified K L ↔
      (∀ (p : Ideal (𝓞 K)) (P : Ideal (𝓞 L)),
          p.IsPrime → p ≠ ⊥ → P ∈ p.primesOver (𝓞 L) →
            P.ramificationIdx (𝓞 K) = 1) ∧
        (∀ w : NumberField.InfinitePlace K, w.IsReal →
          ∀ w' : NumberField.InfinitePlace L,
            w'.comap (algebraMap K L) = w → w'.IsReal)

Module documentation

Explicit everywhere-unramified benchmark bridge

Declarations

finitePlaceUnramifiedness_iff_explicitRamificationIdx

finitePlaceUnramifiedness_iff_formallyUnramified

finitePlaceUnramifiedness_to_etale

finitePlaceUnramifiedness_toFiniteEtale

infinitePlaceUnramifiedness_iff_explicitRealLifts

everywhereUnramified_iff_explicitClauses