Module

EverywhereUnramifiedTower.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.NumberField.EverywhereUnramifiedTower

5 declarations indexed from sourceView source ↗

Module documentation

Everywhere-unramified towers of number fields

This file combines finite-prime and infinite-place unramifiedness and records its tower and intermediate-field properties.

Imports2

Nyll.ClassFieldTheory.AlgebraicNumberTheory.NumberField.FiniteUnramifiedTower
Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Imported by5

structure

IsEverywhereUnramified

L25 ↗

Documentation

A number-field extension is everywhere unramified when it is unramified at every finite prime and at every infinite place.

Source context 2 commands

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

open scoped NumberField
universe u v w

Lean source · full declaration

structure IsEverywhereUnramified
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L] : Prop where
  /-- The extension is unramified at every finite prime. -/
  finitePlaces : IsUnramifiedAtFinitePlaces K L
  /-- The extension is unramified at every infinite place. -/
  infinitePlaces : IsUnramifiedAtInfinitePlaces K L

theorem

refl

L37 ↗

IsEverywhereUnramified.refl

Documentation

The identity extension is everywhere unramified.

Source context 3 commands

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

open scoped NumberField
universe u v w
namespace IsEverywhereUnramified

Lean source · full declaration

theorem refl
    (K : Type u) [Field K] [NumberField K] :
    IsEverywhereUnramified K K where
  finitePlaces :=
    IsUnramifiedAtFinitePlaces.refl K
  infinitePlaces :=
    inferInstance

theorem

trans

L54 ↗

IsEverywhereUnramified.trans

Documentation

Everywhere-unramified extensions are transitive in towers.

Source context 4 commands

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

open scoped NumberField
universe u v w
namespace IsEverywhereUnramified
variable
    {k : Type u} {K : Type v} {F : Type w}
    [Field k] [NumberField k]
    [Field K] [NumberField K]
    [Field F] [NumberField F]
    [Algebra k K] [Algebra k F] [Algebra K F]
    [IsScalarTower k K F]

Lean source · full declaration

theorem trans
    (hkK : IsEverywhereUnramified k K)
    (hKF : IsEverywhereUnramified K F) :
    IsEverywhereUnramified k F where
  finitePlaces :=
    IsUnramifiedAtFinitePlaces.trans
      hkK.finitePlaces hKF.finitePlaces
  infinitePlaces := by
    let : IsUnramifiedAtInfinitePlaces k K :=
      hkK.infinitePlaces
    let : IsUnramifiedAtInfinitePlaces K F :=
      hKF.infinitePlaces
    exact
      IsUnramifiedAtInfinitePlaces.trans k K F

theorem

top

L72 ↗

IsEverywhereUnramified.top

Documentation

If the top of a number-field tower is everywhere unramified over the bottom, then it is everywhere unramified over the intermediate field.

Source context 4 commands

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

open scoped NumberField
universe u v w
namespace IsEverywhereUnramified
variable
    {k : Type u} {K : Type v} {F : Type w}
    [Field k] [NumberField k]
    [Field K] [NumberField K]
    [Field F] [NumberField F]
    [Algebra k K] [Algebra k F] [Algebra K F]
    [IsScalarTower k K F]

Lean source · full declaration

theorem top
    (hkF : IsEverywhereUnramified k F) :
    IsEverywhereUnramified K F where
  finitePlaces :=
    IsUnramifiedAtFinitePlaces.top hkF.finitePlaces
  infinitePlaces := by
    let : IsUnramifiedAtInfinitePlaces k F :=
      hkF.infinitePlaces
    exact
      IsUnramifiedAtInfinitePlaces.top k K F

theorem

bot

L86 ↗

IsEverywhereUnramified.bot

Documentation

If the top of a number-field tower is everywhere unramified over the bottom, then the intermediate field is everywhere unramified over the bottom.

Source context 4 commands

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

open scoped NumberField
universe u v w
namespace IsEverywhereUnramified
variable
    {k : Type u} {K : Type v} {F : Type w}
    [Field k] [NumberField k]
    [Field K] [NumberField K]
    [Field F] [NumberField F]
    [Algebra k K] [Algebra k F] [Algebra K F]
    [IsScalarTower k K F]

Lean source · full declaration

theorem bot
    (hkF : IsEverywhereUnramified k F) :
    IsEverywhereUnramified k K where
  finitePlaces :=
    IsUnramifiedAtFinitePlaces.bot hkF.finitePlaces
  infinitePlaces := by
    let : IsUnramifiedAtInfinitePlaces k F :=
      hkF.infinitePlaces
    exact
      IsUnramifiedAtInfinitePlaces.bot k K F

Module documentation

Everywhere-unramified towers of number fields

Declarations

IsEverywhereUnramified

refl

trans

top

bot