Module

MathlibUnramifiedInterface.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.NumberField.MathlibUnramifiedInterface

7 declarations indexed from sourceView source ↗

Module documentation

Finite-place unramifiedness comparison

The implementation quantifies over primes of the extension, while the public definition quantifies over primes of the base. These are equivalent because every prime above a nonzero base prime is itself nonzero.

Imports4

Imported by2

def

ringOfIntegersEquivOfAlgEquiv

L29 ↗

ClassFieldTheory.ringOfIntegersEquivOfAlgEquiv

Documentation

A number-field equivalence over K restricts to an equivalence of integer rings over the integer ring of K.

Source context 3 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
namespace ClassFieldTheory

Lean source · statement

def ringOfIntegersEquivOfAlgEquiv
    (K L E : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [Field E] [NumberField E] [Algebra K E]
    (e : L ≃ₐ[K] E) : 𝓞 L ≃ₐ[𝓞 K] 𝓞 E

theorem

isUnramifiedAtFinitePlaces_iff_formallyUnramified

L47 ↗

ClassFieldTheory.isUnramifiedAtFinitePlaces_iff_formallyUnramified

Documentation

Unramifiedness at all nonzero primes is equivalent to formal unramifiedness of the entire integer-ring extension; the zero prime is automatically unramified in characteristic zero.

Source context 3 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
namespace ClassFieldTheory

Lean source · statement

theorem isUnramifiedAtFinitePlaces_iff_formallyUnramified
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L] :
    _root_.IsUnramifiedAtFinitePlaces K L ↔
      Algebra.FormallyUnramified (𝓞 K) (𝓞 L)

theorem

isUnramifiedAtFinitePlaces_iff_original

L65 ↗

ClassFieldTheory.isUnramifiedAtFinitePlaces_iff_original

Documentation

The base-prime and extension-prime formulations of finite-place unramifiedness agree.

Source context 3 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
namespace ClassFieldTheory

Lean source · statement

theorem isUnramifiedAtFinitePlaces_iff_original
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L] :
    ClassFieldTheory.IsUnramifiedAtFinitePlaces K L ↔
      _root_.IsUnramifiedAtFinitePlaces K L

theorem

isUnramifiedAtFinitePlaces_iff_of_algEquiv

L84 ↗

ClassFieldTheory.isUnramifiedAtFinitePlaces_iff_of_algEquiv

Documentation

Finite-place unramifiedness is invariant under a number-field equivalence over the base.

Source context 3 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
namespace ClassFieldTheory

Lean source · statement

theorem isUnramifiedAtFinitePlaces_iff_of_algEquiv
    (K L E : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [Field E] [NumberField E] [Algebra K E]
    (e : L ≃ₐ[K] E) :
    ClassFieldTheory.IsUnramifiedAtFinitePlaces K L ↔
      ClassFieldTheory.IsUnramifiedAtFinitePlaces K E

theorem

isUnramifiedAtInfinitePlaces_iff_of_algEquiv

L101 ↗

ClassFieldTheory.isUnramifiedAtInfinitePlaces_iff_of_algEquiv

Documentation

Unramifiedness at infinite places is also invariant under a number-field equivalence over the base.

Source context 3 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
namespace ClassFieldTheory

Lean source · statement

theorem isUnramifiedAtInfinitePlaces_iff_of_algEquiv
    (K L E : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [Field E] [NumberField E] [Algebra K E]
    (e : L ≃ₐ[K] E) :
    IsUnramifiedAtInfinitePlaces K L ↔
      IsUnramifiedAtInfinitePlaces K E

theorem

isEverywhereUnramified_iff_original

L133 ↗

ClassFieldTheory.isEverywhereUnramified_iff_original

Documentation

The public conjunction and the implementation's bundled predicate for unramifiedness at all places agree.

Source context 3 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
namespace ClassFieldTheory

Lean source · statement

theorem isEverywhereUnramified_iff_original
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L] :
    ClassFieldTheory.IsEverywhereUnramified K L ↔
      _root_.IsEverywhereUnramified K L

theorem

isEverywhereUnramified_iff_of_algEquiv

L148 ↗

ClassFieldTheory.isEverywhereUnramified_iff_of_algEquiv

Documentation

Everywhere-unramifiedness is invariant under a number-field equivalence over the base.

Source context 3 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
namespace ClassFieldTheory

Lean source · statement

theorem isEverywhereUnramified_iff_of_algEquiv
    (K L E : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [Field E] [NumberField E] [Algebra K E]
    (e : L ≃ₐ[K] E) :
    ClassFieldTheory.IsEverywhereUnramified K L ↔
      ClassFieldTheory.IsEverywhereUnramified K E

Module documentation

Finite-place unramifiedness comparison

Declarations

ringOfIntegersEquivOfAlgEquiv

isUnramifiedAtFinitePlaces_iff_formallyUnramified

isUnramifiedAtFinitePlaces_iff_original

isUnramifiedAtFinitePlaces_iff_of_algEquiv

isUnramifiedAtInfinitePlaces_iff_of_algEquiv

isEverywhereUnramified_iff_original

isEverywhereUnramified_iff_of_algEquiv