Module

RamificationSupport.lean

Nyll.SawinTotallyRealTowers.RamificationSupport

6 declarations indexed from sourceView source ↗

Module documentation

Finite ramification support in number-field towers

The initial arithmetic group in the Sawin construction permits ramification at specified finite places. This predicate retains the existing local unramifiedness condition outside that set. Its tower lemmas work also for extensions of even degree; real places are a separate condition.

Imports2

Nyll.ClassFieldTheory.AlgebraicNumberTheory.NumberField.FiniteUnramifiedTower
Mathlib.NumberTheory.RamificationInertia.Unramified

Imported by6

def

IsUnramifiedAtFinitePlacesOutside

L30 ↗

ClassFieldTower.Sawin.IsUnramifiedAtFinitePlacesOutside

Documentation

All finite places above the complement of S are unramified. Finiteness of S is unnecessary for the tower properties below.

Source context 5 commands

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

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

Lean source · statement

def IsUnramifiedAtFinitePlacesOutside
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    (S : Set (HeightOneSpectrum (𝓞 K))) : Prop

theorem

mono

L48 ↗

ClassFieldTower.Sawin.IsUnramifiedAtFinitePlacesOutside.mono

Documentation

Enlarging the permitted ramification set preserves the condition.

Source context 8 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
universe u v w
namespace ClassFieldTower.Sawin
namespace IsUnramifiedAtFinitePlacesOutside
section Basic
variable {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]

Lean source · statement

theorem mono {S T : Set (HeightOneSpectrum (𝓞 K))}
    (hST : S ⊆ T) (h : IsUnramifiedAtFinitePlacesOutside K L S) :
    IsUnramifiedAtFinitePlacesOutside K L T

theorem

empty_iff

L55 ↗

ClassFieldTower.Sawin.IsUnramifiedAtFinitePlacesOutside.empty_iff

Documentation

Empty support recovers the existing finite-place predicate.

Source context 8 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
universe u v w
namespace ClassFieldTower.Sawin
namespace IsUnramifiedAtFinitePlacesOutside
section Basic
variable {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]

Lean source · statement

theorem empty_iff :
    IsUnramifiedAtFinitePlacesOutside K L ∅ ↔
      IsUnramifiedAtFinitePlaces K L

theorem

refl

L67 ↗

ClassFieldTower.Sawin.IsUnramifiedAtFinitePlacesOutside.refl

Documentation

The base field itself is a candidate for every support set.

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
universe u v w
namespace ClassFieldTower.Sawin
namespace IsUnramifiedAtFinitePlacesOutside

Lean source · statement

theorem refl (K : Type u) [Field K] [NumberField K]
    (S : Set (HeightOneSpectrum (𝓞 K))) :
    IsUnramifiedAtFinitePlacesOutside K K S

theorem

top

L84 ↗

ClassFieldTower.Sawin.IsUnramifiedAtFinitePlacesOutside.top

Documentation

Over an intermediate field, the permitted support is the set of places above the original support.

Source context 8 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
universe u v w
namespace ClassFieldTower.Sawin
namespace IsUnramifiedAtFinitePlacesOutside
section Tower
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 · statement

theorem top (S : Set (HeightOneSpectrum (𝓞 k)))
    (h : IsUnramifiedAtFinitePlacesOutside k F S) :
    IsUnramifiedAtFinitePlacesOutside K F
      ((finitePlaceBelow (K := k) (L := K)) ⁻¹' S)

theorem

bot

L97 ↗

ClassFieldTower.Sawin.IsUnramifiedAtFinitePlacesOutside.bot

Documentation

A finite intermediate number field inherits the same ramification support on the base. A prime above each intermediate prime is supplied by lying over, rather than assumed as extra input.

Source context 8 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
universe u v w
namespace ClassFieldTower.Sawin
namespace IsUnramifiedAtFinitePlacesOutside
section Tower
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 · statement

theorem bot (S : Set (HeightOneSpectrum (𝓞 k)))
    (h : IsUnramifiedAtFinitePlacesOutside k F S) :
    IsUnramifiedAtFinitePlacesOutside k K S

Module documentation

Finite ramification support in number-field towers

Declarations

IsUnramifiedAtFinitePlacesOutside

mono

empty_iff

refl

top

bot