Module

FiniteUnramifiedEtaleBridge.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.NumberField.FiniteUnramifiedEtaleBridge

3 declarations indexed from sourceView source ↗

Module documentation

Finite-place unramifiedness bridges for number fields

This file transports finite-place unramifiedness across an equivalence of top fields and connects the number-theoretic predicate to the commutative-algebra notions of formal unramifiedness and étaleness for rings of integers.

Imports2

Nyll.ClassFieldTheory.AlgebraicNumberTheory.NumberField.FiniteUnramifiedTower
Mathlib.RingTheory.Etale.Basic

Imported by3

theorem

finitePlaceUnramifiedness_congrTop

L28 ↗

ClassFieldTower.Martinet.finitePlaceUnramifiedness_congrTop

Documentation

Finite-place 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 finitePlaceUnramifiedness_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 : IsUnramifiedAtFinitePlaces K L) :
    IsUnramifiedAtFinitePlaces K M

theorem

finitePlaceUnramifiedness_of_formallyUnramified

L61 ↗

ClassFieldTower.Martinet.finitePlaceUnramifiedness_of_formallyUnramified

Documentation

A formally unramified extension of rings of integers is unramified at every finite place 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 finitePlaceUnramifiedness_of_formallyUnramified
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L]
    [Algebra.FormallyUnramified (𝓞 K) (𝓞 L)] :
    IsUnramifiedAtFinitePlaces K L

theorem

finitePlaceUnramifiedness_of_etale

L74 ↗

ClassFieldTower.Martinet.finitePlaceUnramifiedness_of_etale

Documentation

An étale extension of rings of integers is unramified at every finite place. In particular, this applies to finite étale ring-of-integers extensions.

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 finitePlaceUnramifiedness_of_etale
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L]
    [Algebra.Etale (𝓞 K) (𝓞 L)] :
    IsUnramifiedAtFinitePlaces K L

Module documentation

Finite-place unramifiedness bridges for number fields

Declarations

finitePlaceUnramifiedness_congrTop

finitePlaceUnramifiedness_of_formallyUnramified

finitePlaceUnramifiedness_of_etale