Module

EverywhereUnramifiedBridge.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Global.EverywhereUnramifiedBridge

12 declarations indexed from sourceView source ↗

Module documentation

Everywhere-unramified bridges for number fields

This file combines the finite-prime bridges for rings of integers with the infinite-place API. It also transports everywhere-unramifiedness across an equivalence of top fields and supplies odd-degree Galois constructors.

Imports2

Imported by6

theorem

everywhereUnramified_of_finitePlaces_of_infinitePlaces

L28 ↗

ClassFieldTower.Martinet.everywhereUnramified_of_finitePlaces_of_infinitePlaces

Documentation

Finite-prime and infinite-place unramifiedness together give everywhere-unramifiedness.

Source context 4 commands

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

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

Lean source · full declaration

theorem everywhereUnramified_of_finitePlaces_of_infinitePlaces
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L]
    (hFinite : IsUnramifiedAtFinitePlaces K L)
    (hInfinite : IsUnramifiedAtInfinitePlaces K L) :
    IsEverywhereUnramified K L where
  finitePlaces := hFinite
  infinitePlaces := hInfinite

theorem

isUnramifiedAtFinitePlaces_iff_ramificationIdx_eq_one

L41 ↗

ClassFieldTower.Martinet.isUnramifiedAtFinitePlaces_iff_ramificationIdx_eq_one

Documentation

The finite-place predicate is equivalent to the ramification-index-one formula used by the benchmark.

Source context 4 commands

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

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

Lean source · statement

theorem isUnramifiedAtFinitePlaces_iff_ramificationIdx_eq_one
    {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

isUnramifiedAtInfinitePlaces_iff_real_lifts

L73 ↗

ClassFieldTower.Martinet.isUnramifiedAtInfinitePlaces_iff_real_lifts

Documentation

Infinite-place unramifiedness is exactly the assertion that every lift of a real place is real.

Source context 4 commands

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

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

Lean source · statement

theorem isUnramifiedAtInfinitePlaces_iff_real_lifts
    {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

infinitePlaceUnramifiedness_map_algEquiv

L98 ↗

ClassFieldTower.Martinet.infinitePlaceUnramifiedness_map_algEquiv

Documentation

Infinite-place unramifiedness is preserved by an algebra equivalence of the top field.

Source context 4 commands

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

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

Lean source · statement

theorem infinitePlaceUnramifiedness_map_algEquiv
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [Field L] [Field M]
    [Algebra K L] [Algebra K M]
    (e : L ≃ₐ[K] M)
    (h : IsUnramifiedAtInfinitePlaces K L) :
    IsUnramifiedAtInfinitePlaces K M

theorem

everywhereUnramified_congrTop

L123 ↗

ClassFieldTower.Martinet.everywhereUnramified_congrTop

Documentation

Everywhere-unramifiedness is preserved when the top number field is replaced by an equivalent algebra over the base field.

Source context 4 commands

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

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

Lean source · statement

theorem everywhereUnramified_congrTop
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Field M] [NumberField M]
    [Algebra K L] [Algebra K M]
    (e : L ≃ₐ[K] M)
    (h : IsEverywhereUnramified K L) :
    IsEverywhereUnramified K M

theorem

isEverywhereUnramified_congrTop

L138 ↗

ClassFieldTower.Martinet.isEverywhereUnramified_congrTop

Documentation

Everywhere-unramifiedness is invariant under an algebra equivalence of the top number field.

Source context 4 commands

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

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

Lean source · statement

theorem isEverywhereUnramified_congrTop
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Field M] [NumberField M]
    [Algebra K L] [Algebra K M]
    (e : L ≃ₐ[K] M) :
    IsEverywhereUnramified K L ↔ IsEverywhereUnramified K M

theorem

everywhereUnramified_of_formallyUnramified

L151 ↗

ClassFieldTower.Martinet.everywhereUnramified_of_formallyUnramified

Documentation

Formal unramifiedness of the rings of integers, together with the infinite-place condition, gives everywhere-unramifiedness.

Source context 4 commands

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

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

Lean source · statement

theorem everywhereUnramified_of_formallyUnramified
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L]
    [Algebra.FormallyUnramified (𝓞 K) (𝓞 L)]
    (hInfinite : IsUnramifiedAtInfinitePlaces K L) :
    IsEverywhereUnramified K L

theorem

everywhereUnramified_of_etale

L164 ↗

ClassFieldTower.Martinet.everywhereUnramified_of_etale

Documentation

Étaleness of the rings of integers, together with the infinite-place condition, gives everywhere-unramifiedness.

Source context 4 commands

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

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

Lean source · statement

theorem everywhereUnramified_of_etale
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L]
    [Algebra.Etale (𝓞 K) (𝓞 L)]
    (hInfinite : IsUnramifiedAtInfinitePlaces K L) :
    IsEverywhereUnramified K L

theorem

everywhereUnramified_of_finitePlaces_of_odd_finrank

L177 ↗

ClassFieldTower.Martinet.everywhereUnramified_of_finitePlaces_of_odd_finrank

Documentation

An odd-degree Galois extension that is unramified at finite places is everywhere unramified.

Source context 4 commands

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

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

Lean source · statement

theorem everywhereUnramified_of_finitePlaces_of_odd_finrank
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] [IsGalois K L]
    (hFinite : IsUnramifiedAtFinitePlaces K L)
    (hOdd : Odd (Module.finrank K L)) :
    IsEverywhereUnramified K L

theorem

everywhereUnramified_of_formallyUnramified_of_odd_finrank

L190 ↗

ClassFieldTower.Martinet.everywhereUnramified_of_formallyUnramified_of_odd_finrank

Documentation

A formally unramified ring-of-integers extension of odd Galois degree is everywhere unramified.

Source context 4 commands

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

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

Lean source · statement

theorem everywhereUnramified_of_formallyUnramified_of_odd_finrank
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] [IsGalois K L]
    [Algebra.FormallyUnramified (𝓞 K) (𝓞 L)]
    (hOdd : Odd (Module.finrank K L)) :
    IsEverywhereUnramified K L

theorem

everywhereUnramified_of_etale_of_odd_finrank

L203 ↗

ClassFieldTower.Martinet.everywhereUnramified_of_etale_of_odd_finrank

Documentation

An étale ring-of-integers extension of odd Galois degree is everywhere unramified.

Source context 4 commands

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

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

Lean source · statement

theorem everywhereUnramified_of_etale_of_odd_finrank
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] [IsGalois K L]
    [Algebra.Etale (𝓞 K) (𝓞 L)]
    (hOdd : Odd (Module.finrank K L)) :
    IsEverywhereUnramified K L

theorem

isEverywhereUnramified_iff_explicit

L216 ↗

ClassFieldTower.Martinet.isEverywhereUnramified_iff_explicit

Documentation

The library predicate is equivalent to the benchmark's explicit finite- and infinite-place clauses.

Source context 4 commands

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

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

Lean source · statement

theorem isEverywhereUnramified_iff_explicit
    {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

Everywhere-unramified bridges for number fields

Declarations